Subst fvar Vec quote
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...
Exact Lean statement
lemma subst_fvarVec_quote' {m : ℕ} (β : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ m) :
Bootstrapping.subst ℒₒᵣ (fvarVec ((m : ℕ) : V)) (⌜β⌝ : V)
= (⌜(β ⇜ (fun i : Fin m ↦ (&↑i : SyntacticTerm ℒₒᵣ)))⌝ : V)Formal artifact
Lean source
lemma subst_fvarVec_quote' {m : ℕ} (β : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ m) : Bootstrapping.subst ℒₒᵣ (fvarVec ((m : ℕ) : V)) (⌜β⌝ : V) = (⌜(β ⇜ (fun i : Fin m ↦ (&↑i : SyntacticTerm ℒₒᵣ)))⌝ : V) := by set Kt : Bootstrapping.Semiformula V ℒₒᵣ m := ⌜β⌝ with hKt set w : SemitermVec V ℒₒᵣ m 0 := (fun i : Fin m ↦ (Semiterm.fvar (↑(i : ℕ)) : Bootstrapping.Semiterm V ℒₒᵣ 0)) with hw rw [fvarVec_val_eq, show (⌜β⌝ : V) = Kt.val from rfl, show Bootstrapping.subst ℒₒᵣ w.val Kt.val = (Kt.subst w).val from rfl] rw [show (⌜(β ⇜ (fun i : Fin m ↦ (&↑i : SyntacticTerm ℒₒᵣ)))⌝ : V) = (⌜(β ⇜ (fun i : Fin m ↦ (&↑i : SyntacticTerm ℒₒᵣ)))⌝ : Bootstrapping.Semiformula V ℒₒᵣ 0).val from rfl] 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:454-467
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
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.
Source project: Foundation
Person-level attribution pending.
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 `γ ⇜ ![...
Source project: Foundation
Person-level attribution pending.
Conj
LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.conj
Plain-language statement
Crucial inducion for formalized -completeness.
Source project: Foundation
Person-level attribution pending.