Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

DOI10.4230/LIPICS.ITP.2021.23OpenAlexW3177449200MaRDI QIDQ6099613

Dominik Kirst, Author name not available (Why is that?)

Publication date: 20 June 2023

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2021/13918/pdf/LIPIcs-ITP-2021-23.pdf/

zbMATH Keywords

undecidabilityfirst-order logicconstructive type theoryPeano arithmeticincompletenessZF set theorycoqsynthetic computability

Mathematics Subject Classification ID

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

Related Items (1)

An analysis of Tennenbaum's theorem in constructive type theory

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• A new method for undecidability proofs of first order theories 👍 👎
• On fixed-point theorems in synthetic computability 👍 👎
• First steps in synthetic computability theory 👍 👎
• Propositional proof systems, the consistency of first order theories and the complexity of computations 👍 👎
• Processes, Terms and Cycles: Steps on the Road to Infinity 👍 👎
• Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version 👍 👎
• Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq 👍 👎

This page was built for publication: Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6099613)