Research proof index

!⟪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...

The code of the bounded universal ∀¹[#0 < bShift t] φ is qqBall (termBShift ⌜t⌝) ⌜φ⌝.

Gödel sentence by restricted provability -/ noncomputable abbrev restrictedGödel (e : ℕ) (T : Theory L) [T.Δ₁] : ArithmeticSentence := fixedpoint (∼(T.restrictedProvable e)) private noncomputable abbrev restrictedGödel' (e : ℕ) (T : Theory L) [T.Δ₁] : ArithmeticSentence := ∼(T.restrictedProvable e)/[⌜restrictedGödel e T⌝] private lemma restrictedGödel'_si...

Church's theorem: the set of (purely logically, i.e. ∅-)provable sentences is not computable.

TODO: move to Basic/Syntax/Bootstrapping.Language.lean

Formalized law of noncontradiction cannot be proved. Alternative formulation of Gödel's second incompleteness theorem.