Project Page Index Table of Contents
  • Synthetic Computability
    • Decidability, enumerability, reductions
    • Undecidability
  • First-Order Logic
    • Syntax
    • Tarski Semantics
    • Natural Deduction
  • Peano Arithmetic
    • Axiomatisations
    • The standard model
    • Reduction from H10
  • ZF set theory with Skolem function symbols
    • Axiomatisations
    • Reduction from PCP to semantic entailment
    • Reduction from PCP to deductive entailment
    • Variant allowing intensional models
    • Construction of standard models
      • Extensional model of ZF using CE and TD
      • Extensional model of Z using CE
      • Intensional model of Z' without assumptions
  • ZF set theory without Skolem function symbols
    • Axiomatisations using membership and equality
    • Translation from ZF over Skolem signature
    • Variant allowing intensional models
    • Axiomatisation just using membership
    • Translation from ZF over Skolem signature
  • 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
Generated by coqdoc and improved with CoqdocJS