Project Page Index Table of Contents
  • Synthetic computability
    • Church's thesis
    • Church's thesis for mu-recursive functions
    • Weak representability using DPRM
  • Abstract incompleteness
    • Formal systems
    • Folklore proof using soundness
    • Strengthened proof using consistency
    • Q-decidability
    • Σ1 completeness
  • Church's thesis for Q
    • Church's thesis implies EPF
    • Church's thesis implies weak representability and strong separability
    • EPFμ implies CTQ
  • Incompleteness of first-order logic
    • Q is essentially incomplete and essentially undecidable
Generated by coqdoc and improved with CoqdocJS