An analysis of Tennenbaum's theorem in constructive type theory
From MaRDI portal
Publication:6563042
DOI10.46298/lmcs-20(1:19)2024zbMATH Open1541.03168MaRDI QIDQ6563042
Publication date: 27 June 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Church's thesisfirst-order logicconstructive type theoryPeano arithmeticTennenbaum's theoremsynthetic computability
First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50) Type theory (03B38)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Constructive formalization of the Tennenbaum theorem and its applications
- Pairs, sets and sequences in first-order theories
- Variations on a thesis: intuitionism and computability
- The calculus of constructions
- Incompleteness in intuitionistic metamathematics
- Constructivism in mathematics. An introduction. Volume II
- Computable quotient presentations of models of arithmetic and set theory
- Parametric Church's thesis: synthetic computability without choice
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Church's thesis without tears
- On the complexity of models of arithmetic
- Bounded existential induction
- Completeness theorems for first-order logic analysed in constructive type theory
- Trakhtenbrot’s Theorem in Coq
- Constructive validity is nonarithmetic
- Theorem Proving in Higher Order Logics
- Extensions of some theorems of Gödel and Church
- Recursive Predicates and Quantifiers
- Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
- Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
- Game semantics of Martin-Löf type theory
- An analysis of Tennenbaum's theorem in constructive type theory
- Gödel's theorem without tears -- essential incompleteness in synthetic computability
This page was built for publication: An analysis of Tennenbaum's theorem in constructive type theory
