- Synthetic Computability
- First-Order Logic
- Peano Arithmetic
- ZF set theory with Skolem function symbols
- Axiomatisations
- Reduction from PCP to semantic entailment
- Reduction from PCP to deductive entailment
- Variant allowing intensional models
- Reduction from ZF' to finite ZF
- Reduction from PCP to semantic entailment in finite ZF
- Reduction from PCP to deductive entailment in finite ZF
- Construction of standard models
- ZF set theory without Skolem function symbols
- Finite Set Theory with Adjunction Operation
- Axiomatisations
- Axiomatisation of finite set theory just using membership
- Constructive extensional model of finite set theory
- Indirect reduction from ZF to finite set theory without Skolem functions
- Indirect reduction from ZF to finite set theory with Skolem functions
- Reduction from PCP to semantic entailment
- Reduction from PCP to deductive entailment
- Summary File
- Section 3
- Decision problems on first-order axiomatisations
- Definition 5 : reductions to axiomatisations combine Tarski semantics and intuitionistic ND
- Fact 7 : if a non-trivial problem reduces to T, then T is consistent
- Post's theorem: bi-enumerable logically decidable predicates over discrete domain are decidable
- Fact 9 : consistent complete theories are decidable for closed formulas
- Consequence : problems reducing to complete theories are decidable
- Theorem 10 : undecidability transports to extended axiomatisations satisfied by standard models
- Theorem 10 : variant for classical deduction, using LEM
- Fact 11 : reductions from finite axiomatisations to the Entscheidungsproblem
- Fact 12 : indirect reductions between axiomatisations
- Main results
- Theorem 26 : H10 reduces to Q', Q, and PA
- Theorem 27 : all extensions of Q' satisfied by the standard model are incompletene, using LEM
- Fact 28 : all axiomatisations satisfied by the standard model are undecidable
- Theorem 43 : PCP reduces to Z', Z, and ZF, assuming standard models
- Corollary 44 : the standard models required by the previous theorem can be constructed with CE and TD
- Theorem 45 : all extensions of Z' satisfied by a standard model are incompletene, using LEM
- Theorem 53 : we obtain the same reductions for set theory only formulated with equality and membership
- Theorem 58 : FOL with a single binary relation symbol is undecidable
- Section 3
- Abstract Undecidability and Incompleteness