Project Page Index Table of Contents
  • Preliminaries
    • Cantor Pairing
    • Witness Operator
    • Hedberg's Theorem
    • Decidability
    • Lists
    • Enumerability
    • Vectors
  • First-Order Logic
  • Second-Order Logic
    • Syntax
      • Bounds
      • Discreteness
      • Enumerability
      • Substitutions
    • Tarski Semantics
      • Relational Models
  • Second-Order Peano Arithmetic
    • Axioms
    • Standard Model
    • Signature Embedding
    • Categoricity
    • Failure of Upward Löwenheim-Skolem
    • Failure of Compactness
    • Infinitary Incompleteness
  • Incompleteness and Undecidability
    • Definition of Reduction Function
    • Undecidability
    • Not enumerable
    • Incompleteness
  • Henkin Semantics
  • Natural Deduction
    • Tarski Soundness
    • Enumerability
    • Deduction Facts
    • Incompleteness
    • Henkin Soundness
  • Reduction to FOL
    • Definition of Translation Function
    • Semantic Reduction
      • Translate Henkin Model to First-Order Model.
      • Translate First-Order Model to Henkin Model.
      • Full Translation of Validity
    • Deductive Reduction
      • Preliminaries
      • Removal of Falsity Symbols
      • Backwards Translation Function
      • Translation of Derivations
      • Forwards-Backwards Equivalence
      • Final Provability Reduction
  • Consequences of Reduction
    • Completeness
    • Compactness
    • Löwenheim-Skolem
Generated by coqdoc and improved with CoqdocJS