Supporting results for pointwise provable equality.

Hauptsatz of classical first-order logic

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

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

Data and laws for Positive in FFL.FirstOrder.LK.Derivation.

• 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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.«term_⟶⁺_» : Lean.TrailingParserDescr

The «term ⟶⁺ » construction in FFL.FirstOrder.LK.Derivation.

Equations

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

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

The traversal construction in FFL.FirstOrder.LK.Derivation.Positive.

Equations

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

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.Positive.ofSubset {L : Language} {Ξ Γ : Sequent L} [L.DecidableEq] (tΞ : Multiset.Traversal Ξ) (tΓ : Multiset.Traversal Γ) (ss : Ξ ⊆ Γ) : Ξ ⟶⁺ Γ

The of Subset construction in FFL.FirstOrder.LK.Derivation.Positive.

Equations

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

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

The trans construction in FFL.FirstOrder.LK.Derivation.Positive.

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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.Positive.refl = x✝

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

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

Equations

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

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

The add Left construction in FFL.FirstOrder.LK.Derivation.Positive.

Equations

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

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

The cons construction in FFL.FirstOrder.LK.Derivation.Positive.

Equations

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

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

The add construction in FFL.FirstOrder.LK.Derivation.Positive.

Equations

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

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

The graft construction in FFL.FirstOrder.LK.Derivation.Positive.

Equations

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

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

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

Data and laws for Stronger Than in FFL.FirstOrder.LK.Derivation.Canonical.

• val : ∼p ⟶⁺ ∼q

  The val construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

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

The «term ≼ » construction in FFL.FirstOrder.Derivation.Canonical.

Equations

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

@[instance_reducible]

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

The inst Min Sequent construction in FFL.FirstOrder.LK.Derivation.Canonical.

Equations

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

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

@[simp]

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

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

The refl construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

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

The trans construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

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

The of Subset construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

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

The K left construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

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

The K right construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

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

The all construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

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

The min Le Left construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

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

The min Le Right construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

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

The le Min Right Of Le construction in FFL.FirstOrder.LK.Derivation.Canonical.StrongerThan.

Equations

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

@[irreducible]

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

The Forces construction in FFL.FirstOrder.LK.Derivation.Canonical.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.Canonical.Forces p PointwiseComposition.FFL.FirstOrder.Semiformulaᵢ.falsum = { b : ⊢ᴸᴷ¹ ∼p // b.IsCutFree }

@[reducible, inline]

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

The all Forces construction in FFL.FirstOrder.LK.Derivation.Canonical.

Equations

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

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

The «term ⊩ » construction in FFL.FirstOrder.Derivation.Canonical.Forces.

Equations

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

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

The «term⊩ » construction in FFL.FirstOrder.Derivation.Canonical.Forces.

Equations

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

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

The falsum Equiv construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The rel Equiv construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The and Equiv construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The or Equiv construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The imply Equiv construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The all Equiv construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The exs Equiv construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

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

Equations

• f.cast s = s ▸ f

@[irreducible]

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

The monotone construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

@[irreducible]

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

The explosion construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

def PointwiseComposition.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 (φ ⇒ₗ ψ)

The imply Of construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The modus Ponens construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

@[reducible, inline]

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

The Context Forces construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The of Subset construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.ContextForces.

Equations

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

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

The monotone construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.ContextForces.

Equations

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

def PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.LK.Derivation.Canonical.Forces.HeadForces {L : Language} (p : Sequent L) : LJ.Head L → Type u

The Head Forces construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

@[irreducible]

def PointwiseComposition.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.
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound d_2.weakening p tp b_2 = PointwiseComposition.FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound d_2 p tp (b_2.ofSubset ⋯)
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.Canonical.Forces.sound PointwiseComposition.FFL.FirstOrder.LJ.Derivation.falsum p tp b_2 = b_2 ⊥ ⋯

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

The lj Sound construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The rel Refl construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

def PointwiseComposition.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 (φ ⋎ ψ))

The or construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.refl.

Equations

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

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

The exs construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.refl.

Equations

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

@[irreducible]

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

The refl construction in FFL.FirstOrder.LK.Derivation.Canonical.Forces.

Equations

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

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

The hauptsatz construction in FFL.FirstOrder.LK.Derivation.Canonical.

Equations

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