A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
From MaRDI portal
Publication:2940885
DOI10.1017/S1755020314000112zbMath1337.03021arXiv2104.14260WikidataQ57382547 ScholiaQ57382547MaRDI QIDQ2940885
Publication date: 21 January 2015
Published in: The Review of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2104.14260
Mechanization of proofs and logical operations (03B35) Gödel numberings and issues of incompleteness (03F40)
Related Items
A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle, Computational logic: its origins and applications, Formalization of the resolution calculus for first-order logic, Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started, Undecidable problems in quantum field theory, Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’, The scope of Gödel's first incompleteness theorem, Formalizing Bachmair and Ganzinger's ordered resolution prover, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, A formally verified abstract account of Gödel's incompleteness theorems, NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
Uses Software
Cites Work
