A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS

DOI10.1017/S1755020314000112zbMath1337.03021arXiv2104.14260WikidataQ57382547 ScholiaQ57382547MaRDI QIDQ2940885

Lawrence Charles Paulson

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

zbMATH Keywords

mechanical verificationsecond incompleteness theorem

Mathematics Subject Classification ID

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

• Isabelle/HOL

Cites Work

• Addition and multiplication of sets
• Finite sets and Gödel's incompleteness theorems
• Unnamed Item
• Unnamed Item