- Synthetic Computability
- First-Order Logic
- Peano Arithmetic
- ZF set theory with Skolem function symbols
- ZF set theory without Skolem function symbols
- 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

- Main results
- Theorem 25 : H10 reduces to Q', Q, and PA
- Theorem 26 : all extensions of Q' satisfied by the standard model are incompletene, using LEM
- Theorem 34 : PCP reduces to Z', Z, and ZF, assuming standard models
- Corollary 35 : the standard models required by the previous theorem can be constructed with CE and TD
- Theorem 36 : all extensions of Z' satisfied by a standard model are incompletene, using LEM
- Theorem 44 : we obtain the same reductions for set theory only formulated with equality and membership
- Theorem 45 : FOL with a single binary relation symbol is undecidable

- Section 3