Standalone Lean project
A formal metatheory library covering axiomatic systems, syntax, semantics, proof theory, and incompleteness.
Flagship declarations
ComputablePred.iff_decoded_pred
Plain-language statement
Computability of a predicate on a Primcodable type is equivalent to the computability of the corresponding predicate on ℕ obtained by decoding.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.bv_quote_fixitr
Plain-language statement
bv-pin bridge (over ℕ): bv ⌜fixitr 0 (fvSup χ) ▹ χ⌝ = fvSup χ. - ≤ is immediate from quote_univCl_eq + bv_qqAlls (closing fvSup quantifiers reaches a sentence, whose bv is 0). - ≥ is by level-factoring: were the body an IsSemiformula j for some j < fvSup, IsSemiformula.sound + castLE-invariance would re-express χ as `γ ⇜ ![...
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.conj
Plain-language statement
Crucial inducion for formalized -completeness.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.fvarVec_val_eq
Plain-language statement
fvarVec is the code of the typed substitution vector fun i ↦ ^&i (over a standard length).
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.IsSigma1.of_all
Plain-language statement
Inversion of the bounded-∀ clause: a ^∀-headed 𝚺₁ code is a qqBall.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.le_termBShift
Plain-language statement
termBShift only grows codes: t ≤ termBShift t for well-formed terms. The ^#z → ^#(z+1) bvar shift grows, ^&x is fixed, and functions recurse componentwise. Bounds the ∃ t guard in the bounded-∀ clause.
Source project: Foundation
Person-level attribution pending.
Project index
Showing 8 of 25 additional declarations. Use project search for the complete index.
LO.FirstOrder.Arithmetic.Bootstrapping.quote_subst_fvar_fixitr
Plain-language statement
Closure inversion at the code level. Substituting the free-variable atoms &0 … &(m-1) back into the fixitr-image recovers ⌜φ⌝. This is the DECODE direction: the recognizer can recover ⌜succInd ψ⌝ (hence ψ) from the freevar-free closure body using the already-proven internal subst, with no need for an internal fixitr. Meta witness: `sub...
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.subst_fvarVec_quote
Plain-language statement
Raw closure inversion. subst (fvarVec (fvSup φ)) ⌜fixitr 0 (fvSup φ) ▹ φ⌝ = ⌜φ⌝: the internal substitution by fvarVec undoes the universal-closure fixitr at the code level. This is the recognizer's mechanism for recovering ⌜succInd ψ⌝ from the freevar-free closure body.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.subst_fvarVec_quote'
Plain-language statement
Generalized free-ization. For any β : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ m, substituting the free-variable atoms &0 … &(m-1) for its m bound slots equals ⌜β ⇜ (&·)⌝. This is the forward recognizer's tool: once IsSemiformula.sound yields a β with ⌜β⌝ = b, this computes subst (fvarVec m) b. (Specializes to `subst_fvarVec_quot...
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.Bootstrapping.termBV_termBShift_le
Plain-language statement
termBShift shifts the bound-variable depth up by exactly one (on well-formed terms): so t is a level-m term iff termBShift t is level-(m+1). The ←-direction recovers the lowered arity, which is how the bounded-∀ bound (a termBShift-image) is recognized as a bShift of a real term of the outer arity.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.chSigma1_mem_iff
Plain-language statement
mem_iff math (C = Hierarchy 𝚺 1). Mirrors chUniv_mem_iff, threading the IsSigma1 K side condition through isSigma1_iff_hierarchy.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.church_theorem_general
Project documentation
Church's theorem, for an arbitrary arithmetic theory T ⊇ 𝗥₀ sound on 𝚺₁ sentences: the set of T-provable sentences is not computable.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.closure_inversion
Plain-language statement
Closure inversion (forward keystone). A freevar-free level-m formula β whose internal bv is m and which substitutes back to succInd γ is exactly the fixitr-image, so its m-fold closure is (succInd γ).univCl'. Mirror of bv_quote_fixitr's ≥-direction inversion; the genuine remaining math.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.hierarchy_of_isSigma1
Plain-language statement
(⟹) 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.
Source project: Foundation
Person-level attribution pending.