One-sided sequent calculus for first-order classical logic

@[reducible, inline]

abbrev LO.FirstOrder.Sequent (L : Language) : Type u_1

Equations

• LO.FirstOrder.Sequent L = List (LO.FirstOrder.Proposition L)

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

Equations

• Γ.newVar = List.foldr max 0 (List.map LO.FirstOrder.Semiformula.fvSup Γ)

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

@[simp]

theorem LO.FirstOrder.Sequent.lcHom_comm {L : Language} {ξ : Type u_1} {Γ : List (Formula L ξ)} (f : Formula L ξ →ˡᶜ Proposition L) : List.map (⇑f) (∼Γ) = ∼List.map (⇑f) Γ

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

Equations

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

def LO.FirstOrder.Sequent.embed {L : Language} (Γ : List (Sentence L)) : Sequent L

Equations

• LO.FirstOrder.Sequent.embed Γ = List.map (⇑LO.FirstOrder.Rewriting.emb) Γ

@[simp]

theorem LO.FirstOrder.Sequent.embed_nil {L : Language} : embed [] = []

@[simp]

theorem LO.FirstOrder.Sequent.embed_cons {L : Language} {φ : Sentence L} {Γ : List (Sentence L)} : embed (φ :: Γ) = Rewriting.emb φ :: embed Γ

@[simp]

theorem LO.FirstOrder.Sequent.embed_append {L : Language} (Γ Δ : List (Sentence L)) : embed (Γ ++ Δ) = embed Γ ++ embed Δ

@[simp]

theorem LO.FirstOrder.Sequent.embed_shift {L : Language} (Γ : List (Sentence L)) : Rewriting.shifts (embed Γ) = embed Γ

Derivation for one-sided $\mathbf{LK}$

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

Derivation for one-sided $\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} {φ : Proposition L} {Γ Δ : List (Proposition L)} : ⊢ᴸᴷ¹ φ :: Γ → ⊢ᴸᴷ¹ ∼φ :: Δ → ⊢ᴸᴷ¹ Γ ++ Δ
• contraction {L : Language} {Δ Γ : Sequent L} : ⊢ᴸᴷ¹ Δ → Δ ⊆ Γ → ⊢ᴸᴷ¹ Γ
• verum {L : Language} : ⊢ᴸᴷ¹ [⊤]
• or {L : Language} {φ ψ : Proposition L} {Γ : List (Proposition L)} : ⊢ᴸᴷ¹ φ :: ψ :: Γ → ⊢ᴸᴷ¹ φ ⋎ ψ :: Γ
• and {L : Language} {φ : Proposition L} {Γ : List (Proposition L)} {ψ : Proposition L} : ⊢ᴸᴷ¹ φ :: Γ → ⊢ᴸᴷ¹ ψ :: Γ → ⊢ᴸᴷ¹ φ ⋏ ψ :: Γ
• all {L : Language} {Γ : List (Semiproposition L 0)} {φ : Semiproposition L (0 + 1)} : ⊢ᴸᴷ¹ Semiformula.free φ :: Rewriting.shifts Γ → ⊢ᴸᴷ¹ (∀⁰ φ) :: Γ
• exs {L : Language} {φ : Semiproposition L (Nat.succ 0)} {t : Semiterm L ℕ 0} {Γ : List (Proposition L)} : ⊢ᴸᴷ¹ φ/[t] :: Γ → ⊢ᴸᴷ¹ (∃⁰ φ) :: Γ

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

Equations

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

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

Equations

• (LO.FirstOrder.Derivation.identity r v).height = 0
• (dp.cut dn).height = max dp.height dn.height + 1
• (d.contraction a).height = d.height + 1
• LO.FirstOrder.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 LO.FirstOrder.Derivation.height_id {L : Language} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ℕ 0} : (identity r v).height = 0

@[simp]

theorem LO.FirstOrder.Derivation.height_cut {L✝ : Language} {Δ : List (Proposition L✝)} {φ : Proposition L✝} (dp : ⊢ᴸᴷ¹ φ :: Δ) (dn : ⊢ᴸᴷ¹ ∼φ :: Δ) : (dp.cut dn).height = (max dp.height dn.height).succ

@[simp]

theorem LO.FirstOrder.Derivation.height_contraction {L✝ : Language} {Δ Γ : Sequent L✝} (d : ⊢ᴸᴷ¹ Δ) (h : Δ ⊆ Γ) : (d.contraction h).height = d.height.succ

@[simp]

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

@[simp]

theorem LO.FirstOrder.Derivation.height_and {L✝ : Language} {Δ : List (Proposition L✝)} {φ ψ : Proposition L✝} (dp : ⊢ᴸᴷ¹ φ :: Δ) (dq : ⊢ᴸᴷ¹ ψ :: Δ) : (dp.and dq).height = (max dp.height dq.height).succ

@[simp]

theorem LO.FirstOrder.Derivation.height_or {L✝ : Language} {Δ : List (Proposition L✝)} {φ ψ : Proposition L✝} (d : ⊢ᴸᴷ¹ φ :: ψ :: Δ) : d.or.height = d.height.succ

@[simp]

theorem LO.FirstOrder.Derivation.height_all {L : Language} {Δ : List (Semiproposition L 0)} {φ : Semiproposition L 1} (d : ⊢ᴸᴷ¹ Semiformula.free φ :: Rewriting.shifts Δ) : d.all.height = d.height.succ

@[simp]

theorem LO.FirstOrder.Derivation.height_exs {L✝ : Language} {Δ : List (Proposition L✝)} {t : Semiterm L✝ ℕ 0} {φ : Semiproposition L✝ (Nat.succ 0)} (d : ⊢ᴸᴷ¹ φ/[t] :: Δ) : d.exs.height = d.height.succ

@[reducible, inline]

abbrev LO.FirstOrder.Derivation.cast {L✝ : Language} {Δ Γ : Sequent L✝} (d : ⊢ᴸᴷ¹ Δ) (e : Δ = Γ := by simp) : ⊢ᴸᴷ¹ Γ

Equations

• d.cast e = e ▸ d

@[simp]

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

def LO.FirstOrder.Derivation.contra {L✝ : Language} {Δ Γ : Sequent L✝} (d : ⊢ᴸᴷ¹ Δ) (h : Δ ⊆ Γ := by simp) : ⊢ᴸᴷ¹ Γ

Equations

• d.contra h = d.contraction h

def LO.FirstOrder.Derivation.top {L✝ : Language} {Δ : Sequent L✝} (h : ⊤ ∈ Δ := by simp) : ⊢ᴸᴷ¹ Δ

Equations

• LO.FirstOrder.Derivation.top h = LO.FirstOrder.Derivation.verum.contraction ⋯

def LO.FirstOrder.Derivation.identity' {L : Language} {k : ℕ} {Δ : Sequent L} (r : L.Rel k) (v : Fin k → Semiterm L ℕ 0) (hpos : Semiformula.rel r v ∈ Δ := by simp) (hneg : Semiformula.nrel r v ∈ Δ := by simp) : ⊢ᴸᴷ¹ Δ

Equations

• LO.FirstOrder.Derivation.identity' r v hpos hneg = (LO.FirstOrder.Derivation.identity r v).contraction ⋯

def LO.FirstOrder.Derivation.tensor {L✝ : Language} {Γ Δ : List (Proposition L✝)} {φ ψ : Proposition L✝} (dφ : ⊢ᴸᴷ¹ φ :: Γ) (dψ : ⊢ᴸᴷ¹ ψ :: Δ) : ⊢ᴸᴷ¹ φ ⋏ ψ :: (Γ ++ Δ)

Equations

• dφ.tensor dψ = (dφ.contra ⋯).and (dψ.contra ⋯)

def LO.FirstOrder.Derivation.rotate {L✝ : Language} {φ : Proposition L✝} {Γ : List (Proposition L✝)} (d : ⊢ᴸᴷ¹ φ :: Γ) : ⊢ᴸᴷ¹ Γ ++ [φ]

Equations

• d.rotate = d.contra ⋯

@[irreducible]

def LO.FirstOrder.Derivation.eta {L : Language} (φ : Proposition L) : ⊢ᴸᴷ¹ [φ, ∼φ]

Equations

• LO.FirstOrder.Derivation.eta (LO.FirstOrder.Semiformula.rel R v) = LO.FirstOrder.Derivation.identity' R v ⋯ ⋯
• LO.FirstOrder.Derivation.eta (LO.FirstOrder.Semiformula.nrel R v) = LO.FirstOrder.Derivation.identity' R v ⋯ ⋯
• LO.FirstOrder.Derivation.eta LO.FirstOrder.Semiformula.verum = LO.FirstOrder.Derivation.top ⋯
• LO.FirstOrder.Derivation.eta LO.FirstOrder.Semiformula.falsum = LO.FirstOrder.Derivation.top ⋯
• LO.FirstOrder.Derivation.eta (LO.FirstOrder.Semiformula.and φ ψ) = ((LO.FirstOrder.Derivation.eta φ).tensor (LO.FirstOrder.Derivation.eta ψ)).rotate.or.rotate
• LO.FirstOrder.Derivation.eta (LO.FirstOrder.Semiformula.or φ ψ) = ((LO.FirstOrder.Derivation.eta φ).rotate.tensor (LO.FirstOrder.Derivation.eta ψ).rotate).rotate.or
• LO.FirstOrder.Derivation.eta (LO.FirstOrder.Semiformula.all φ) = (((LO.FirstOrder.Derivation.eta (LO.FirstOrder.Semiformula.free φ)).rotate.cast ⋯).exs.rotate.cast ⋯).all
• LO.FirstOrder.Derivation.eta (LO.FirstOrder.Semiformula.exs φ) = (((LO.FirstOrder.Derivation.eta (LO.FirstOrder.Semiformula.free φ)).cast ⋯).exs.rotate.cast ⋯).all.rotate

def LO.FirstOrder.Derivation.close {L : Language} {Δ : Sequent L} (φ : Proposition L) (hp : φ ∈ Δ := by simp) (hn : ∼φ ∈ Δ := by simp) : ⊢ᴸᴷ¹ Δ

Equations

• LO.FirstOrder.Derivation.close φ hp hn = (LO.FirstOrder.Derivation.eta φ).contra ⋯

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

@[implicit_reducible]

instance LO.FirstOrder.Derivation.instOneSidedLKProposition {L : Language} : OneSidedLK Derivation

Equations

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

@[implicit_reducible]

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

Equations

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

def LO.FirstOrder.Derivation.rewrite {L : Language} {Γ : Sequent L} (f : ℕ → SyntacticTerm L) : ⊢ᴸᴷ¹ Γ → ⊢ᴸᴷ¹ List.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.
• LO.FirstOrder.Derivation.rewrite f (LO.FirstOrder.Derivation.identity r v) = LO.FirstOrder.Derivation.identity r (⇑(LO.FirstOrder.Rew.rewrite f) ∘ v)
• LO.FirstOrder.Derivation.rewrite f (dp.cut dn) = (((LO.FirstOrder.Derivation.rewrite f dp).cast ⋯).cut ((LO.FirstOrder.Derivation.rewrite f dn).cast ⋯)).cast ⋯
• LO.FirstOrder.Derivation.rewrite f (d.contraction a) = (LO.FirstOrder.Derivation.rewrite f d).contraction ⋯
• LO.FirstOrder.Derivation.rewrite f LO.FirstOrder.Derivation.verum = LO.FirstOrder.Derivation.verum
• LO.FirstOrder.Derivation.rewrite f d.or = (LO.FirstOrder.Derivation.rewrite f d).or
• LO.FirstOrder.Derivation.rewrite f (dp.and dq) = (LO.FirstOrder.Derivation.rewrite f dp).and (LO.FirstOrder.Derivation.rewrite f dq)
• LO.FirstOrder.Derivation.rewrite f d.exs = ((LO.FirstOrder.Derivation.rewrite f d).cast ⋯).exs.cast ⋯

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

Equations

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

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

Equations

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

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

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

Equations

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

def LO.FirstOrder.Derivation.genelalizeByNewver {L : Language} {m : ℕ} {Δ : List (Proposition L)} {φ : Semiproposition L 1} (hp : ¬Semiformula.FVar? φ m) (hΔ : ∀ ψ ∈ Δ, ¬Semiformula.FVar? ψ m) (d : ⊢ᴸᴷ¹ φ/[Semiterm.fvar m] :: Δ) : ⊢ᴸᴷ¹ (∀⁰ φ) :: Δ

Equations

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

def LO.FirstOrder.Derivation.exOfInstances {L : Language} {Γ : List (Proposition L)} (v : List (SyntacticTerm L)) (φ : Semiproposition L 1) (h : ⊢ᴸᴷ¹ List.map (fun (x : Semiterm L ℕ 0) => φ/[x]) v ++ Γ) : ⊢ᴸᴷ¹ (∃⁰ φ) :: Γ

Equations

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

def LO.FirstOrder.Derivation.exOfInstances' {L : Language} {Γ : List (Proposition L)} (v : List (SyntacticTerm L)) (φ : Semiproposition L 1) (h : ⊢ᴸᴷ¹ (∃⁰ φ) :: List.map (fun (x : Semiterm L ℕ 0) => φ/[x]) v ++ Γ) : ⊢ᴸᴷ¹ (∃⁰ φ) :: Γ

Equations

• LO.FirstOrder.Derivation.exOfInstances' v φ h = (LO.FirstOrder.Derivation.exOfInstances v φ (h.contraction ⋯)).contraction ⋯

def LO.FirstOrder.Derivation.allNvar {L : Language} {Δ : Sequent L} {φ : Semiproposition L (0 + 1)} (h : ∀⁰ φ ∈ Δ) : ⊢ᴸᴷ¹ φ/[Semiterm.fvar Δ.newVar] :: Δ → ⊢ᴸᴷ¹ Δ

Equations

• LO.FirstOrder.Derivation.allNvar h b = (LO.FirstOrder.Derivation.genelalizeByNewver ⋯ ⋯ b).contraction ⋯

Classical proof system

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

• symbol {L : Language} : LK L

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

• LO.FirstOrder.LK.Proof φ = (⊢ᴸᴷ¹ [φ])

@[implicit_reducible]

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

Equations

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

theorem LO.FirstOrder.LK.Proof.def_eq {L : Language} (φ : Proposition L) : (𝐋𝐊¹ ⊢! φ) = (⊢ᴸᴷ¹ [φ])

theorem LO.FirstOrder.LK.Proof.provable_def {L : Language} (φ : Proposition L) : 𝐋𝐊¹ ⊢ φ ↔ Nonempty (⊢ᴸᴷ¹ [φ])

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

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

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

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

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

• axioms : List (Sentence L)
• axioms_mem (ψ : Sentence L) : ψ ∈ self.axioms → ψ ∈ T
• derivation : OneSidedLK.Pullback Derivation Rewriting.emb (σ :: ∼self.axioms)

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Theory.Proof.instContextualEntailmentSemiformulaEmptyOfNatNatPullbackPropositionDerivationEmbSemiproposition {L : Language} : OneSidedLK.ContextualEntailment (OneSidedLK.Pullback Derivation Rewriting.emb) (Theory L)

Equations

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

@[implicit_reducible]

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

Equations

• LO.FirstOrder.Theory.Proof.instClSentence = LO.OneSidedLK.ContextualEntailment.cl T

@[implicit_reducible]

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

Equations

• LO.FirstOrder.Theory.Proof.instAxiomatizedSentence = inferInstance

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

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

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

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

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

@[simp]

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

theorem LO.FirstOrder.Theory.Proof.iff_context {L : Language} {φ : Sentence L} {T : Theory L} : T ⊢ φ ↔ T *⊢[Entailment.pullback 𝐋𝐊¹ ⇑Rewriting.emb] φ

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

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

@[implicit_reducible]

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

Equations

• LO.FirstOrder.Theory.Proof.instDeductionSentence = LO.OneSidedLK.ContextualEntailment.deduction (LO.Entailment.pullback 𝐋𝐊¹ ⇑LO.FirstOrder.Rewriting.emb)

Theory

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

Equations

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

@[simp]

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