Alternative definition of proof

inductive FFL.FirstOrder.LK2.Derivation {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) : φ ∈ Γ → ∼φ ∈ Γ → Derivation T Γ
• axm {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} (φ : Sentence L) : φ ∈ T → Rewriting.emb φ ∈ Γ → Derivation T Γ
• verum {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} : ⊤ ∈ Γ → Derivation T Γ
• and {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ ψ : Proposition L} : φ ⋏ ψ ∈ Γ → Derivation T (insert φ Γ) → Derivation T (insert ψ Γ) → Derivation T Γ
• or {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ ψ : Proposition L} : φ ⋎ ψ ∈ Γ → Derivation T (insert φ (insert ψ Γ)) → Derivation T Γ
• all {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Semiproposition L 1} : ∀¹ φ ∈ Γ → Derivation T (insert (Rewriting.free φ) (Finset.image (⇑Rewriting.shift) Γ)) → Derivation T Γ
• exs {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Semiproposition L 1} : ∃¹ φ ∈ Γ → (t : SyntacticTerm L) → Derivation T (insert (φ/[t]) Γ) → Derivation T Γ
• wk {L : Language} [L.DecidableEq] {T : Theory L} {Δ Γ : Finset (Proposition L)} : Derivation T Δ → Δ ⊆ Γ → Derivation T Γ
• shift {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} : Derivation T Γ → Derivation T (Finset.image (⇑Rewriting.shift) Γ)
• cut {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Proposition L} : Derivation T (insert φ Γ) → Derivation T (insert (∼φ) Γ) → Derivation T Γ

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

Equations

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

@[reducible, inline]

abbrev FFL.FirstOrder.LK2.Derivable {L : Language} [L.DecidableEq] (T : Theory L) (Γ : Finset (Proposition L)) : Prop

Equations

• FFL.FirstOrder.LK2.Derivable T Γ = Nonempty (FFL.FirstOrder.LK2.Derivation T Γ)

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

Equations

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

@[reducible, inline]

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

Equations

• T.Proof2 φ = FFL.FirstOrder.LK2.Derivation T {φ}

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

Equations

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

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

def FFL.FirstOrder.LK.Derivation.toDerivation2 {L : Language} [L.DecidableEq] (T : Theory L) {Γ : Sequent L} : ⊢ᴸᴷ¹ Γ → LK2.Derivation T (Multiset.toFinset Γ)

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.LK.Derivation.toDerivation2 T FFL.FirstOrder.LK.Derivation.verum = FFL.FirstOrder.LK2.Derivation.verum ⋯
• FFL.FirstOrder.LK.Derivation.toDerivation2 T dpq.or = FFL.FirstOrder.LK2.Derivation.or ⋯ ((FFL.FirstOrder.LK.Derivation.toDerivation2 T dpq).wk ⋯)
• FFL.FirstOrder.LK.Derivation.toDerivation2 T dp.all = FFL.FirstOrder.LK2.Derivation.all ⋯ ((FFL.FirstOrder.LK.Derivation.toDerivation2 T dp).wk ⋯)
• FFL.FirstOrder.LK.Derivation.toDerivation2 T dp.exs = FFL.FirstOrder.LK2.Derivation.exs ⋯ t ((FFL.FirstOrder.LK.Derivation.toDerivation2 T dp).wk ⋯)
• FFL.FirstOrder.LK.Derivation.toDerivation2 T d.contraction = (FFL.FirstOrder.LK.Derivation.toDerivation2 T d).wk ⋯
• FFL.FirstOrder.LK.Derivation.toDerivation2 T d.weakening = (FFL.FirstOrder.LK.Derivation.toDerivation2 T d).wk ⋯
• FFL.FirstOrder.LK.Derivation.toDerivation2 T (d₁.cut d₂) = ((FFL.FirstOrder.LK.Derivation.toDerivation2 T d₁).wk ⋯).cut ((FFL.FirstOrder.LK.Derivation.toDerivation2 T d₂).wk ⋯)

structure FFL.FirstOrder.LK2.Derivation.ProofData {L : Language} (T : Theory L) (Γ : Finset (Proposition L)) : Type u_1

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

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

Equations

• d.cast h = h ▸ d

@[simp]

theorem FFL.FirstOrder.LK2.Derivation.shifts_tilde_embed {L : Language} (A : Multiset (Sentence L)) : Rewriting.shifts (∼LK.Sequent.embed A) = ∼LK.Sequent.embed A

@[reducible]

noncomputable def FFL.FirstOrder.LK2.Derivation.cutManyProof {L : Language} [L.DecidableEq] {T : Theory L} {φ : Proposition L} (A : Multiset (Sentence L)) (hA : ∀ ψ ∈ A, ψ ∈ T) (d : Derivation T (insert φ (Multiset.toFinset (∼LK.Sequent.embed A)))) : Derivation T {φ}

Equations

• FFL.FirstOrder.LK2.Derivation.cutManyProof A hA d = FFL.FirstOrder.LK2.Derivation.cutManyProof.go A.toList ⋯ (d.cast ⋯)

noncomputable def FFL.FirstOrder.LK2.Derivation.cutManyProof.go {L : Language} [L.DecidableEq] {T : Theory L} {φ : Proposition L} (l : List (Sentence L)) : (∀ ψ ∈ l, ψ ∈ T) → Derivation T (insert φ (Multiset.toFinset (∼LK.Sequent.embed ↑l))) → Derivation T {φ}

Equations

• FFL.FirstOrder.LK2.Derivation.cutManyProof.go [] x_3 d = d.cast ⋯
• FFL.FirstOrder.LK2.Derivation.cutManyProof.go (ψ :: l_1) hl d = FFL.FirstOrder.LK2.Derivation.cutManyProof.go l_1 ⋯ (((FFL.FirstOrder.LK2.Derivation.axm ψ ⋯ ⋯).cut (d.cast ⋯)).cast ⋯)

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

Equations

• One or more equations did not get rendered due to their size.
• (FFL.FirstOrder.LK2.Derivation.closed Γ φ hp hn).toProofData = { axioms := 0, axioms_mem := ⋯, derivation := (FFL.FirstOrder.LK.Derivation.eta φ).contra default ⋯ }
• (FFL.FirstOrder.LK2.Derivation.axm φ hT hΓ).toProofData = { axioms := ⦃φ⦄, axioms_mem := ⋯, derivation := (FFL.FirstOrder.LK.Derivation.eta (FFL.FirstOrder.Rewriting.emb φ)).contra default ⋯ }
• (FFL.FirstOrder.LK2.Derivation.verum h).toProofData = { axioms := 0, axioms_mem := ⋯, derivation := FFL.FirstOrder.LK.Derivation.verum.contra default ⋯ }

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

Equations

• FFL.FirstOrder.Theory.Proof.toProof2 b = FFL.FirstOrder.LK2.Derivation.cutManyProof b.axioms ⋯ ((FFL.FirstOrder.LK.Derivation.toDerivation2 T b.derivation).cast ⋯)

noncomputable def FFL.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 FFL.FirstOrder.provable_iff_derivable2 {L : Language} [L.DecidableEq] {T : Theory L} {φ : Sentence L} : T ⊢ φ ↔ Nonempty (T.Proof2 (Rewriting.emb φ))