Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Proof.Coding

source

noncomputable def FFL.FirstOrder.LK2.Derivation.Sequent.quote (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ : Finset (Proposition L)) :

Equations

FFL.FirstOrder.LK2.Derivation.Sequent.quote V Γ = ∑ φ ∈ Γ, FFL.Exp.exp ⌜φ⌝

Instances For

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.LK2.Derivation.instGödelQuoteFinsetProposition (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] :

GödelQuote (Finset (Proposition L)) V

Equations

FFL.FirstOrder.LK2.Derivation.instGödelQuoteFinsetProposition V = { quote := FFL.FirstOrder.LK2.Derivation.Sequent.quote V }

source

theorem FFL.FirstOrder.LK2.Derivation.Sequent.quote_def (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ : Finset (Proposition L)) :

⌜Γ⌝ = ∑ φ ∈ Γ, Exp.exp ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.quote_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] :

⌜∅⌝ = ∅

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.mem_quote_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ : Finset (Proposition L)} {φ : Proposition L} :

⌜φ⌝ ∈ ⌜Γ⌝ ↔ φ ∈ Γ

source

theorem FFL.FirstOrder.LK2.Derivation.Sequent.quote_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (Proposition L)} :

⌜Γ⌝ = ⌜Δ⌝ → Γ = Δ

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.quote_singleton {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] [L.DecidableEq] (φ : Proposition L) :

⌜{φ}⌝ = {⌜φ⌝}

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.quote_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] [L.DecidableEq] (Γ : Finset (Proposition L)) (φ : Proposition L) :

⌜insert φ Γ⌝ = insert ⌜φ⌝ ⌜Γ⌝

source

theorem FFL.FirstOrder.LK2.Derivation.Sequent.mem_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {x : V} [L.DecidableEq] {Γ : Finset (Proposition L)} (hx : x ∈ ⌜Γ⌝) :

∃ φ ∈ Γ, x = ⌜φ⌝

source

theorem FFL.FirstOrder.LK2.Derivation.Sequent.mem_quote_iff' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {x : V} {Γ : Finset (Proposition L)} :

x ∈ ⌜Γ⌝ ↔ ∃ φ ∈ Γ, x = ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.quote_subset_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (Proposition L)} :

⌜Γ⌝ ⊆ ⌜Δ⌝ ↔ Γ ⊆ Δ

source

theorem FFL.FirstOrder.LK2.Derivation.setShift_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (Proposition L)) :

Arithmetic.Bootstrapping.setShift L ⌜Γ⌝ = ⌜Finset.image (⇑Rewriting.shift) Γ⌝

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.formulaSet_quote_finset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (Proposition L)) :

Arithmetic.Bootstrapping.IsFormulaSet L ⌜Γ⌝

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.LK2.Derivation.instGödelQuoteFinsetPropositionSequent {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] :

GödelQuote (Finset (Proposition L)) (Arithmetic.Bootstrapping.Sequent V L)

Equations

FFL.FirstOrder.LK2.Derivation.instGödelQuoteFinsetPropositionSequent = { quote := fun (Γ : Finset (FFL.FirstOrder.Proposition L)) => { val := ⌜Γ⌝, val_formulaSet := ⋯ } }

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.typed_quote_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (Proposition L)) :

⌜Γ⌝.val = ⌜Γ⌝

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.quote_mem_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {φ : Proposition L} {Γ : Finset (Proposition L)} :

⌜φ⌝ ∈ ⌜Γ⌝ ↔ φ ∈ Γ

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.typed_quote_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (Proposition L)) (φ : Proposition L) :

⌜insert φ Γ⌝ = insert ⌜φ⌝ ⌜Γ⌝

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.typed_quote_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] :

⌜∅⌝ = ∅

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.typed_quote_singleton {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (φ : Proposition L) :

⌜{φ}⌝ = {⌜φ⌝}

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.setShift_typed_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (Proposition L)) :

⌜Finset.image (⇑Rewriting.shift) Γ⌝ = ⌜Γ⌝.shift

source

theorem FFL.FirstOrder.LK2.Derivation.Sequent.typed_quote_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (Proposition L)} :

⌜Γ⌝ = ⌜Δ⌝ → Γ = Δ

source

theorem FFL.FirstOrder.LK2.Derivation.Sequent.coe_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (Proposition L)) :

↑⌜Γ⌝ = ⌜Γ⌝

source

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.Sequent.typed_quote_subset_typed_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (Proposition L)} :

⌜Γ⌝ ⊆ ⌜Δ⌝ ↔ Γ ⊆ Δ

source

theorem FFL.FirstOrder.LK2.Derivation.isFormulaSet_sound {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {s : ℕ} :

Arithmetic.Bootstrapping.IsFormulaSet L s → ∃ (S : Finset (Proposition L)), ⌜S⌝ = s

source

noncomputable def FFL.FirstOrder.LK2.Derivation.typedQuote (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} :

Derivation T Γ → Arithmetic.Bootstrapping.TDerivation (Theory.internalize V T) ⌜Γ⌝

Equations

One or more equations did not get rendered due to their size.
FFL.FirstOrder.LK2.Derivation.typedQuote V (FFL.FirstOrder.LK2.Derivation.closed Γ φ h hn) = FFL.FirstOrder.Arithmetic.Bootstrapping.TDerivation.em ⌜φ⌝ ⋯ ⋯
FFL.FirstOrder.LK2.Derivation.typedQuote V (FFL.FirstOrder.LK2.Derivation.axm φ hT hΓ) = FFL.FirstOrder.Arithmetic.Bootstrapping.TDerivation.byAxm ⌜φ⌝ ⋯ ⋯
FFL.FirstOrder.LK2.Derivation.typedQuote V (FFL.FirstOrder.LK2.Derivation.verum h) = FFL.FirstOrder.Arithmetic.Bootstrapping.TDerivation.verum ⋯
FFL.FirstOrder.LK2.Derivation.typedQuote V (d.wk ss) = (FFL.FirstOrder.LK2.Derivation.typedQuote V d).wk ⋯
FFL.FirstOrder.LK2.Derivation.typedQuote V d.shift = FFL.FirstOrder.Arithmetic.Bootstrapping.TDerivation.cast ⋯ (FFL.FirstOrder.LK2.Derivation.typedQuote V d).shift

Instances For

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.LK2.Derivation.instGödelQuoteTDerivationInternalizeQuoteFinsetPropositionSequent (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (Γ : Finset (Proposition L)) :

GödelQuote (Derivation T Γ) (Arithmetic.Bootstrapping.TDerivation (Theory.internalize V T) ⌜Γ⌝)

Equations

FFL.FirstOrder.LK2.Derivation.instGödelQuoteTDerivationInternalizeQuoteFinsetPropositionSequent V Γ = { quote := FFL.FirstOrder.LK2.Derivation.typedQuote V }

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.LK2.Derivation.instGödelQuote (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (Γ : Finset (Proposition L)) :

GödelQuote (Derivation T Γ) V

Equations

FFL.FirstOrder.LK2.Derivation.instGödelQuote V Γ = { quote := fun (d : FFL.FirstOrder.LK2.Derivation T Γ) => ⌜d⌝.val }

source

theorem FFL.FirstOrder.LK2.Derivation.quote_cast (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ Δ : Finset (Proposition L)} (d : Derivation T Γ) (h : Γ = Δ) :

⌜d.cast h⌝ = ⌜d⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_def (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} (d : Derivation T Γ) :

⌜d⌝ = (typedQuote V d).val

source

theorem FFL.FirstOrder.LK2.Derivation.quote_closed (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} {φ : Proposition L} (h : φ ∈ Γ) (hn : ∼φ ∈ Γ) :

⌜closed Γ φ h hn⌝ = Arithmetic.Bootstrapping.axL ⌜Γ⌝ ⌜φ⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_axm (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} (σ : Sentence L) (hT : σ ∈ T) (hΓ : Rewriting.emb σ ∈ Γ) :

⌜axm σ hT hΓ⌝ = Arithmetic.Bootstrapping.axm ⌜Γ⌝ ⌜σ⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_verum (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} (h : ⊤ ∈ Γ) :

⌜verum h⌝ = Arithmetic.Bootstrapping.verumIntro ⌜Γ⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_and (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} {φ ψ : Proposition L} (h : φ ⋏ ψ ∈ Γ) (d₁ : Derivation T (insert φ Γ)) (d₂ : Derivation T (insert ψ Γ)) :

⌜and h d₁ d₂⌝ = Arithmetic.Bootstrapping.andIntro ⌜Γ⌝ ⌜φ⌝ ⌜ψ⌝ ⌜d₁⌝ ⌜d₂⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_or (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} {φ ψ : Proposition L} (h : φ ⋎ ψ ∈ Γ) (d : Derivation T (insert φ (insert ψ Γ))) :

⌜or h d⌝ = Arithmetic.Bootstrapping.orIntro ⌜Γ⌝ ⌜φ⌝ ⌜ψ⌝ ⌜d⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_all (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} {φ : Semiproposition L 1} (h : ∀¹ φ ∈ Γ) (d : Derivation T (insert (Rewriting.free φ) (Finset.image (⇑Rewriting.shift) Γ))) :

⌜all h d⌝ = Arithmetic.Bootstrapping.allIntro ⌜Γ⌝ ⌜φ⌝ ⌜d⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_exs (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} {φ : Semiproposition L 1} (h : ∃¹ φ ∈ Γ) (t : SyntacticTerm L) (d : Derivation T (insert (φ/[t]) Γ)) :

⌜exs h t d⌝ = Arithmetic.Bootstrapping.exsIntro ⌜Γ⌝ ⌜φ⌝ ⌜t⌝ ⌜d⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_wk (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ Δ : Finset (Proposition L)} (d : Derivation T Δ) (ss : Δ ⊆ Γ) :

⌜d.wk ss⌝ = Arithmetic.Bootstrapping.wkRule ⌜Γ⌝ ⌜d⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_shift (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} (d : Derivation T Γ) :

⌜d.shift⌝ = Arithmetic.Bootstrapping.shiftRule ⌜Finset.image (⇑Rewriting.shift) Γ⌝ ⌜d⌝

source

theorem FFL.FirstOrder.LK2.Derivation.quote_cut (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} {φ : Proposition L} (d₁ : Derivation T (insert φ Γ)) (d₂ : Derivation T (insert (∼φ) Γ)) :

⌜d₁.cut d₂⌝ = Arithmetic.Bootstrapping.cutRule ⌜Γ⌝ ⌜φ⌝ ⌜d₁⌝ ⌜d₂⌝

source

theorem FFL.FirstOrder.LK2.Derivation.coe_typedQuote_val_eq (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} (d : Derivation T Γ) :

↑(typedQuote ℕ d).val = (typedQuote V d).val

source

theorem FFL.FirstOrder.LK2.Derivation.coe_quote_eq (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} (d : Derivation T Γ) :

↑⌜d⌝ = ⌜d⌝

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.instGödelQuoteDerivation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : LK.Sequent L) :

GödelQuote (⊢ᴸᴷ¹ Γ) V

Equations

FFL.FirstOrder.instGödelQuoteDerivation Γ = { quote := fun (b : ⊢ᴸᴷ¹ Γ) => ⌜FFL.FirstOrder.LK.Derivation.toDerivation2 ∅ b⌝ }

source

@[instance_reducible]

noncomputable instance FFL.FirstOrder.instGödelQuotePrfTheorySentence {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (φ : Sentence L) :

GödelQuote (T ⊢! φ) V

Equations

FFL.FirstOrder.instGödelQuotePrfTheorySentence φ = { quote := fun (b : T ⊢! φ) => ⌜FFL.FirstOrder.Theory.Proof.toProof2 b⌝ }

source

theorem FFL.FirstOrder.quote_derivation_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ : LK.Sequent L} (b : ⊢ᴸᴷ¹ Γ) :

⌜b⌝ = ⌜LK.Derivation.toDerivation2 ∅ b⌝

source

theorem FFL.FirstOrder.quote_proof_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} (b : T ⊢! φ) :

⌜b⌝ = ⌜Theory.Proof.toProof2 b⌝

source

@[simp]

theorem FFL.FirstOrder.derivation_of_quote_derivation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : LK.Sequent L} (b : ⊢ᴸᴷ¹ Γ) :

Arithmetic.Bootstrapping.DerivationOf T ⌜b⌝ ⌜Multiset.toFinset Γ⌝

source

@[simp]

theorem FFL.FirstOrder.proof_of_quote_proof2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} (d : T.Proof2 (Rewriting.emb φ)) :

Arithmetic.Bootstrapping.Proof T ⌜d⌝ ⌜φ⌝

source

@[simp]

theorem FFL.FirstOrder.proof_of_quote_proof {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} (b : T ⊢! φ) :

Arithmetic.Bootstrapping.Proof T ⌜b⌝ ⌜φ⌝

source

theorem FFL.FirstOrder.coe_quote_proof_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} (d : T ⊢! φ) :

↑⌜d⌝ = ⌜d⌝

source

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Derivation.sound {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {d : ℕ} (h : Derivation T d) :

∃ (Γ : Finset (Proposition L)), ⌜Γ⌝ = fstIdx d ∧ LK2.Derivable T Γ

source

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.Provable.sound2 {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Proposition L} (h : Provable T ⌜φ⌝) :

T.Proof2 φ

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Provable.sound {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} (h : Provable T ⌜φ⌝) :

T ⊢ φ