Alternative definition of proof

inductive LO.FirstOrder.Derivation2 {L : Language} [L.DecidableEq] (T : Theory L) : Finset (Proposition L) → Type u_1

• closed {L : Language} [L.DecidableEq] {T : Theory L} (Γ : Finset (Proposition L)) (φ : Proposition L) : φ ∈ Γ → ∼φ ∈ Γ → Derivation2 T Γ
• axm {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} (φ : Sentence L) : φ ∈ T → Rewriting.emb φ ∈ Γ → Derivation2 T Γ
• verum {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} : ⊤ ∈ Γ → Derivation2 T Γ
• and {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ ψ : Proposition L} : φ ⋏ ψ ∈ Γ → Derivation2 T (insert φ Γ) → Derivation2 T (insert ψ Γ) → Derivation2 T Γ
• or {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ ψ : Proposition L} : φ ⋎ ψ ∈ Γ → Derivation2 T (insert φ (insert ψ Γ)) → Derivation2 T Γ
• all {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Semiproposition L 1} : ∀⁰ φ ∈ Γ → Derivation2 T (insert (Rewriting.free φ) (Finset.image (⇑Rewriting.shift) Γ)) → Derivation2 T Γ
• exs {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Semiproposition L 1} : ∃⁰ φ ∈ Γ → (t : SyntacticTerm L) → Derivation2 T (insert (φ/[t]) Γ) → Derivation2 T Γ
• wk {L : Language} [L.DecidableEq] {T : Theory L} {Δ Γ : Finset (Proposition L)} : Derivation2 T Δ → Δ ⊆ Γ → Derivation2 T Γ
• shift {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} : Derivation2 T Γ → Derivation2 T (Finset.image (⇑Rewriting.shift) Γ)
• cut {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Proposition L} : Derivation2 T (insert φ Γ) → Derivation2 T (insert (∼φ) Γ) → Derivation2 T Γ

def LO.FirstOrder.«term_⟹₂_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⟹₂_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⟹₂_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹₂") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Derivable2 {L : Language} [L.DecidableEq] (T : Theory L) (Γ : Finset (Proposition L)) : Prop

Equations

• LO.FirstOrder.Derivable2 T Γ = Nonempty (LO.FirstOrder.Derivation2 T Γ)

def LO.FirstOrder.«term_⟹₂!_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⟹₂!_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⟹₂!_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹₂! ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Proof2 {L : Language} [L.DecidableEq] (T : Theory L) (φ : Proposition L) : Type u_1

Equations

• T.Proof2 φ = LO.FirstOrder.Derivation2 T {φ}

def LO.FirstOrder.«term_⊢!₂!_» : Lean.TrailingParserDescr

Equations

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

theorem LO.FirstOrder.shifts_toFinset_eq_image_shift {L : Language} [L.DecidableEq] (Γ : Sequent L) : (Rewriting.shifts Γ).toFinset = Finset.image (⇑Rewriting.shift) (List.toFinset Γ)

def LO.FirstOrder.Derivation.toDerivation2 {L : Language} [L.DecidableEq] (T : Theory L) {Γ : Sequent L} : ⊢ᴸᴷ¹ Γ → Derivation2 T (List.toFinset Γ)

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.toDerivation2 T LO.FirstOrder.Derivation.verum = LO.FirstOrder.Derivation2.verum ⋯
• LO.FirstOrder.Derivation.toDerivation2 T (dp.and dq) = LO.FirstOrder.Derivation2.and ⋯ ((LO.FirstOrder.Derivation.toDerivation2 T dp).wk ⋯) ((LO.FirstOrder.Derivation.toDerivation2 T dq).wk ⋯)
• LO.FirstOrder.Derivation.toDerivation2 T dpq.or = LO.FirstOrder.Derivation2.or ⋯ ((LO.FirstOrder.Derivation.toDerivation2 T dpq).wk ⋯)
• LO.FirstOrder.Derivation.toDerivation2 T dp.all = LO.FirstOrder.Derivation2.all ⋯ ((LO.FirstOrder.Derivation.toDerivation2 T dp).wk ⋯)
• LO.FirstOrder.Derivation.toDerivation2 T dp.exs = LO.FirstOrder.Derivation2.exs ⋯ t ((LO.FirstOrder.Derivation.toDerivation2 T dp).wk ⋯)
• LO.FirstOrder.Derivation.toDerivation2 T (d.contraction h) = (LO.FirstOrder.Derivation.toDerivation2 T d).wk ⋯
• LO.FirstOrder.Derivation.toDerivation2 T (d₁.cut d₂) = ((LO.FirstOrder.Derivation.toDerivation2 T d₁).wk ⋯).cut ((LO.FirstOrder.Derivation.toDerivation2 T d₂).wk ⋯)

structure LO.FirstOrder.Derivation2.ProofData {L : Language} (T : Theory L) (Γ : Finset (Proposition L)) : Type u_1

• axioms : List (Sentence L)
• axioms_mem (ψ : Sentence L) : ψ ∈ self.axioms → ψ ∈ T
• derivation : ⊢ᴸᴷ¹ Γ.toList ++ ∼Sequent.embed self.axioms

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

Equations

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

@[reducible]

noncomputable def LO.FirstOrder.Derivation2.cutManyProof {L : Language} [L.DecidableEq] {T : Theory L} {φ : Proposition L} (A : List (Sentence L)) : (∀ ψ ∈ A, ψ ∈ T) → Derivation2 T (insert φ (List.toFinset (∼Sequent.embed A))) → Derivation2 T {φ}

Equations

• LO.FirstOrder.Derivation2.cutManyProof [] x_3 d = d
• LO.FirstOrder.Derivation2.cutManyProof (ψ :: A) hA d = LO.FirstOrder.Derivation2.cutManyProof A ⋯ (((LO.FirstOrder.Derivation2.axm ψ ⋯ ⋯).cut (d.cast ⋯)).cast ⋯)

@[reducible]

noncomputable def LO.FirstOrder.Derivation2.cutMany {L : Language} [L.DecidableEq] {T : Theory L} {φ : Proposition L} (A : List (Sentence L)) (hA : ∀ ψ ∈ A, ψ ∈ T) (d : Derivable2 T (insert φ (List.toFinset (∼Sequent.embed A)))) : Derivable2 T {φ}

Equations

• ⋯ = ⋯

noncomputable def LO.FirstOrder.Derivation2.toProofData {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} : Derivation2 T Γ → ProofData T Γ

Equations

• One or more equations did not get rendered due to their size.
• (LO.FirstOrder.Derivation2.closed x✝ φ hp hn).toProofData = { axioms := [], axioms_mem := ⋯, derivation := (LO.FirstOrder.Derivation.eta φ).contra ⋯ }
• (LO.FirstOrder.Derivation2.axm φ hT hΓ).toProofData = { axioms := [φ], axioms_mem := ⋯, derivation := (LO.FirstOrder.Derivation.eta (LO.FirstOrder.Rewriting.emb φ)).contra ⋯ }
• (LO.FirstOrder.Derivation2.verum h).toProofData = { axioms := [], axioms_mem := ⋯, derivation := LO.FirstOrder.Derivation.verum.contra ⋯ }

noncomputable def LO.FirstOrder.Derivation2.toProof {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} (d : Derivation2 T Γ) : ∃ (A : List (Sentence L)), (∀ ψ ∈ A, ψ ∈ T) ∧ Nonempty (⊢ᴸᴷ¹ Γ.toList ++ ∼Sequent.embed A)

Equations

• ⋯ = ⋯

noncomputable def LO.FirstOrder.Theory.Proof.toProof2 {L : Language} [L.DecidableEq] {T : Theory L} {φ : Sentence L} (b : T ⊢! φ) : T.Proof2 (Rewriting.emb φ)

Equations

• LO.FirstOrder.Theory.Proof.toProof2 b = LO.FirstOrder.Derivation2.cutManyProof b.axioms ⋯ ((LO.FirstOrder.Derivation.toDerivation2 T b.derivation).cast ⋯)

noncomputable def LO.FirstOrder.Theory.Proof2.toProof {L : Language} [L.DecidableEq] {T : Theory L} {φ : Sentence L} (d : T.Proof2 (Rewriting.emb φ)) : T ⊢! φ

Equations

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

theorem LO.FirstOrder.provable_iff_derivable2 {L : Language} [L.DecidableEq] {T : Theory L} {φ : Sentence L} : T ⊢ φ ↔ Nonempty (T.Proof2 (Rewriting.emb φ))