Project-declaredLean 4.32.1 · mathlib@520045ab

Subst fvar Vec quote

LO.FirstOrder.Arithmetic.Bootstrapping.subst_fvarVec_quote

formal logic metatheory proof theory induction scheme delta1

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.

Exact Lean statement

lemma subst_fvarVec_quote (φ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ 0) :
    Bootstrapping.subst ℒₒᵣ (fvarVec ((0 + φ.fvSup : ℕ) : V))
        (⌜(Rew.fixitr 0 φ.fvSup ▹ φ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ (0 + φ.fvSup))⌝ : V)
      = (⌜φ⌝ : V)

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma subst_fvarVec_quote (φ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ 0) :    Bootstrapping.subst ℒₒᵣ (fvarVec ((0 + φ.fvSup : ℕ) : V))        (⌜(Rew.fixitr 0 φ.fvSup ▹ φ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ (0 + φ.fvSup))⌝ : V)      = (⌜φ⌝ : V) := by  set Kt : Bootstrapping.Semiformula V ℒₒᵣ (0 + φ.fvSup) :=    ⌜(Rew.fixitr 0 φ.fvSup ▹ φ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ (0 + φ.fvSup))⌝ with hKt  set w : SemitermVec V ℒₒᵣ (0 + φ.fvSup) 0 :=    (fun i : Fin (0 + φ.fvSup) ↦ (Semiterm.fvar (↑(i : ℕ)) : Bootstrapping.Semiterm V ℒₒᵣ 0)) with hw  rw [fvarVec_val_eq,    show (⌜(Rew.fixitr 0 φ.fvSup ▹ φ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ (0 + φ.fvSup))⌝ : V) = Kt.val from rfl,    show Bootstrapping.subst ℒₒᵣ w.val Kt.val = (Kt.subst w).val from rfl,    ← quote_subst_fvar_fixitr (V := V) φ]  congr 1  rw [hKt]  simp only [FirstOrder.Semiformula.typed_quote_substs, hw, Semiterm.typed_quote_fvar]

Project: Foundation
License: Apache-2.0
Commit: 8dcdb3196454
Source: Foundation/FirstOrder/Incompleteness/InductionSchemeDelta1.lean:434-448

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.1

Computable Pred iff decoded pred

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.

formal logicmetatheoryproof theory

Source project: Foundation

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.1

Bv quote fixitr

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 `γ ⇜ ![...

formal logicmetatheoryproof theory

Source project: Foundation

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.1

Conj

LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.conj

Plain-language statement

Crucial inducion for formalized $\Sigma_1$ -completeness.

formal logicmetatheoryproof theory

Source project: Foundation

Person-level attribution pending.

View proof record