Project Page
Index
Table of Contents
Synthetic computability
Church's thesis
Church's thesis for mu-recursive functions
Abstract incompleteness
Formal systems
Folklore proof using soundness
Strengthened proof using consistency
First-order logic
Q-decidability
Sigma1 completeness
Weak representability implies strong separability using Rosser's trick
Illustrative proof of Rosser's trick using completeness
Incompleteness of first-order logic
Weak representability from DPRM
Q is essentially incomplete and essentially undecidable