Research proof index

(⟹) A 𝚺₁-recognized code is the code of a 𝚺₁ formula. Meta-induction on the formula: atoms are 𝚺₁ unconditionally; ∧/∨/∃ recurse; the ^∀ case is forced into the bounded shape by the recognizer (IsSigma1.of_all), and the bound is a bShift-image (positivity via termBV_termBShift_le), so Hierarchy.ball applies.

Gödel's first incompleteness theorem

(⟸) Every 𝚺₁ formula has a 𝚺₁-recognized code. By sigma₁_induction'.

RHS of chSigma1_mem_iff reduced to a clean ∃ψ (with the 𝚺₁ side condition).

RHS of chUniv_mem_iff reduced to a clean ∃ψ over the syntactic universal closure.

!⟪x, y, z, ...⟫ notation for Seq -/ syntax "⟪" term,* "⟫" : term macro_rules | (⟪$term:term, $terms:term,*⟫) => (pair $term ⟪$terms,*⟫) | (⟪$term:term⟫) => ($term) @[app_unexpander pair] meta def pairUnexpander : Lean.PrettyPrinter.Unexpander | `($_ $term$term2) => `(⟪$term,$term2⟫) | _ => throw () lemma pair_graph {a b c : V} : c = ⟪a, b⟫ ↔ (a...