One-sided sequent calculus for first-order classical logic

@[reducible, inline]

abbrev FFL.FirstOrder.LK.Sequent (L : Language) : Type u_1

Equations

• FFL.FirstOrder.LK.Sequent L = Multiset (FFL.FirstOrder.Proposition L)

def FFL.FirstOrder.LK.Sequent.newVar {L : Language} (Γ : Sequent L) : ℕ

Equations

• Γ.newVar = Multiset.foldr max 0 (Multiset.map FFL.FirstOrder.Semiformula.fvSup Γ)

theorem FFL.FirstOrder.LK.Sequent.not_fvar?_newVar {L : Language} {φ : Proposition L} {Γ : Sequent L} (h : φ ∈ Γ) : ¬Semiformula.FVar? φ Γ.newVar

def FFL.FirstOrder.LK.Sequent.IsClosed {L : Language} (Γ : Sequent L) : Prop

Equations

• Γ.IsClosed = ∃ φ ∈ Γ, ∼φ ∈ Γ

def FFL.FirstOrder.LK.Sequent.embed {L : Language} (Γ : Multiset (Sentence L)) : Sequent L

Equations

• FFL.FirstOrder.LK.Sequent.embed Γ = Multiset.map (⇑FFL.FirstOrder.Rewriting.emb) Γ

@[simp]

theorem FFL.FirstOrder.LK.Sequent.embed_nil {L : Language} : embed 0 = 0

@[simp]

theorem FFL.FirstOrder.LK.Sequent.embed_singleton {L : Language} {φ : Sentence L} : embed ⦃φ⦄ = ⦃Rewriting.emb φ⦄

@[simp]

theorem FFL.FirstOrder.LK.Sequent.embed_add {L : Language} (Γ Δ : Multiset (Sentence L)) : embed (Γ + Δ) = embed Γ + embed Δ

@[simp]

theorem FFL.FirstOrder.LK.Sequent.embed_shift {L : Language} (Γ : Multiset (Sentence L)) : Rewriting.shifts (embed Γ) = embed Γ

Derivation for $\mathbf{LK}$

inductive FFL.FirstOrder.LK.Derivation {L : Language} : Sequent L → Type u_1

Derivation for $\mathbf{LK}$

• identity {L : Language} {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ℕ 0) : ⊢ᴸᴷ¹ ⦃Semiformula.rel r v⦄ + ⦃Semiformula.nrel r v⦄
• cut {L : Language} {Γ : Sequent L} {φ : Proposition L} {Δ : Sequent L} : ⊢ᴸᴷ¹ Γ + ⦃φ⦄ → ⊢ᴸᴷ¹ Δ + ⦃∼φ⦄ → ⊢ᴸᴷ¹ Γ + Δ
• contraction {L : Language} {Γ : Multiset (Proposition L)} {φ : Proposition L} : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃φ⦄) → ⊢ᴸᴷ¹ Γ + ⦃φ⦄
• weakening {L : Language} {Γ : Sequent L} {φ : Proposition L} : ⊢ᴸᴷ¹ Γ → ⊢ᴸᴷ¹ Γ + ⦃φ⦄
• verum {L : Language} : ⊢ᴸᴷ¹ ⦃⊤⦄
• or {L : Language} {Γ : Multiset (Proposition L)} {φ ψ : Proposition L} : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃ψ⦄) → ⊢ᴸᴷ¹ Γ + ⦃φ ⋎ ψ⦄
• and {L : Language} {Γ : Multiset (Proposition L)} {φ ψ : Proposition L} : ⊢ᴸᴷ¹ Γ + ⦃φ⦄ → ⊢ᴸᴷ¹ Γ + ⦃ψ⦄ → ⊢ᴸᴷ¹ Γ + ⦃φ ⋏ ψ⦄
• all {L : Language} {Γ : Multiset (Semiproposition L 0)} {φ : Semiproposition L (0 + 1)} : ⊢ᴸᴷ¹ Rewriting.shifts Γ + ⦃Semiformula.free φ⦄ → ⊢ᴸᴷ¹ Γ + ⦃∀¹ φ⦄
• exs {L : Language} {Γ : Multiset (Semiproposition L 0)} {φ : Semiproposition L (Nat.succ 0)} {t : Semiterm L ℕ 0} : ⊢ᴸᴷ¹ Γ + ⦃φ/[t]⦄ → ⊢ᴸᴷ¹ Γ + ⦃∃¹ φ⦄

def FFL.FirstOrder.«term⊢ᴸᴷ¹_» : Lean.ParserDescr

Equations

• FFL.FirstOrder.«term⊢ᴸᴷ¹_» = Lean.ParserDescr.node `FFL.FirstOrder.«term⊢ᴸᴷ¹_» 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ᴸᴷ¹ ") (Lean.ParserDescr.cat `term 45))

def FFL.FirstOrder.LK.Derivation.height {L : Language} {Δ : Sequent L} : ⊢ᴸᴷ¹ Δ → ℕ

Equations

• (FFL.FirstOrder.LK.Derivation.identity r v).height = 0
• (dp.cut dn).height = max dp.height dn.height + 1
• d.contraction.height = d.height + 1
• d.weakening.height = d.height + 1
• FFL.FirstOrder.LK.Derivation.verum.height = 0
• d.or.height = d.height + 1
• (dp.and dq).height = max dp.height dq.height + 1
• d.all.height = d.height + 1
• d.exs.height = d.height + 1

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_id {L : Language} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ℕ 0} : (identity r v).height = 0

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_cut {L : Language} {Γ Δ : Sequent L} {φ : Proposition L} (dp : ⊢ᴸᴷ¹ Γ + ⦃φ⦄) (dn : ⊢ᴸᴷ¹ Δ + ⦃∼φ⦄) : (dp.cut dn).height = (max dp.height dn.height).succ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_contraction {L : Language} {Γ : Sequent L} {φ : Proposition L} (d : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃φ⦄)) : d.contraction.height = d.height.succ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_weakening {L : Language} {Γ : Sequent L} {φ : Proposition L} (d : ⊢ᴸᴷ¹ Γ) : d.weakening.height = d.height.succ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_verum {L : Language} : verum.height = 0

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_and {L : Language} {Γ : Sequent L} {φ ψ : Proposition L} (dp : ⊢ᴸᴷ¹ Γ + ⦃φ⦄) (dq : ⊢ᴸᴷ¹ Γ + ⦃ψ⦄) : (dp.and dq).height = (max dp.height dq.height).succ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_or {L : Language} {Γ : Sequent L} {φ ψ : Proposition L} (d : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃ψ⦄)) : d.or.height = d.height.succ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_all {L : Language} {Γ : Sequent L} {φ : Semiproposition L 1} (d : ⊢ᴸᴷ¹ Rewriting.shifts Γ + ⦃Semiformula.free φ⦄) : d.all.height = d.height.succ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_exs {L : Language} {Γ : Sequent L} {t : Semiterm L ℕ 0} {φ : Semiproposition L (Nat.succ 0)} (d : ⊢ᴸᴷ¹ Γ + ⦃φ/[t]⦄) : d.exs.height = d.height.succ

@[reducible, inline]

abbrev FFL.FirstOrder.LK.Derivation.cast {L : Language} {Γ Δ : Sequent L} (d : ⊢ᴸᴷ¹ Δ) (e : Δ = Γ := by abel) : ⊢ᴸᴷ¹ Γ

Equations

• d.cast e = e ▸ d

@[simp]

theorem FFL.FirstOrder.LK.Derivation.height_cast {L : Language} {Γ Δ : Sequent L} (d : ⊢ᴸᴷ¹ Δ) (e : Δ = Γ) : (d.cast e).height = d.height

@[instance_reducible]

instance FFL.FirstOrder.LK.Derivation.instStructuralProposition {L : Language} : Structural Derivation

Equations

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

def FFL.FirstOrder.LK.Derivation.traversal {L : Language} [L.DecidableEq] {Γ : Sequent L} : ⊢ᴸᴷ¹ Γ → Multiset.Traversal Γ

Enumerates the end sequent by recursion on the local inference rules. This is a routine syntactic construction.

Equations

• One or more equations did not get rendered due to their size.
• (FFL.FirstOrder.LK.Derivation.identity r v).traversal = Multiset.Traversal.succ (FFL.FirstOrder.Semiformula.nrel r v) (Multiset.Traversal.atom (FFL.FirstOrder.Semiformula.rel r v))
• (dp.cut dn).traversal = dp.traversal.remove.add dn.traversal.remove
• d.contraction.traversal = (Multiset.Traversal.cast ⋯ d.traversal).remove
• d.weakening.traversal = Multiset.Traversal.succ φ d.traversal
• FFL.FirstOrder.LK.Derivation.verum.traversal = Multiset.Traversal.atom ⊤
• d.or.traversal = Multiset.Traversal.succ (φ ⋎ ψ) (Multiset.Traversal.cast ⋯ d.traversal).remove.remove
• (dp.and dq).traversal = Multiset.Traversal.succ (φ ⋏ ψ) dp.traversal.remove
• d.exs.traversal = Multiset.Traversal.succ (∃¹ φ) d.traversal.remove

def FFL.FirstOrder.LK.Derivation.contra {L : Language} {Γ Δ : Sequent L} [L.DecidableEq] (d : ⊢ᴸᴷ¹ Δ) (t : Multiset.Traversal Γ) (h : Δ ⊆ Γ := by simp) : ⊢ᴸᴷ¹ Γ

Applies structural rules along supplied traversals (a routine derived rule).

Equations

• d.contra t h = FFL.Structural.ofSubset d.traversal t d h

def FFL.FirstOrder.LK.Derivation.tensor {L : Language} {Γ Δ : Sequent L} {φ ψ : Proposition L} (tΓ : Multiset.Traversal Γ) (tΔ : Multiset.Traversal Δ) (dφ : ⊢ᴸᴷ¹ Γ + ⦃φ⦄) (dψ : ⊢ᴸᴷ¹ Δ + ⦃ψ⦄) : ⊢ᴸᴷ¹ Γ + Δ + ⦃φ ⋏ ψ⦄

Equations

• FFL.FirstOrder.LK.Derivation.tensor tΓ tΔ dφ dψ = ((FFL.Structural.weakenMany tΔ dφ).cast ⋯).and ((FFL.Structural.weakenMany tΓ dψ).cast ⋯)

@[irreducible]

def FFL.FirstOrder.LK.Derivation.eta {L : Language} (φ : Proposition L) : ⊢ᴸᴷ¹ ⦃φ⦄ + ⦃∼φ⦄

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.LK.Derivation.eta (FFL.FirstOrder.Semiformula.rel R v) = FFL.FirstOrder.LK.Derivation.identity R v
• FFL.FirstOrder.LK.Derivation.eta (FFL.FirstOrder.Semiformula.nrel R v) = (FFL.FirstOrder.LK.Derivation.identity R v).cast ⋯
• FFL.FirstOrder.LK.Derivation.eta FFL.FirstOrder.Semiformula.verum = FFL.FirstOrder.LK.Derivation.verum.weakening
• FFL.FirstOrder.LK.Derivation.eta FFL.FirstOrder.Semiformula.falsum = FFL.FirstOrder.LK.Derivation.verum.weakening.cast ⋯
• FFL.FirstOrder.LK.Derivation.eta (FFL.FirstOrder.Semiformula.all φ) = (((FFL.FirstOrder.LK.Derivation.eta (FFL.FirstOrder.Semiformula.free φ)).cast ⋯).exs.cast ⋯).all.cast ⋯
• FFL.FirstOrder.LK.Derivation.eta (FFL.FirstOrder.Semiformula.exs φ) = (((FFL.FirstOrder.LK.Derivation.eta (FFL.FirstOrder.Semiformula.free φ)).cast ⋯).exs.cast ⋯).all.cast ⋯

@[instance_reducible]

instance FFL.FirstOrder.LK.Derivation.instOneSidedLKProposition {L : Language} : OneSidedLK Derivation

Equations

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

@[instance_reducible]

instance FFL.FirstOrder.LK.Derivation.instCutProposition {L : Language} : OneSidedLK.Cut Derivation

Equations

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

theorem FFL.FirstOrder.LK.Derivation.of_isClosed {L : Language} {Γ : Sequent L} (h : Γ.IsClosed) : Nonempty (⊢ᴸᴷ¹ Γ)

def FFL.FirstOrder.LK.Derivation.rewrite {L : Language} {Γ : Sequent L} (f : ℕ → SyntacticTerm L) : ⊢ᴸᴷ¹ Γ → ⊢ᴸᴷ¹ Multiset.map (fun (x : Semiproposition L 0) => (Rewriting.app (Rew.rewrite f)) x) Γ

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.LK.Derivation.rewrite f (FFL.FirstOrder.LK.Derivation.identity r v) = FFL.FirstOrder.LK.Derivation.identity r (⇑(FFL.FirstOrder.Rew.rewrite f) ∘ v)
• FFL.FirstOrder.LK.Derivation.rewrite f (dp.cut dn) = (((FFL.FirstOrder.LK.Derivation.rewrite f dp).cast ⋯).cut ((FFL.FirstOrder.LK.Derivation.rewrite f dn).cast ⋯)).cast ⋯
• FFL.FirstOrder.LK.Derivation.rewrite f d.contraction = ((FFL.FirstOrder.LK.Derivation.rewrite f d).cast ⋯).contraction.cast ⋯
• FFL.FirstOrder.LK.Derivation.rewrite f d.weakening = (FFL.FirstOrder.LK.Derivation.rewrite f d).weakening.cast ⋯
• FFL.FirstOrder.LK.Derivation.rewrite f FFL.FirstOrder.LK.Derivation.verum = FFL.FirstOrder.LK.Derivation.verum
• FFL.FirstOrder.LK.Derivation.rewrite f d.or = ((FFL.FirstOrder.LK.Derivation.rewrite f d).cast ⋯).or.cast ⋯
• FFL.FirstOrder.LK.Derivation.rewrite f (dp.and dq) = (((FFL.FirstOrder.LK.Derivation.rewrite f dp).cast ⋯).and ((FFL.FirstOrder.LK.Derivation.rewrite f dq).cast ⋯)).cast ⋯
• FFL.FirstOrder.LK.Derivation.rewrite f d.exs = ((FFL.FirstOrder.LK.Derivation.rewrite f d).cast ⋯).exs.cast ⋯

def FFL.FirstOrder.LK.Derivation.map {L : Language} {Δ : Sequent L} (d : ⊢ᴸᴷ¹ Δ) (f : ℕ → ℕ) : ⊢ᴸᴷ¹ Multiset.map (fun (x : Semiproposition L 0) => (Rewriting.app (Rew.rewriteMap f)) x) Δ

Equations

• d.map f = FFL.FirstOrder.LK.Derivation.rewrite (fun (x : ℕ) => FFL.FirstOrder.Semiterm.fvar (f x)) d

def FFL.FirstOrder.LK.Derivation.shift {L : Language} {Δ : Sequent L} (d : ⊢ᴸᴷ¹ Δ) : ⊢ᴸᴷ¹ Rewriting.shifts Δ

Equations

• d.shift = (d.map Nat.succ).cast ⋯

theorem FFL.FirstOrder.LK.Derivation.shifts_image {L₁ : Language} {L₂ : Language} (Φ : L₁.Hom L₂) {Δ : Multiset (Proposition L₁)} : Rewriting.shifts (Multiset.map (⇑(Semiformula.lMap Φ)) Δ) = Multiset.map (⇑(Semiformula.lMap Φ)) (Rewriting.shifts Δ)

def FFL.FirstOrder.LK.Derivation.lMap {L₁ : Language} {L₂ : Language} (Φ : L₁.Hom L₂) {Γ : Sequent L₁} : ⊢ᴸᴷ¹ Γ → ⊢ᴸᴷ¹ Multiset.map (⇑(Semiformula.lMap Φ)) Γ

Equations

• FFL.FirstOrder.LK.Derivation.lMap Φ (FFL.FirstOrder.LK.Derivation.identity r v) = (FFL.FirstOrder.LK.Derivation.identity (Φ.rel r) fun (i : Fin k) => FFL.FirstOrder.Semiterm.lMap Φ (v i)).cast ⋯
• FFL.FirstOrder.LK.Derivation.lMap Φ (dp.cut dn) = (((FFL.FirstOrder.LK.Derivation.lMap Φ dp).cast ⋯).cut ((FFL.FirstOrder.LK.Derivation.lMap Φ dn).cast ⋯)).cast ⋯
• FFL.FirstOrder.LK.Derivation.lMap Φ d.contraction = ((FFL.FirstOrder.LK.Derivation.lMap Φ d).cast ⋯).contraction.cast ⋯
• FFL.FirstOrder.LK.Derivation.lMap Φ d.weakening = (FFL.FirstOrder.LK.Derivation.lMap Φ d).weakening.cast ⋯
• FFL.FirstOrder.LK.Derivation.lMap Φ FFL.FirstOrder.LK.Derivation.verum = ⋯.mpr FFL.FirstOrder.LK.Derivation.verum
• FFL.FirstOrder.LK.Derivation.lMap Φ d.or = ((FFL.FirstOrder.LK.Derivation.lMap Φ d).cast ⋯).or.cast ⋯
• FFL.FirstOrder.LK.Derivation.lMap Φ (dp.and dq) = (((FFL.FirstOrder.LK.Derivation.lMap Φ dp).cast ⋯).and ((FFL.FirstOrder.LK.Derivation.lMap Φ dq).cast ⋯)).cast ⋯
• FFL.FirstOrder.LK.Derivation.lMap Φ d.all = ((FFL.FirstOrder.LK.Derivation.lMap Φ d).cast ⋯).all.cast ⋯
• FFL.FirstOrder.LK.Derivation.lMap Φ d.exs = ((FFL.FirstOrder.LK.Derivation.lMap Φ d).cast ⋯).exs.cast ⋯

def FFL.FirstOrder.LK.Derivation.generalizeByNewVar {L : Language} {Δ : Sequent L} {m : ℕ} {φ : Semiproposition L 1} (hp : ¬Semiformula.FVar? φ m) (hΔ : ∀ ψ ∈ Δ, ¬Semiformula.FVar? ψ m) (d : ⊢ᴸᴷ¹ Δ + ⦃φ/[Semiterm.fvar m]⦄) : ⊢ᴸᴷ¹ Δ + ⦃∀¹ φ⦄

Equations

• FFL.FirstOrder.LK.Derivation.generalizeByNewVar hp hΔ d = ((d.map fun (x : ℕ) => if x = m then 0 else x + 1).cast ⋯).all

Classical proof system

inductive FFL.FirstOrder.LK (L : Language) : Type

• symbol {L : Language} : LK L

def FFL.FirstOrder.«term𝐋𝐊¹» : Lean.ParserDescr

Equations

• FFL.FirstOrder.«term𝐋𝐊¹» = Lean.ParserDescr.node `FFL.FirstOrder.«term𝐋𝐊¹» 1024 (Lean.ParserDescr.symbol "𝐋𝐊¹")

def FFL.FirstOrder.«term𝐋𝐊¹[_]» : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev FFL.FirstOrder.LK.Proof {L : Language} (φ : Proposition L) : Type u_1

Equations

• FFL.FirstOrder.LK.Proof φ = (⊢ᴸᴷ¹ ⦃φ⦄)

@[instance_reducible]

instance FFL.FirstOrder.instEntailmentLKProposition {L : Language} : Entailment (LK L) (Proposition L)

Equations

• FFL.FirstOrder.instEntailmentLKProposition = { Prf := fun (x : FFL.FirstOrder.LK L) => FFL.FirstOrder.LK.Proof }

theorem FFL.FirstOrder.LK.Proof.def_eq {L : Language} (φ : Proposition L) : (𝐋𝐊¹ ⊢! φ) = (⊢ᴸᴷ¹ ⦃φ⦄)

theorem FFL.FirstOrder.LK.Proof.provable_def {L : Language} (φ : Proposition L) : 𝐋𝐊¹ ⊢ φ ↔ Nonempty (⊢ᴸᴷ¹ ⦃φ⦄)

theorem FFL.FirstOrder.LK.Proof.unprovable_def {L : Language} (φ : Proposition L) : 𝐋𝐊¹ ⊬ φ ↔ IsEmpty (⊢ᴸᴷ¹ ⦃φ⦄)

@[instance_reducible]

instance FFL.FirstOrder.LK.Proof.instPrincipalEntailmentPropositionDerivationSymbol {L : Language} : OneSidedLK.PrincipalEntailment Derivation 𝐋𝐊¹

Equations

• FFL.FirstOrder.LK.Proof.instPrincipalEntailmentPropositionDerivationSymbol = { equiv := fun {φ : FFL.FirstOrder.Proposition L} => Equiv.refl (𝐋𝐊¹ ⊢! φ) }

@[instance_reducible]

instance FFL.FirstOrder.LK.Proof.classical {L : Language} : Entailment.Cl 𝐋𝐊¹

Equations

• FFL.FirstOrder.LK.Proof.classical = inferInstance

theorem FFL.FirstOrder.LK.Proof.all {L : Language} (φ : Semiproposition L 1) : 𝐋𝐊¹ ⊢ Semiformula.free φ → 𝐋𝐊¹ ⊢ ∀¹ φ

theorem FFL.FirstOrder.LK.Proof.allClosure_fixitr {L : Language} {φ : Proposition L} (dp : 𝐋𝐊¹ ⊢ φ) (m : ℕ) : 𝐋𝐊¹ ⊢ ∀¹* (Rewriting.app (Rew.fixitr 0 m)) φ

theorem FFL.FirstOrder.LK.Proof.univCl' {L : Language} {φ : Proposition L} (b : 𝐋𝐊¹ ⊢ φ) : 𝐋𝐊¹ ⊢ Semiformula.univCl' φ

theorem FFL.FirstOrder.LK.Proof.lMap {L₁ : Language} {L₂ : Language} (Φ : L₁.Hom L₂) {φ : Proposition L₁} : 𝐋𝐊¹ ⊢ φ → 𝐋𝐊¹ ⊢ (Semiformula.lMap Φ) φ

structure FFL.FirstOrder.Theory.Proof {L : Language} (T : Theory L) (σ : Sentence L) : Type u_1

• axioms : Multiset (Sentence L)
• axioms_mem (ψ : Sentence L) : ψ ∈ self.axioms → ψ ∈ T
• derivation : OneSidedLK.Pullback LK.Derivation Rewriting.emb (⦃σ⦄ + ∼self.axioms)

@[instance_reducible]

instance FFL.FirstOrder.Theory.Proof.instEntailmentSentence {L : Language} : Entailment (Theory L) (Sentence L)

Equations

• FFL.FirstOrder.Theory.Proof.instEntailmentSentence = { Prf := FFL.FirstOrder.Theory.Proof }

def FFL.FirstOrder.Theory.Proof.ofDerivation {L : Language} {T : Theory L} {φ : Sentence L} (d : OneSidedLK.Pullback LK.Derivation Rewriting.emb ⦃φ⦄) : T ⊢! φ

A singleton derivation gives a theory proof without using any axioms.

Equations

• FFL.FirstOrder.Theory.Proof.ofDerivation d = { axioms := 0, axioms_mem := ⋯, derivation := FFL.OneSidedLK.cast d ⋯ }

@[instance_reducible]

instance FFL.FirstOrder.Theory.Proof.instCompactSentence {L : Language} : Entailment.Compact (Theory L)

Equations

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

@[instance_reducible]

instance FFL.FirstOrder.Theory.Proof.instModusPonensSentence {L : Language} (T : Theory L) : Entailment.ModusPonens T

Equations

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

@[instance_reducible]

instance FFL.FirstOrder.Theory.Proof.instClSentence {L : Language} {T : Theory L} : Entailment.Cl T

Equations

• FFL.FirstOrder.Theory.Proof.instClSentence = FFL.OneSidedLK.AxiomDerivation.cl T fun {φ : FFL.FirstOrder.Sentence L} => FFL.FirstOrder.Theory.Proof.ofDerivation

@[instance_reducible]

instance FFL.FirstOrder.Theory.Proof.instAxiomatizedSentence {L : Language} : Entailment.Axiomatized (Theory L)

Equations

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

noncomputable def FFL.FirstOrder.Theory.Proof.cut {L : Language} {T : Theory L} {φ : Sentence L} {U : Theory L} (h : T ⊢!* U) (b : U ⊢! φ) : T ⊢! φ

Replaces each used axiom by its proof in another theory. This is a routine consequence of implication introduction and modus ponens.

Equations

• FFL.FirstOrder.Theory.Proof.cut h b = FFL.FirstOrder.Theory.Proof.cut.go h b.axioms.toList ⋯ (FFL.OneSidedLK.cast b.derivation ⋯)

noncomputable def FFL.FirstOrder.Theory.Proof.cut.go {L : Language} {T U : Theory L} (h : T ⊢!* U) (l : List (Sentence L)) (hl : ∀ ψ ∈ l, ψ ∈ U) {φ : Sentence L} (d : OneSidedLK.Pullback LK.Derivation Rewriting.emb (⦃φ⦄ + ∼↑l)) : T ⊢! φ

Equations

• FFL.FirstOrder.Theory.Proof.cut.go h [] hl_2 d_2 = FFL.FirstOrder.Theory.Proof.ofDerivation (FFL.OneSidedLK.cast d_2 ⋯)
• FFL.FirstOrder.Theory.Proof.cut.go h (ψ :: l_2) hl_2 d_2 = FFL.FirstOrder.Theory.Proof.cut.go h l_2 ⋯ (FFL.OneSidedLK.cast (FFL.OneSidedLK.or (FFL.OneSidedLK.cast d_2 ⋯)) ⋯)⨀!h ⋯

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Theory.Proof.instStrongCutSentence {L : Language} : Entailment.StrongCut (Theory L) (Theory L)

Equations

• FFL.FirstOrder.Theory.Proof.instStrongCutSentence = { cut := fun {𝓢 𝓣 : FFL.FirstOrder.Theory L} {φ : FFL.FirstOrder.Sentence L} => FFL.FirstOrder.Theory.Proof.cut }

@[instance_reducible]

instance FFL.FirstOrder.Theory.Proof.instDeductiveExplosionSentence {L : Language} : Entailment.DeductiveExplosion (Theory L)

Equations

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

theorem FFL.FirstOrder.Theory.Proof.weakerThan_of_le {L : Language} {T U : Theory L} (h : T ⊆ U) : T ⪯ U

instance FFL.FirstOrder.Theory.Proof.instWeakerThanSentenceUnion {L : Language} (T U : Theory L) : T ⪯ T ∪ U

instance FFL.FirstOrder.Theory.Proof.instWeakerThanSentenceUnion_1 {L : Language} (T U : Theory L) : U ⪯ T ∪ U

theorem FFL.FirstOrder.Theory.Proof.provable_iff {L : Language} {T : Theory L} {φ : Sentence L} : T ⊢ φ ↔ ∃ (Γ : Multiset (Sentence L)), (∀ ψ ∈ Γ, ψ ∈ T) ∧ Nonempty (⊢ᴸᴷ¹ ⦃Rewriting.emb φ⦄ + ∼LK.Sequent.embed Γ)

theorem FFL.FirstOrder.Theory.Proof.inconsistent_iff {L : Language} {T : Theory L} : Entailment.Inconsistent T ↔ ∃ (Γ : Multiset (Sentence L)), (∀ ψ ∈ Γ, ψ ∈ T) ∧ Nonempty (⊢ᴸᴷ¹ ∼LK.Sequent.embed Γ)

@[simp]

theorem FFL.FirstOrder.Theory.Proof.empty_provable_iff_eprovable {L : Language} {φ : Sentence L} : ∅ ⊢ φ ↔ 𝐋𝐊¹ ⊢ Rewriting.emb φ

theorem FFL.FirstOrder.Theory.Proof.of_LK_provable {L : Language} {T : Theory L} {φ : Sentence L} : 𝐋𝐊¹ ⊢ Rewriting.emb φ → T ⊢ φ

theorem FFL.FirstOrder.Theory.Proof.specialize {L : Language} {T : Theory L} (φ : Semisentence L 1) (t : ClosedTerm L) : T ⊢ ∀¹ φ 🡒 Semiformula.subst φ ![t]

@[instance_reducible]

noncomputable instance FFL.FirstOrder.Theory.Proof.instDeductionSentence {L : Language} : Entailment.Deduction (Theory L)

Equations

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

Theory

def FFL.FirstOrder.Theory.theory {L : Language} (T : Theory L) : Theory L

Equations

• T.theory = {σ : FFL.FirstOrder.Sentence L | T ⊢ σ}

@[simp]

theorem FFL.FirstOrder.Theory.mem_theory {L : Language} {σ : Sentence L} {T : Theory L} : σ ∈ T.theory ↔ T ⊢ σ