Project Page Index Table of Contents
  • Basic First-Order Logic
    • Syntax
    • Syntax Facts
    • Natural Deduction
    • Natural Deduction Facts
    • Tarski Semantics
    • Tarski Soundness
    • Kripke Semantics
    • Kripke Soundness
    • Heyting Semantics
    • Heyting Soundness
    • Peano Arithmetic
    • Eliminating excluded middle
  • Completeness
    • Henkin Constructions
    • Tarski Completeness
    • Kripke Completeness
    • MacNeille Completion
    • Lindenbaum Algebra
    • Heyting Completeness
    • Boolean Completeness
  • Undecidability
    • The Entscheidungsproblem
    • Signature Minimisation
    • Trakhtenbrot's Theorem
    • Peano Arithmetic
    • Set Theory
  • Incompleteness
    • Church's Thesis
    • Abstract Incompleteness
    • Church's Thesis for Q
    • Essential Incompleteness of Q
Generated by coqdoc and improved with CoqdocJS