Distilling the requirements of Gödel's incompleteness theorems with a proof assistant

DOI10.1007/s10817-021-09599-8OpenAlexW3196549399WikidataQ113901237 ScholiaQ113901237MaRDI QIDQ2051568

Andrei Popescu, Dmitriy Traytel

Publication date: 24 November 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-021-09599-8

zbMATH Keywords

formal verificationproof assistantGödel's incompleteness theoremsIsabelle/HOLabstract requirements

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Isabelle/HOL
• HOL Light
• Sledgehammer
• NQTHM
• HOLyHammer
• Nominal Isabelle
• Locales
• Eisbach
• GitHub
• Archive Formal Proofs
• Robinson arithmetic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Eisbach: a proof method language for Isabelle
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Nominal techniques in Isabelle/HOL
• Self-reference and modal logic
• Automated proofs of Löb's theorem and Gödel's two incompleteness theorems
• Abstract proof checking: An example motivated by an incompleteness theorem
• Isabelle/HOL. A proof assistant for higher-order logic
• From types to sets by local type definition in higher-order logic
• Automated search for Gödel's proofs
• HOL(y)Hammer: online ATP service for HOL Light
• The scope of Gödel's first incompleteness theorem
• A formally verified abstract account of Gödel's incompleteness theorems
• Term-generic logic
• Locales: a module system for mathematical theories
• Institution-independent model theory
• Undecidable theories
• Concrete Semantics
• A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
• A Consistent Foundation for Isabelle/HOL
• Comprehending Isabelle/HOL’s Consistency
• HOL Light: An Overview
• Unified Classical Logic Completeness
• Solution of a problem of Leon Henkin
• Nominal (Universal) Algebra: Equational Logic with Names and Binding
• Metamathematics, Machines and Gödel's Proof
• Institutions: abstract model theory for specification and programming
• Redundancies in the Hilbert-Bernays derivability conditions for Gödel's second incompleteness theorem
• GENERALIZATIONS OF GÖDEL’S INCOMPLETENESS THEOREMS FOR ∑_n-DEFINABLE THEORIES OF ARITHMETIC
• Finite sets and Gödel's incompleteness theorems
• Theorem Proving in Higher Order Logics
• Formalizing Bachmair and Ganzinger's ordered resolution prover

This page was built for publication: Distilling the requirements of Gödel's incompleteness theorems with a proof assistant