Documentation

Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding

def LO.FirstOrder.Derivation2.cast {L : Language} [L.DecidableEq] {T : Theory L} {Γ Δ : Finset (SyntacticFormula L)} (d : Derivation2 (↑T) Γ) (h : Γ = Δ) :

Derivation2 (↑T) Δ

Equations

d.cast h = h ▸ d

Instances For

noncomputable def LO.FirstOrder.Derivation2.Sequent.quote (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ : Finset (SyntacticFormula L)) :

V

Equations

LO.FirstOrder.Derivation2.Sequent.quote V Γ = ∑ φ ∈ Γ, LO.Exp.exp ⌜φ⌝

Instances For

noncomputable instance LO.FirstOrder.Derivation2.instGödelQuoteFinsetSyntacticFormula (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] :

GödelQuote (Finset (SyntacticFormula L)) V

Equations

LO.FirstOrder.Derivation2.instGödelQuoteFinsetSyntacticFormula V = { quote := LO.FirstOrder.Derivation2.Sequent.quote V }

theorem LO.FirstOrder.Derivation2.Sequent.quote_def (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ : Finset (SyntacticFormula L)) :

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

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.quote_empty {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] :

⌜∅⌝ = ∅

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.mem_quote_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ : Finset (SyntacticFormula L)} {φ : SyntacticFormula L} :

⌜φ⌝ ∈ ⌜Γ⌝ ↔ φ ∈ Γ

theorem LO.FirstOrder.Derivation2.Sequent.quote_inj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (SyntacticFormula L)} :

⌜Γ⌝ = ⌜Δ⌝ → Γ = Δ

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.quote_singleton {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] [L.DecidableEq] (φ : SyntacticFormula L) :

⌜{φ}⌝ = {⌜φ⌝}

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.quote_insert {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] [L.DecidableEq] (Γ : Finset (SyntacticFormula L)) (φ : SyntacticFormula L) :

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

theorem LO.FirstOrder.Derivation2.Sequent.mem_quote {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {x : V} [L.DecidableEq] {Γ : Finset (SyntacticFormula L)} (hx : x ∈ ⌜Γ⌝) :

∃ φ ∈ Γ, x = ⌜φ⌝

theorem LO.FirstOrder.Derivation2.Sequent.mem_quote_iff' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {x : V} {Γ : Finset (SyntacticFormula L)} :

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

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.quote_subset_quote {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (SyntacticFormula L)} :

⌜Γ⌝ ⊆ ⌜Δ⌝ ↔ Γ ⊆ Δ

theorem LO.FirstOrder.Derivation2.setShift_quote {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (SyntacticFormula L)) :

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

@[simp]

theorem LO.FirstOrder.Derivation2.formulaSet_quote_finset {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (SyntacticFormula L)) :

Arithmetic.Bootstrapping.IsFormulaSet L ⌜Γ⌝

noncomputable instance LO.FirstOrder.Derivation2.instGödelQuoteFinsetSyntacticFormulaSequent {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] :

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

Equations

LO.FirstOrder.Derivation2.instGödelQuoteFinsetSyntacticFormulaSequent = { quote := fun (Γ : Finset (LO.FirstOrder.SyntacticFormula L)) => { val := ⌜Γ⌝, val_formulaSet := ⋯ } }

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.typed_quote_val {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (SyntacticFormula L)) :

⌜Γ⌝.val = ⌜Γ⌝

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.quote_mem_quote {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {φ : SyntacticFormula L} {Γ : Finset (SyntacticFormula L)} :

⌜φ⌝ ∈ ⌜Γ⌝ ↔ φ ∈ Γ

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.typed_quote_insert {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (SyntacticFormula L)) (φ : SyntacticFormula L) :

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

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.typed_quote_empty {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] :

⌜∅⌝ = ∅

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.typed_quote_singleton {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (φ : SyntacticFormula L) :

⌜{φ}⌝ = {⌜φ⌝}

@[simp]

theorem LO.FirstOrder.Derivation2.setShift_typed_quote {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (SyntacticFormula L)) :

⌜Finset.image Rewriting.shift Γ⌝ = ⌜Γ⌝.shift

theorem LO.FirstOrder.Derivation2.Sequent.typed_quote_inj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (SyntacticFormula L)} :

⌜Γ⌝ = ⌜Δ⌝ → Γ = Δ

theorem LO.FirstOrder.Derivation2.Sequent.coe_eq {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] (Γ : Finset (SyntacticFormula L)) :

↑⌜Γ⌝ = ⌜Γ⌝

@[simp]

theorem LO.FirstOrder.Derivation2.Sequent.typed_quote_subset_typed_quote {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (SyntacticFormula L)} :

⌜Γ⌝ ⊆ ⌜Δ⌝ ↔ Γ ⊆ Δ

theorem LO.FirstOrder.Derivation2.isFormulaSet_sound {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {s : ℕ} :

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

noncomputable def LO.FirstOrder.Derivation2.typedQuote (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (SyntacticFormula L)} :

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

Equations

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

Instances For

noncomputable instance LO.FirstOrder.Derivation2.instGödelQuoteTDerivationInternalizeQuoteFinsetSyntacticFormulaSequent (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (Γ : Finset (SyntacticFormula L)) :

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

Equations

LO.FirstOrder.Derivation2.instGödelQuoteTDerivationInternalizeQuoteFinsetSyntacticFormulaSequent V Γ = { quote := LO.FirstOrder.Derivation2.typedQuote V }

noncomputable instance LO.FirstOrder.Derivation2.instGödelQuote (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (Γ : Finset (SyntacticFormula L)) :

GödelQuote (Derivation2 (↑T) Γ) V

Equations

LO.FirstOrder.Derivation2.instGödelQuote V Γ = { quote := fun (d : LO.FirstOrder.Derivation2 (↑T) Γ) => ⌜d⌝.val }

theorem LO.FirstOrder.Derivation2.quote_def (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (SyntacticFormula L)} (d : Derivation2 (↑T) Γ) :

⌜d⌝ = ⌜d⌝.val

theorem LO.FirstOrder.Derivation2.coe_typedQuote_val_eq (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (SyntacticFormula L)} (d : Derivation2 (↑T) Γ) :

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

theorem LO.FirstOrder.Derivation2.coe_quote_eq (V : Type u_1) [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (SyntacticFormula L)} (d : Derivation2 (↑T) Γ) :

↑⌜d⌝ = ⌜d⌝

noncomputable instance LO.FirstOrder.instGödelQuoteDerivationSchemaSyntacticFormulaToSchema {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (Γ : Sequent L) :

GödelQuote (↑T ⟹ Γ) V

Equations

LO.FirstOrder.instGödelQuoteDerivationSchemaSyntacticFormulaToSchema Γ = { quote := fun (b : ↑T ⟹ Γ) => ⌜LO.FirstOrder.Derivation.toDerivation2 (↑T) b⌝ }

noncomputable instance LO.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

LO.FirstOrder.instGödelQuotePrfTheorySentence φ = { quote := fun (b : T ⊢! φ) => have b := b; ⌜b⌝ }

theorem LO.FirstOrder.quote_derivation_def {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Sequent L} (b : ↑T ⟹ Γ) :

⌜b⌝ = ⌜Derivation.toDerivation2 (↑T) b⌝

theorem LO.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⌝ = ⌜Derivation.toDerivation2 (↑T) b⌝

@[simp]

theorem LO.FirstOrder.derivation_of_quote_derivation {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Sequent L} (b : ↑T ⟹ Γ) :

T.DerivationOf ⌜b⌝ ⌜List.toFinset Γ⌝

@[simp]

theorem LO.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 ⊢! φ) :

T.Proof ⌜b⌝ ⌜φ⌝

theorem LO.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⌝

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

∃ (Γ : Finset (SyntacticFormula L)), ⌜Γ⌝ = Arithmetic.fstIdx d ∧ Derivable2 (↑T) Γ

theorem LO.FirstOrder.Theory.Provable.sound2 {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : SyntacticFormula L} (h : T.Provable ⌜φ⌝) :

Derivable2SingleConseq (↑T) φ

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

T ⊢ φ