Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding

source

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

Equations

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

Instances For

source

@[implicit_reducible]

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

GödelQuote (Finset (Proposition L)) V

Equations

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

source

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

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

source

@[simp]

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

⌜∅⌝ = ∅

source

@[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 (Proposition L)} {φ : Proposition L} :

⌜φ⌝ ∈ ⌜Γ⌝ ↔ φ ∈ Γ

source

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

⌜Γ⌝ = ⌜Δ⌝ → Γ = Δ

source

@[simp]

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

⌜{φ}⌝ = {⌜φ⌝}

source

@[simp]

theorem LO.FirstOrder.Derivation2.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 LO.FirstOrder.Derivation2.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 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 (Proposition L)} :

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

source

@[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 (Proposition L)} :

⌜Γ⌝ ⊆ ⌜Δ⌝ ↔ Γ ⊆ Δ

source

theorem LO.FirstOrder.Derivation2.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 LO.FirstOrder.Derivation2.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

@[implicit_reducible]

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

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

source

@[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 (Proposition L)) :

⌜Γ⌝.val = ⌜Γ⌝

source

@[simp]

theorem LO.FirstOrder.Derivation2.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 LO.FirstOrder.Derivation2.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 LO.FirstOrder.Derivation2.Sequent.typed_quote_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] :

⌜∅⌝ = ∅

source

@[simp]

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

⌜{φ}⌝ = {⌜φ⌝}

source

@[simp]

theorem LO.FirstOrder.Derivation2.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 LO.FirstOrder.Derivation2.Sequent.typed_quote_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {Γ Δ : Finset (Proposition L)} :

⌜Γ⌝ = ⌜Δ⌝ → Γ = Δ

source

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

↑⌜Γ⌝ = ⌜Γ⌝

source

@[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 (Proposition L)} :

⌜Γ⌝ ⊆ ⌜Δ⌝ ↔ Γ ⊆ Δ

source

theorem LO.FirstOrder.Derivation2.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 LO.FirstOrder.Derivation2.typedQuote (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗜𝚺₁] {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition 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 hΓ) = 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

source

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Derivation2.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 (Derivation2 T Γ) (Arithmetic.Bootstrapping.TDerivation (Theory.internalize V T) ⌜Γ⌝)

Equations

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

source

@[implicit_reducible]

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 (Proposition L)) :

GödelQuote (Derivation2 T Γ) V

Equations

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

source

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 (Proposition L)} (d : Derivation2 T Γ) :

⌜d⌝ = ⌜d⌝.val

source

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 (Proposition L)} (d : Derivation2 T Γ) :

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

source

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 (Proposition L)} (d : Derivation2 T Γ) :

↑⌜d⌝ = ⌜d⌝

source

@[implicit_reducible]

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

GödelQuote (⊢ᴸᴷ¹ Γ) V

Equations

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

source

@[implicit_reducible]

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 ⊢! φ) => ⌜LO.FirstOrder.Theory.Proof.toProof2 b⌝ }

source

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

⌜b⌝ = ⌜Derivation.toDerivation2 ∅ b⌝

source

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⌝ = ⌜Theory.Proof.toProof2 b⌝

source

@[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 : ⊢ᴸᴷ¹ Γ) :

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

source

@[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 ⊢! φ) :

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

source

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⌝

source

theorem LO.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 ∧ Derivable2 T Γ

source

noncomputable def LO.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 LO.FirstOrder.Arithmetic.Bootstrapping.Provable.sound {L : Language} [L.DecidableEq] [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} (h : Provable T ⌜φ⌝) :

T ⊢ φ