Gödel Incompleteness & Provability Logic
GL modal frames · □φ means "φ is provable in PA" · Fixed point: G ↔ ¬□G
GL Frames
Fixed Point
Proof Tree
Theorems
Provability Logic GL
□φ → φ
// T: not in GL!
□(□φ → φ) → □φ
// Löb's theorem
□(φ → ψ) → (□φ → □ψ)
// K axiom
□φ → □□φ
// 4 axiom
¬□⊥
// not in GL (Con(PA) unprovable)
GL Frame Properties