Hauptsatz of classical first-order logic

Main reference: Jeremy Avigad, Algebraic proofs of cut elimination [Avi01]

inductive FFL.FirstOrder.LK.Derivation.Positive {L : Language} (Ξ : Sequent L) : Sequent L → Type u_1

• refl {L : Language} {Ξ : Sequent L} : Ξ ⟶⁺ Ξ
• weakening {L : Language} {Ξ Γ : Sequent L} {φ : Proposition L} : Ξ ⟶⁺ Γ → Ξ ⟶⁺ Γ + ⦃φ⦄
• contraction {L : Language} {Ξ : Sequent L} {Γ : Multiset (Proposition L)} {φ : Proposition L} : Ξ ⟶⁺ Γ + (⦃φ⦄ + ⦃φ⦄) → Ξ ⟶⁺ Γ + ⦃φ⦄
• or {L : Language} {Ξ : Sequent L} {Γ : Multiset (Proposition L)} {φ ψ : Proposition L} : Ξ ⟶⁺ Γ + (⦃φ⦄ + ⦃ψ⦄) → Ξ ⟶⁺ Γ + ⦃φ ⋎ ψ⦄
• exs {L : Language} {Ξ : Sequent L} {Γ : Multiset (Semiproposition L 0)} {φ : Semiproposition L (Nat.succ 0)} {t : Semiterm L ℕ 0} : Ξ ⟶⁺ Γ + ⦃φ/[t]⦄ → Ξ ⟶⁺ Γ + ⦃∃¹ φ⦄

def FFL.FirstOrder.LK.Derivation.«term_⟶⁺_» : Lean.TrailingParserDescr

Equations

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

def FFL.FirstOrder.LK.Derivation.Positive.traversal {L : Language} {Ξ : Sequent L} [L.DecidableEq] {Γ : Sequent L} : Ξ ⟶⁺ Γ → Multiset.Traversal Ξ → Multiset.Traversal Γ

Equations

• FFL.FirstOrder.LK.Derivation.Positive.refl.traversal x✝ = x✝
• d.weakening.traversal x✝ = Multiset.Traversal.succ φ (d.traversal x✝)
• d.contraction.traversal x✝ = (Multiset.Traversal.cast ⋯ (d.traversal x✝)).remove
• d.or.traversal x✝ = Multiset.Traversal.succ (φ ⋎ ψ) (Multiset.Traversal.cast ⋯ (d.traversal x✝)).remove.remove
• d.exs.traversal x✝ = Multiset.Traversal.succ (∃¹ φ) (d.traversal x✝).remove

@[instance_reducible]

instance FFL.FirstOrder.LK.Derivation.Positive.instStructuralProposition {L : Language} {Ξ : Sequent L} : Structural (Positive Ξ)

Equations

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

def FFL.FirstOrder.LK.Derivation.Positive.ofSubset {L : Language} {Ξ Γ : Sequent L} [L.DecidableEq] (tΞ : Multiset.Traversal Ξ) (tΓ : Multiset.Traversal Γ) (ss : Ξ ⊆ Γ) : Ξ ⟶⁺ Γ

Equations

• FFL.FirstOrder.LK.Derivation.Positive.ofSubset tΞ tΓ ss = FFL.Structural.ofSubset tΞ tΓ FFL.FirstOrder.LK.Derivation.Positive.refl ss

def FFL.FirstOrder.LK.Derivation.Positive.trans {L : Language} {Ξ Γ Δ : Sequent L} : Ξ ⟶⁺ Γ → Γ ⟶⁺ Δ → Ξ ⟶⁺ Δ

Equations

• x✝.trans d.or = (x✝.trans d).or
• x✝.trans d.exs = (x✝.trans d).exs
• x✝.trans d.weakening = (x✝.trans d).weakening
• x✝.trans d.contraction = (x✝.trans d).contraction
• x✝.trans FFL.FirstOrder.LK.Derivation.Positive.refl = x✝

def FFL.FirstOrder.LK.Derivation.Positive.cast {L : Language} {Ξ Γ Ξ' Γ' : Sequent L} (d : Ξ ⟶⁺ Γ) (hΞ : Ξ = Ξ' := by abel) (hΓ : Γ = Γ' := by abel) : Ξ' ⟶⁺ Γ'

Equations

• d.cast hΞ hΓ = hΞ ▸ hΓ ▸ d

def FFL.FirstOrder.LK.Derivation.Positive.addLeft {L : Language} {Ξ : Sequent L} (Δ : Sequent L) {Γ : Sequent L} : Ξ ⟶⁺ Γ → Δ + Ξ ⟶⁺ Δ + Γ

Equations

• FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ d.or = ((FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ d).cast ⋯ ⋯).or.cast ⋯ ⋯
• FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ d.exs = ((FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ d).cast ⋯ ⋯).exs.cast ⋯ ⋯
• FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ d.weakening = (FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ d).weakening.cast ⋯ ⋯
• FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ d.contraction = ((FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ d).cast ⋯ ⋯).contraction.cast ⋯ ⋯
• FFL.FirstOrder.LK.Derivation.Positive.addLeft Δ FFL.FirstOrder.LK.Derivation.Positive.refl = FFL.FirstOrder.LK.Derivation.Positive.refl

def FFL.FirstOrder.LK.Derivation.Positive.cons {L : Language} {Ξ Γ : Sequent L} (φ : Proposition L) (d : Ξ ⟶⁺ Γ) : Ξ + ⦃φ⦄ ⟶⁺ Γ + ⦃φ⦄

Equations

• FFL.FirstOrder.LK.Derivation.Positive.cons φ d = (FFL.FirstOrder.LK.Derivation.Positive.addLeft ⦃φ⦄ d).cast ⋯ ⋯

def FFL.FirstOrder.LK.Derivation.Positive.add {L : Language} {Γ Δ Ξ Θ : Sequent L} (d : Γ ⟶⁺ Δ) (b : Ξ ⟶⁺ Θ) : Γ + Ξ ⟶⁺ Δ + Θ

Equations

• d.add b = (FFL.FirstOrder.LK.Derivation.Positive.addLeft Γ b).trans ((FFL.FirstOrder.LK.Derivation.Positive.addLeft Θ d).cast ⋯ ⋯)

def FFL.FirstOrder.LK.Derivation.Positive.graft {L : Language} {Ξ Γ : Sequent L} (b : ⊢ᴸᴷ¹ Ξ) : Ξ ⟶⁺ Γ → ⊢ᴸᴷ¹ Γ

Equations

• FFL.FirstOrder.LK.Derivation.Positive.graft b d.or = (FFL.FirstOrder.LK.Derivation.Positive.graft b d).or
• FFL.FirstOrder.LK.Derivation.Positive.graft b d.exs = (FFL.FirstOrder.LK.Derivation.Positive.graft b d).exs
• FFL.FirstOrder.LK.Derivation.Positive.graft b d.weakening = (FFL.FirstOrder.LK.Derivation.Positive.graft b d).weakening
• FFL.FirstOrder.LK.Derivation.Positive.graft b d.contraction = (FFL.FirstOrder.LK.Derivation.Positive.graft b d).contraction
• FFL.FirstOrder.LK.Derivation.Positive.graft b FFL.FirstOrder.LK.Derivation.Positive.refl = b

theorem FFL.FirstOrder.LK.Derivation.Positive.graft_isCutFree_of_isCutFree {L : Language} {Ξ Γ : Sequent L} {b : ⊢ᴸᴷ¹ Ξ} {d : Ξ ⟶⁺ Γ} (hb : b.IsCutFree) : (graft b d).IsCutFree

structure FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan {L : Language} (q p : Sequent L) : Type u_1

• val : ∼p ⟶⁺ ∼q

def FFL.FirstOrder.Derivation.Canonical.«term_≼_» : Lean.TrailingParserDescr

Equations

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

@[instance_reducible]

def FFL.FirstOrder.LK.Derivation.Canonical.instMinSequent {L : Language} : Min (Sequent L)

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.instMinSequent = { min := fun (p q : FFL.FirstOrder.LK.Sequent L) => p + q }

theorem FFL.FirstOrder.LK.Derivation.Canonical.inf_def {L : Language} (p q : Sequent L) : p ⊓ q = p + q

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.neg_inf_p_eq {L : Language} (p q : Sequent L) : ∼(p ⊓ q) = ∼p ⊓ ∼q

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.refl {L : Language} (p : Sequent L) : StrongerThan p p

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.refl p = { val := FFL.FirstOrder.LK.Derivation.Positive.refl }

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.trans {L : Language} {r q p : Sequent L} (srq : StrongerThan r q) (sqp : StrongerThan q p) : StrongerThan r p

Equations

• srq.trans sqp = { val := sqp.val.trans srq.val }

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.ofSubset {L : Language} [L.DecidableEq] {q p : Sequent L} (tp : Multiset.Traversal (∼p)) (tq : Multiset.Traversal (∼q)) (h : q ⊇ p) : StrongerThan q p

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.ofSubset tp tq h = { val := FFL.FirstOrder.LK.Derivation.Positive.ofSubset tp tq ⋯ }

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.K_left {L : Language} {p : Sequent L} (φ ψ : Proposition L) : StrongerThan (p + ⦃φ ⋏ ψ⦄) (p + ⦃φ⦄)

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.K_left φ ψ = { val := (FFL.FirstOrder.LK.Derivation.Positive.refl.weakening.cast ⋯ ⋯).or.cast ⋯ ⋯ }

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.K_right {L : Language} {p : Sequent L} (φ ψ : Proposition L) : StrongerThan (p + ⦃φ ⋏ ψ⦄) (p + ⦃ψ⦄)

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.K_right φ ψ = { val := (FFL.FirstOrder.LK.Derivation.Positive.refl.weakening.cast ⋯ ⋯).or.cast ⋯ ⋯ }

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.all {L : Language} {p : Sequent L} (φ : Semiproposition L 1) (t : Semiterm L ℕ 0) : StrongerThan (p + ⦃∀¹ φ⦄) (p + ⦃φ/[t]⦄)

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.all φ t = { val := FFL.FirstOrder.LK.Derivation.Positive.refl.exs.cast ⋯ ⋯ }

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.minLeLeft {L : Language} (p q : Sequent L) (tq : Multiset.Traversal (∼q)) : StrongerThan (p ⊓ q) p

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.minLeLeft p q tq = { val := (FFL.Structural.weakenMany tq FFL.FirstOrder.LK.Derivation.Positive.refl).cast ⋯ ⋯ }

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.minLeRight {L : Language} (p q : Sequent L) (tp : Multiset.Traversal (∼p)) : StrongerThan (p ⊓ q) q

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.minLeRight p q tp = { val := (FFL.Structural.weakenMany tp FFL.FirstOrder.LK.Derivation.Positive.refl).cast ⋯ ⋯ }

def FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.leMinRightOfLe {L : Language} {p q : Sequent L} (s : StrongerThan q p) (tq : Multiset.Traversal (∼q)) : StrongerThan q (p ⊓ q)

Equations

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

@[irreducible]

def FFL.FirstOrder.LK.Derivation.Canonical.Forces {L : Language} (p : Sequent L) : Propositionᵢ L → Type u

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.LK.Derivation.Canonical.Forces p FFL.FirstOrder.Semiformulaᵢ.falsum = { b : ⊢ᴸᴷ¹ ∼p // b.IsCutFree }
• FFL.FirstOrder.LK.Derivation.Canonical.Forces p (FFL.FirstOrder.Semiformulaᵢ.rel R v) = { b : ⊢ᴸᴷ¹ ∼p + ⦃FFL.FirstOrder.Semiformula.rel R v⦄ // b.IsCutFree }
• FFL.FirstOrder.LK.Derivation.Canonical.Forces p (FFL.FirstOrder.Semiformulaᵢ.and φ ψ) = (FFL.FirstOrder.LK.Derivation.Canonical.Forces p φ × FFL.FirstOrder.LK.Derivation.Canonical.Forces p ψ)
• FFL.FirstOrder.LK.Derivation.Canonical.Forces p (FFL.FirstOrder.Semiformulaᵢ.or φ ψ) = (FFL.FirstOrder.LK.Derivation.Canonical.Forces p φ ⊕ FFL.FirstOrder.LK.Derivation.Canonical.Forces p ψ)
• FFL.FirstOrder.LK.Derivation.Canonical.Forces p (FFL.FirstOrder.Semiformulaᵢ.all φ) = ((t : FFL.FirstOrder.SyntacticTerm L) → FFL.FirstOrder.LK.Derivation.Canonical.Forces p (φ/[t]))
• FFL.FirstOrder.LK.Derivation.Canonical.Forces p (FFL.FirstOrder.Semiformulaᵢ.exs φ) = ((t : FFL.FirstOrder.SyntacticTerm L) × FFL.FirstOrder.LK.Derivation.Canonical.Forces p (φ/[t]))

@[reducible, inline]

abbrev FFL.FirstOrder.LK.Derivation.Canonical.allForces {L : Language} (φ : Propositionᵢ L) : Type u_1

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.allForces φ = ((p : FFL.FirstOrder.LK.Sequent L) → Multiset.Traversal (∼p) → FFL.FirstOrder.LK.Derivation.Canonical.Forces p φ)

def FFL.FirstOrder.Derivation.Canonical.Forces.«term_⊩_» : Lean.TrailingParserDescr

Equations

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

def FFL.FirstOrder.Derivation.Canonical.Forces.«term⊩_» : Lean.ParserDescr

Equations

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

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.falsumEquiv {L : Language} {p : Sequent L} : Forces p ⊥ ≃ { b : ⊢ᴸᴷ¹ ∼p // b.IsCutFree }

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.falsumEquiv = ⋯.mpr (Equiv.refl { b : ⊢ᴸᴷ¹ ∼p // b.IsCutFree })

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.relEquiv {L : Language} {p : Sequent L} {k : ℕ} {R : L.Rel k} {v : Fin k → Semiterm L ℕ 0} : Forces p (Semiformulaᵢ.rel R v) ≃ { b : ⊢ᴸᴷ¹ ∼p + ⦃Semiformula.rel R v⦄ // b.IsCutFree }

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.relEquiv = ⋯.mpr (Equiv.refl { b : ⊢ᴸᴷ¹ ∼p + ⦃FFL.FirstOrder.Semiformula.rel R v⦄ // b.IsCutFree })

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.andEquiv {L : Language} {p : Sequent L} {φ ψ : Propositionᵢ L} : Forces p (φ ⋏ ψ) ≃ Forces p φ × Forces p ψ

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.andEquiv = ⋯.mpr (Equiv.refl (FFL.FirstOrder.LK.Derivation.Canonical.Forces p φ × FFL.FirstOrder.LK.Derivation.Canonical.Forces p ψ))

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.orEquiv {L : Language} {p : Sequent L} {φ ψ : Propositionᵢ L} : Forces p (φ ⋎ ψ) ≃ Forces p φ ⊕ Forces p ψ

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.orEquiv = ⋯.mpr (Equiv.refl (FFL.FirstOrder.LK.Derivation.Canonical.Forces p φ ⊕ FFL.FirstOrder.LK.Derivation.Canonical.Forces p ψ))

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.implyEquiv {L : Language} {p : Sequent L} {φ ψ : Propositionᵢ L} : Forces p (φ 🡒 ψ) ≃ ((q : Sequent L) → StrongerThan q p → Forces q φ → Forces q ψ)

Equations

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

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.allEquiv {L : Language} {p : Sequent L} {φ : Semipropositionᵢ L (0 + 1)} : Forces p (∀¹ φ) ≃ ((t : SyntacticTerm L) → Forces p (φ/[t]))

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.allEquiv = ⋯.mpr (Equiv.refl ((t : FFL.FirstOrder.SyntacticTerm L) → FFL.FirstOrder.LK.Derivation.Canonical.Forces p (φ/[t])))

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.exsEquiv {L : Language} {p : Sequent L} {φ : Semipropositionᵢ L (0 + 1)} : Forces p (∃¹ φ) ≃ (t : SyntacticTerm L) × Forces p (φ/[t])

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.exsEquiv = ⋯.mpr (Equiv.refl ((t : FFL.FirstOrder.SyntacticTerm L) × FFL.FirstOrder.LK.Derivation.Canonical.Forces p (φ/[t])))

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.cast {L : Language} {φ ψ : Propositionᵢ L} {p : Sequent L} (f : Forces p φ) (s : φ = ψ) : Forces p ψ

Equations

• f.cast s = s ▸ f

@[irreducible]

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.monotone {L : Language} {q p : Sequent L} (s : StrongerThan q p) {φ : Propositionᵢ L} : Forces p φ → Forces q φ

Equations

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

@[irreducible]

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.explosion {L : Language} {p : Sequent L} (b : Forces p ⊥) (φ : Propositionᵢ L) : Forces p φ

Equations

• One or more equations did not get rendered due to their size.
• b.explosion FFL.FirstOrder.Semiformulaᵢ.falsum = b
• b.explosion (FFL.FirstOrder.Semiformulaᵢ.and φ ψ) = FFL.FirstOrder.LK.Derivation.Canonical.Forces.andEquiv.symm (b.explosion φ, b.explosion ψ)
• b.explosion (FFL.FirstOrder.Semiformulaᵢ.or φ ψ) = FFL.FirstOrder.LK.Derivation.Canonical.Forces.orEquiv.symm (Sum.inl (b.explosion φ))
• b.explosion (FFL.FirstOrder.Semiformulaᵢ.all φ) = FFL.FirstOrder.LK.Derivation.Canonical.Forces.allEquiv.symm fun (t : FFL.FirstOrder.SyntacticTerm L) => b.explosion (φ/[t])
• b.explosion (FFL.FirstOrder.Semiformulaᵢ.exs φ) = FFL.FirstOrder.LK.Derivation.Canonical.Forces.exsEquiv.symm ⟨default, b.explosion (φ/[default])⟩

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.implyOf {L : Language} [L.DecidableEq] {p : Sequent L} {φ ψ : Propositionᵢ L} (tp : Multiset.Traversal (∼p)) (b : (q : Sequent L) → Multiset.Traversal (∼q) → Forces q φ → Forces (p ⊓ q) ψ) : Forces p (φ 🡒 ψ)

Equations

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

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.modusPonens {L : Language} {p : Sequent L} {φ ψ : Propositionᵢ L} (f : Forces p (φ 🡒 ψ)) (g : Forces p φ) : Forces p ψ

Equations

• f.modusPonens g = FFL.FirstOrder.LK.Derivation.Canonical.Forces.implyEquiv f p (FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.refl p) g

@[reducible, inline]

abbrev FFL.FirstOrder.LK.Derivation.Canonical.Forces.ContextForces {L : Language} (p : Sequent L) (Γ : LJ.Sequent L) : Type u_1

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.ContextForces p Γ = ((φ : FFL.FirstOrder.Propositionᵢ L) → φ ∈ Γ → FFL.FirstOrder.LK.Derivation.Canonical.Forces p φ)

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.ContextForces.ofSubset {L : Language} {p : Sequent L} {Γ Δ : LJ.Sequent L} (b : ContextForces p Δ) (h : Γ ⊆ Δ) : ContextForces p Γ

Equations

• b.ofSubset h φ hφ = b φ ⋯

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.ContextForces.monotone {L : Language} {p q : Sequent L} {Γ : LJ.Sequent L} (b : ContextForces p Γ) (s : StrongerThan q p) : ContextForces q Γ

Equations

• b.monotone s φ hφ = FFL.FirstOrder.LK.Derivation.Canonical.Forces.monotone s (b φ hφ)

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.ContextForces.cons {L : Language} [L.DecidableEq] {p : Sequent L} {Γ : LJ.Sequent L} {φ : Propositionᵢ L} (b : ContextForces p Γ) (hφ : Forces p φ) : ContextForces p (Γ + ⦃φ⦄)

Extend a forcing assignment by one formula (a routine semantic operation).

Equations

• b.cons hφ ψ hψ = if h : φ = ψ then hφ.cast h else b ψ ⋯

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.HeadForces {L : Language} (p : Sequent L) : LJ.Head L → Type u

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.HeadForces p none = FFL.FirstOrder.LK.Derivation.Canonical.Forces p ⊥
• FFL.FirstOrder.LK.Derivation.Canonical.Forces.HeadForces p (some φ) = FFL.FirstOrder.LK.Derivation.Canonical.Forces p φ

@[irreducible]

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound {L : Language} [L.DecidableEq] {Γ : LJ.Sequent L} {Ξ : LJ.Head L} (d : Γ ⊢ᴸᴶ¹ Ξ) (p : Sequent L) (tp : Multiset.Traversal (∼p)) (b : ContextForces p Γ) : HeadForces p Ξ

Soundness of LJ for the canonical Type-valued forcing interpretation.

• [Avi01, Section 3]

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound (FFL.FirstOrder.LJ.Derivation.identity R v) p tp b_2 = b_2 (FFL.FirstOrder.Semiformulaᵢ.rel R v) ⋯
• FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound d_2.weakening p tp b_2 = FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound d_2 p tp (b_2.ofSubset ⋯)
• FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound FFL.FirstOrder.LJ.Derivation.falsum p tp b_2 = b_2 ⊥ ⋯

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.ljSound {L : Language} [L.DecidableEq] {φ : Propositionᵢ L} (d : 𝐋𝐉¹ ⊢! φ) : allForces φ

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.ljSound d p tp = FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound d p tp fun (x : FFL.FirstOrder.Propositionᵢ L) (h : x ∈ 0) => ⋯.elim

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.relRefl {L : Language} {k : ℕ} (R : L.Rel k) (v : Fin k → SyntacticTerm L) : Forces ⦃Semiformula.rel R v⦄ (Semiformulaᵢ.rel R v)

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.Forces.relRefl R v = FFL.FirstOrder.LK.Derivation.Canonical.Forces.relEquiv.symm ⟨(FFL.FirstOrder.LK.Derivation.identity R v).cast ⋯, ⋯⟩

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.refl.or {L : Language} [L.DecidableEq] {φ ψ : Proposition L} (ihφ : Forces ⦃φ⦄ (Semiformula.doubleNegation φ)) (ihψ : Forces ⦃ψ⦄ (Semiformula.doubleNegation ψ)) : Forces ⦃φ ⋎ ψ⦄ (Semiformula.doubleNegation (φ ⋎ ψ))

Equations

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

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.refl.exs {L : Language} [L.DecidableEq] {φ : Semiproposition L 1} (d : (x : ℕ) → Forces ⦃φ/[Semiterm.fvar x]⦄ φ/[Semiterm.fvar x].doubleNegation) : Forces ⦃∃¹ φ⦄ (∃¹ φ).doubleNegation

Equations

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

@[irreducible]

def FFL.FirstOrder.LK.Derivation.Canonical.Forces.refl {L : Language} [L.DecidableEq] (φ : Proposition L) : Forces ⦃φ⦄ (Semiformula.doubleNegation φ)

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.LK.Derivation.Canonical.Forces.refl FFL.FirstOrder.Semiformula.falsum = FFL.FirstOrder.LK.Derivation.Canonical.Forces.falsumEquiv.symm ⟨FFL.FirstOrder.LK.Derivation.verum, ⋯⟩

def FFL.FirstOrder.LK.Derivation.Canonical.hauptsatz {L : Language} [L.DecidableEq] {Γ : Sequent L} : ⊢ᴸᴷ¹ Γ → { d : ⊢ᴸᴷ¹ Γ // d.IsCutFree }

Equations

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