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 (11)

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

• Unnamed Item

Cites Work

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

This page was built for publication: A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS