Supporting results for pointwise provable equality.

One-sided sequent calculus for first-order classical logic

@[reducible, inline]

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

The Sequent construction in FFL.FirstOrder.LK.

Equations

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

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

The new Var construction in FFL.FirstOrder.LK.Sequent.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.LK.Sequent.not_hasFreeVariable_newVar {L : Language} {φ : Proposition L} {Γ : Sequent L} (h : φ ∈ Γ) : ¬Semiformula.HasFreeVariable φ Γ.newVar

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

The Is Closed construction in FFL.FirstOrder.LK.Sequent.

Equations

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

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

The embed construction in FFL.FirstOrder.LK.Sequent.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Derivation for $\mathbf{LK}$

inductive PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.«term⊢ᴸᴷ¹_» : Lean.ParserDescr

The «term⊢ᴸᴷ¹ » construction in FFL.FirstOrder.

Equations

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

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

The height construction in FFL.FirstOrder.LK.Derivation.

Equations

• (PointwiseComposition.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
• PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.height_contraction {L : Language} {Γ : Sequent L} {φ : Proposition L} (d : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃φ⦄)) : d.contraction.height = d.height.succ

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.height_or {L : Language} {Γ : Sequent L} {φ ψ : Proposition L} (d : ⊢ᴸᴷ¹ Γ + (⦃φ⦄ + ⦃ψ⦄)) : d.or.height = d.height.succ

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.cast {L : Language} {Γ Δ : Sequent L} (d : ⊢ᴸᴷ¹ Δ) (e : Δ = Γ := by abel) : ⊢ᴸᴷ¹ Γ

The cast construction in FFL.FirstOrder.LK.Derivation.

Equations

• d.cast e = e ▸ d

@[simp]

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

@[instance_reducible]

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

Equations

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

def PointwiseComposition.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.
• (dp.cut dn).traversal = dp.traversal.remove.add dn.traversal.remove
• d.contraction.traversal = (PointwiseComposition.Multiset.Traversal.cast ⋯ d.traversal).remove
• d.weakening.traversal = PointwiseComposition.Multiset.Traversal.succ φ d.traversal
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.verum.traversal = PointwiseComposition.Multiset.Traversal.atom ⊤
• d.or.traversal = PointwiseComposition.Multiset.Traversal.succ (φ ⋎ ψ) (PointwiseComposition.Multiset.Traversal.cast ⋯ d.traversal).remove.remove
• (dp.and dq).traversal = PointwiseComposition.Multiset.Traversal.succ (φ ⋏ ψ) dp.traversal.remove
• d.exs.traversal = PointwiseComposition.Multiset.Traversal.succ (∃¹ φ) d.traversal.remove

def PointwiseComposition.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 = PointwiseComposition.FFL.Structural.ofSubset d.traversal t d h

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

The tensor construction in FFL.FirstOrder.LK.Derivation.

Equations

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

@[irreducible]

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

The eta construction in FFL.FirstOrder.LK.Derivation.

Equations

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

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.instCutProposition {L : Language} : OneSidedLK.Cut Derivation

Equations

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

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

def PointwiseComposition.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) Γ

The rewrite construction in FFL.FirstOrder.LK.Derivation.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f d.contraction = ((PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f d).cast ⋯).contraction.cast ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f d.weakening = (PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f d).weakening.cast ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f PointwiseComposition.FFL.FirstOrder.LK.Derivation.verum = PointwiseComposition.FFL.FirstOrder.LK.Derivation.verum
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f d.or = ((PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f d).cast ⋯).or.cast ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f d.exs = ((PointwiseComposition.FFL.FirstOrder.LK.Derivation.rewrite f d).cast ⋯).exs.cast ⋯

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

The map construction in FFL.FirstOrder.LK.Derivation.

Equations

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

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

The shift construction in FFL.FirstOrder.LK.Derivation.

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap {L₁ : Language} {L₂ : Language} (Φ : L₁.Hom L₂) {Γ : Sequent L₁} : ⊢ᴸᴷ¹ Γ → ⊢ᴸᴷ¹ Multiset.map (⇑(Semiformula.lMap Φ)) Γ

The l Map construction in FFL.FirstOrder.LK.Derivation.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d.contraction = ((PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d).cast ⋯).contraction.cast ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d.weakening = (PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d).weakening.cast ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ PointwiseComposition.FFL.FirstOrder.LK.Derivation.verum = ⋯.mpr PointwiseComposition.FFL.FirstOrder.LK.Derivation.verum
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d.or = ((PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d).cast ⋯).or.cast ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d.all = ((PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d).cast ⋯).all.cast ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d.exs = ((PointwiseComposition.FFL.FirstOrder.LK.Derivation.lMap Φ d).cast ⋯).exs.cast ⋯

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

The generalize By New Var construction in FFL.FirstOrder.LK.Derivation.

Equations

• PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.LK (L : Language) : Type

Data and laws for LK in FFL.FirstOrder.

• symbol {L : Language} : LK L

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

The «term𝐋𝐊¹» construction in FFL.FirstOrder.

Equations

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

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

The «term𝐋𝐊¹[ ]» construction in FFL.FirstOrder.

Equations

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

@[reducible, inline]

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

The Proof construction in FFL.FirstOrder.LK.

Equations

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

@[instance_reducible]

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

Equations

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

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

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

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

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

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

Data and laws for Proof in FFL.FirstOrder.Theory.

• axioms : Multiset (Sentence L)

  The axioms construction in FFL.FirstOrder.Theory.Proof.

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

  The derivation construction in FFL.FirstOrder.Theory.Proof.

@[instance_reducible]

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

Equations

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

def PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Theory.Proof.instClSentence {L : Language} {T : Theory L} : Entailment.Cl T

Equations

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

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.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

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

noncomputable def PointwiseComposition.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 ⊢! φ

The go construction in FFL.FirstOrder.Theory.Proof.cut.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Theory.Proof.cut.go h [] hl_2 d_2 = PointwiseComposition.FFL.FirstOrder.Theory.Proof.ofDerivation (PointwiseComposition.FFL.OneSidedLK.cast d_2 ⋯)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Theory.Proof.weakerThan_of_le {L : Language} {T U : Theory L} (h : T ⊆ U) : T ≼ U

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

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

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

@[simp]

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

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

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

@[instance_reducible]

noncomputable instance PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Theory.theory {L : Language} (T : Theory L) : Theory L

The theory construction in FFL.FirstOrder.Theory.

Equations

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

@[simp]

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