Supporting results for pointwise provable equality.

inductive PointwiseComposition.FFL.FirstOrder.LJ.Derivation {L : Language} : Sequent L → Head L → Type u

Data and laws for Derivation in FFL.FirstOrder.LJ.

• identity {L : Language} {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ℕ 0) : ⦃Semiformulaᵢ.rel R v⦄ ⊢ᴸᴶ¹ some (Semiformulaᵢ.rel R v)

  Identity rule

• cut {L : Language} {φ : Propositionᵢ L} {Γ Δ : Sequent L} {Ξ : Head L} : Γ ⊢ᴸᴶ¹ some φ → Δ + ⦃φ⦄ ⊢ᴸᴶ¹ Ξ → Γ + Δ ⊢ᴸᴶ¹ Ξ

  Cut rule

• contraction {L : Language} {Γ : Multiset (Propositionᵢ L)} {φ : Propositionᵢ L} {Ξ : Head L} : Γ + (⦃φ⦄ + ⦃φ⦄) ⊢ᴸᴶ¹ Ξ → Γ + ⦃φ⦄ ⊢ᴸᴶ¹ Ξ

  Left contraction

• weakening {L : Language} {Γ : Sequent L} {Ξ : Head L} {φ : Propositionᵢ L} : Γ ⊢ᴸᴶ¹ Ξ → Γ + ⦃φ⦄ ⊢ᴸᴶ¹ Ξ

  Left weakening

• weakeningRight {L : Language} {Γ : Sequent L} {φ : Propositionᵢ L} : Γ ⊢ᴸᴶ¹ none → Γ ⊢ᴸᴶ¹ some φ

  Right weakening

• verum {L : Language} : 0 ⊢ᴸᴶ¹ some ⊤

  Positive introduction of verum

• falsum {L : Language} : ⦃⊥⦄ ⊢ᴸᴶ¹ none

  Negative introduction of falsum

• positiveImply {L : Language} {Γ : Sequent L} {φ ψ : Propositionᵢ L} : Γ + ⦃φ⦄ ⊢ᴸᴶ¹ some ψ → Γ ⊢ᴸᴶ¹ some (φ ⇒ₗ ψ)

  Positive introduction of implication

• negativeImply {L : Language} {Γ Δ : Sequent L} {Ξ : Head L} {φ ψ : Propositionᵢ L} : Γ ⊢ᴸᴶ¹ some φ → Δ + ⦃ψ⦄ ⊢ᴸᴶ¹ Ξ → Γ + Δ + ⦃φ ⇒ₗ ψ⦄ ⊢ᴸᴶ¹ Ξ

  Negative introduction of implication

• positiveAnd {L : Language} {Γ : Sequent L} {φ ψ : Propositionᵢ L} : Γ ⊢ᴸᴶ¹ some φ → Γ ⊢ᴸᴶ¹ some ψ → Γ ⊢ᴸᴶ¹ some (φ ⋏ ψ)

  Positive introduction of conjunction

• negativeAnd {L : Language} {Γ : Sequent L} {Ξ : Head L} {φ ψ : Propositionᵢ L} : Γ + (⦃φ⦄ + ⦃ψ⦄) ⊢ᴸᴶ¹ Ξ → Γ + ⦃φ ⋏ ψ⦄ ⊢ᴸᴶ¹ Ξ

  Negative introduction of conjunction

• positiveOrLeft {L : Language} {Γ : Sequent L} {φ ψ : Propositionᵢ L} : Γ ⊢ᴸᴶ¹ some φ → Γ ⊢ᴸᴶ¹ some (φ ⋎ ψ)

  Positive introduction of disjunction (left)

• positiveOrRight {L : Language} {Γ : Sequent L} {φ ψ : Propositionᵢ L} : Γ ⊢ᴸᴶ¹ some ψ → Γ ⊢ᴸᴶ¹ some (φ ⋎ ψ)

  Positive introduction of disjunction (right)

• negativeOr {L : Language} {Γ : Multiset (Propositionᵢ L)} {φ : Propositionᵢ L} {Ξ : Head L} {ψ : Propositionᵢ L} : Γ + ⦃φ⦄ ⊢ᴸᴶ¹ Ξ → Γ + ⦃ψ⦄ ⊢ᴸᴶ¹ Ξ → Γ + ⦃φ ⋎ ψ⦄ ⊢ᴸᴶ¹ Ξ

  Negative introduction of disjunction

• positiveForall {L : Language} {Γ : Multiset (Semipropositionᵢ L 0)} {φ : Semipropositionᵢ L 1} : Rewriting.shifts Γ ⊢ᴸᴶ¹ some (Rewriting.free φ) → Γ ⊢ᴸᴶ¹ some (∀¹ φ)

  Positive introduction of universal quantifier

• negativeForall {L : Language} {Γ : Sequent L} {Ξ : Head L} {φ : Semipropositionᵢ L 1} {t : Term L ℕ} : Γ + ⦃φ/[t]⦄ ⊢ᴸᴶ¹ Ξ → Γ + ⦃∀¹ φ⦄ ⊢ᴸᴶ¹ Ξ

  Negative introduction of universal quantifier

• positiveExists {L : Language} {Γ : Sequent L} {φ : Semipropositionᵢ L 1} {t : Term L ℕ} : Γ ⊢ᴸᴶ¹ some (φ/[t]) → Γ ⊢ᴸᴶ¹ some (∃¹ φ)

  Positive introduction of existential quantifier

• negativeExists {L : Language} {Γ : Multiset (Semipropositionᵢ L 0)} {Ξ : Head L} {φ : Semipropositionᵢ L 1} : Rewriting.shifts Γ + ⦃Rewriting.free φ⦄ ⊢ᴸᴶ¹ Ξ.shift → Γ + ⦃∃¹ φ⦄ ⊢ᴸᴶ¹ Ξ

  Negative introduction of existential quantifier

def PointwiseComposition.FFL.FirstOrder.LJ.«term_⊢ᴸᴶ¹_» : Lean.TrailingParserDescr

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

Equations

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

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.cast {L : Language} {Γ Δ : Sequent L} {Ξ Λ : Head L} (d : Γ ⊢ᴸᴶ¹ Ξ) (seq : Γ = Δ := by abel) (heq : Ξ = Λ := by simp) : Δ ⊢ᴸᴶ¹ Λ

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

Equations

• d.cast seq heq = seq ▸ heq ▸ d

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.LJ.Derivation.instStructuralPropositionᵢ {L : Language} {Ξ : Head L} : Structural fun (Γ : Multiset (Propositionᵢ L)) => Γ ⊢ᴸᴶ¹ Ξ

Equations

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

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.traversal {L : Language} [L.DecidableEq] {Γ : Sequent L} {Ξ : Head L} : Γ ⊢ᴸᴶ¹ Ξ → Multiset.Traversal Γ

The traversal construction in FFL.FirstOrder.LJ.Derivation.

Equations

• One or more equations did not get rendered due to their size.
• (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.identity R v).traversal = PointwiseComposition.Multiset.Traversal.atom (PointwiseComposition.FFL.FirstOrder.Semiformulaᵢ.rel R v)
• (d.cut e).traversal = d.traversal.add e.traversal.remove
• d.contraction.traversal = (PointwiseComposition.Multiset.Traversal.cast ⋯ d.traversal).remove
• d.weakening.traversal = PointwiseComposition.Multiset.Traversal.succ φ d.traversal
• d.weakeningRight.traversal = d.traversal
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.verum.traversal = PointwiseComposition.Multiset.Traversal.zero
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.falsum.traversal = PointwiseComposition.Multiset.Traversal.atom ⊥
• d.positiveImply.traversal = d.traversal.remove
• (d.negativeImply e).traversal = PointwiseComposition.Multiset.Traversal.succ (φ ⇒ₗ ψ) (d.traversal.add e.traversal.remove)
• (d.positiveAnd a).traversal = d.traversal
• d.negativeAnd.traversal = PointwiseComposition.Multiset.Traversal.succ (φ ⋏ ψ) (PointwiseComposition.Multiset.Traversal.cast ⋯ d.traversal).remove.remove
• d.positiveOrLeft.traversal = d.traversal
• d.positiveOrRight.traversal = d.traversal
• (d.negativeOr a).traversal = PointwiseComposition.Multiset.Traversal.succ (φ ⋎ ψ) d.traversal.remove
• d.negativeForall.traversal = PointwiseComposition.Multiset.Traversal.succ (∀¹ φ) d.traversal.remove
• d.positiveExists.traversal = d.traversal

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

The contra construction in FFL.FirstOrder.LJ.Derivation.

Equations

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

@[irreducible]

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta {L : Language} (φ : Propositionᵢ L) : ⦃φ⦄ ⊢ᴸᴶ¹ some φ

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

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta (PointwiseComposition.FFL.FirstOrder.Semiformulaᵢ.rel R v) = PointwiseComposition.FFL.FirstOrder.LJ.Derivation.identity R v
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta PointwiseComposition.FFL.FirstOrder.Semiformulaᵢ.falsum = PointwiseComposition.FFL.FirstOrder.LJ.Derivation.falsum.weakeningRight

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.assumption {L : Language} {Γ : Sequent L} [L.DecidableEq] {φ : Propositionᵢ L} (t : Multiset.Traversal Γ) (h : φ ∈ Γ) : Γ ⊢ᴸᴶ¹ some φ

The assumption construction in FFL.FirstOrder.LJ.Derivation.

Equations

• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.assumption t h = (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta φ).contra t ⋯

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.positiveNeg {L : Language} {Γ : Sequent L} {φ : Propositionᵢ L} (d : Γ + ⦃φ⦄ ⊢ᴸᴶ¹ some ⊥) : Γ ⊢ᴸᴶ¹ some (∼φ)

The positive Neg construction in FFL.FirstOrder.LJ.Derivation.

Equations

• d.positiveNeg = d.positiveImply

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.negativeNeg {L : Language} {Γ : Sequent L} {φ : Propositionᵢ L} (d : Γ ⊢ᴸᴶ¹ some φ) : Γ + ⦃∼φ⦄ ⊢ᴸᴶ¹ none

The negative Neg construction in FFL.FirstOrder.LJ.Derivation.

Equations

• d.negativeNeg = (d.negativeImply (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.falsum.cast ⋯ ⋯)).cast ⋯ ⋯

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.modusPonens {L : Language} {Γ : Sequent L} [L.DecidableEq] {φ ψ : Propositionᵢ L} (di : Γ ⊢ᴸᴶ¹ some (φ ⇒ₗ ψ)) (dφ : Γ ⊢ᴸᴶ¹ some φ) : Γ ⊢ᴸᴶ¹ some ψ

The modus Ponens construction in FFL.FirstOrder.LJ.Derivation.

Equations

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

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.negElim {L : Language} {Γ : Sequent L} [L.DecidableEq] {φ : Propositionᵢ L} (dn : Γ ⊢ᴸᴶ¹ some (∼φ)) (dφ : Γ ⊢ᴸᴶ¹ some φ) : Γ ⊢ᴸᴶ¹ some ⊥

The neg Elim construction in FFL.FirstOrder.LJ.Derivation.

Equations

• dn.negElim dφ = dn.modusPonens dφ

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.cutOne {L : Language} {Γ : Sequent L} {Ξ : Head L} {φ : Propositionᵢ L} (dφ : Γ ⊢ᴸᴶ¹ some φ) (d : ⦃φ⦄ ⊢ᴸᴶ¹ Ξ) : Γ ⊢ᴸᴶ¹ Ξ

The cut One construction in FFL.FirstOrder.LJ.Derivation.

Equations

• dφ.cutOne d = (dφ.cut (d.cast ⋯ ⋯)).cast ⋯ ⋯

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.andLeft {L : Language} {Γ : Sequent L} {φ ψ : Propositionᵢ L} (d : Γ ⊢ᴸᴶ¹ some (φ ⋏ ψ)) : Γ ⊢ᴸᴶ¹ some φ

The and Left construction in FFL.FirstOrder.LJ.Derivation.

Equations

• d.andLeft = d.cutOne (((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta φ).weakening.cast ⋯ ⋯).negativeAnd.cast ⋯ ⋯)

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.andRight {L : Language} {Γ : Sequent L} {φ ψ : Propositionᵢ L} (d : Γ ⊢ᴸᴶ¹ some (φ ⋏ ψ)) : Γ ⊢ᴸᴶ¹ some ψ

The and Right construction in FFL.FirstOrder.LJ.Derivation.

Equations

• d.andRight = d.cutOne (((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta ψ).weakening.cast ⋯ ⋯).negativeAnd.cast ⋯ ⋯)

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.specialize {L : Language} {Γ : Sequent L} {φ : Semipropositionᵢ L 1} (d : Γ ⊢ᴸᴶ¹ some (∀¹ φ)) (t : Term L ℕ) : Γ ⊢ᴸᴶ¹ some (φ/[t])

The specialize construction in FFL.FirstOrder.LJ.Derivation.

Equations

• d.specialize t = d.cutOne (((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta (φ/[t])).cast ⋯ ⋯).negativeForall.cast ⋯ ⋯)

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

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

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.contraction = ((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).contraction.cast ⋯ ⋯
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.weakening = (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).weakening.cast ⋯ ⋯
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.weakeningRight = (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).weakeningRight.cast ⋯ ⋯
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f PointwiseComposition.FFL.FirstOrder.LJ.Derivation.verum = PointwiseComposition.FFL.FirstOrder.LJ.Derivation.verum
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f PointwiseComposition.FFL.FirstOrder.LJ.Derivation.falsum = PointwiseComposition.FFL.FirstOrder.LJ.Derivation.falsum
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.positiveImply = ((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).positiveImply.cast ⋯ ⋯
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.negativeAnd = ((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).negativeAnd.cast ⋯ ⋯
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.positiveOrLeft = (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).positiveOrLeft
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.positiveOrRight = (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).positiveOrRight
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.negativeForall = ((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).negativeForall.cast ⋯ ⋯
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d.positiveExists = ((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).positiveExists.cast ⋯ ⋯

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.height {L : Language} {Γ : Sequent L} {Ξ : Head L} : Γ ⊢ᴸᴶ¹ Ξ → ℕ

Height of an LJ derivation, with initial rules at height zero (standard definition).

Equations

• (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.identity R v).height = 0
• (d.cut e).height = max d.height e.height + 1
• d.contraction.height = d.height + 1
• d.weakening.height = d.height + 1
• d.weakeningRight.height = d.height + 1
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.verum.height = 0
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.falsum.height = 0
• d.positiveImply.height = d.height + 1
• (d.negativeImply e).height = max d.height e.height + 1
• (d.positiveAnd a).height = max d.height a.height + 1
• d.negativeAnd.height = d.height + 1
• d.positiveOrLeft.height = d.height + 1
• d.positiveOrRight.height = d.height + 1
• (d.negativeOr a).height = max d.height a.height + 1
• d.positiveForall.height = d.height + 1
• d.negativeForall.height = d.height + 1
• d.positiveExists.height = d.height + 1
• d.negativeExists.height = d.height + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LJ.Derivation.height_cast {L : Language} {Γ Δ : Sequent L} {Ξ Λ : Head L} (d : Γ ⊢ᴸᴶ¹ Ξ) (hΓ : Γ = Δ) (hΞ : Ξ = Λ) : (d.cast hΓ hΞ).height = d.height

Transport along sequent equalities preserves height (routine).

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LJ.Derivation.height_rewrite {L : Language} (f : ℕ → SyntacticTerm L) {Γ : Sequent L} {Ξ : Head L} (d : Γ ⊢ᴸᴶ¹ Ξ) : (rewrite f d).height = d.height

Term substitution preserves derivation height (standard syntactic property).

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.map {L : Language} {Γ : Sequent L} {Ξ : Head L} (d : Γ ⊢ᴸᴶ¹ Ξ) (f : ℕ → ℕ) : Multiset.map (fun (x : Semipropositionᵢ L 0) => (Rewriting.app (Rew.rewriteMap f)) x) Γ ⊢ᴸᴶ¹ Option.map (fun (x : Semipropositionᵢ L 0) => (Rewriting.app (Rew.rewriteMap f)) x) Ξ

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

Equations

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

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.shift {L : Language} {Γ : Sequent L} {Ξ : Head L} (d : Γ ⊢ᴸᴶ¹ Ξ) : Rewriting.shifts Γ ⊢ᴸᴶ¹ Ξ.shift

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

Equations

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

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.dni {L : Language} {Γ : Sequent L} {φ : Propositionᵢ L} (d : Γ ⊢ᴸᴶ¹ some φ) : Γ ⊢ᴸᴶ¹ some (∼∼φ)

The dni construction in FFL.FirstOrder.LJ.Derivation.

Equations

• d.dni = d.negativeNeg.weakeningRight.positiveNeg

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.contrapose {L : Language} {φ ψ : Propositionᵢ L} (d : ⦃φ⦄ ⊢ᴸᴶ¹ some ψ) : ⦃∼ψ⦄ ⊢ᴸᴶ¹ some (∼φ)

Contraposition for singleton derivations (standard intuitionistic reasoning).

Equations

• d.contrapose = (d.negativeNeg.weakeningRight.cast ⋯ ⋯).positiveNeg

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.doubleNegationMap {L : Language} {φ ψ : Propositionᵢ L} (d : ⦃φ⦄ ⊢ᴸᴶ¹ some ψ) : ⦃∼∼φ⦄ ⊢ᴸᴶ¹ some (∼∼ψ)

Double negation preserves derivability, by twice applying contraposition (folklore).

Equations

• d.doubleNegationMap = d.contrapose.contrapose

@[irreducible]

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.dneOfNegative {L : Language} {φ : Propositionᵢ L} : Semiformulaᵢ.IsNegative φ → ⦃∼∼φ⦄ ⊢ᴸᴶ¹ some φ

The dne Of Negative construction in FFL.FirstOrder.LJ.Derivation.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.dneOfNegative x_2 = ((PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta ⊥).cast ⋯ ⋯).positiveNeg.negativeNeg.weakeningRight.cast ⋯ ⋯

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.ofDNOfNegative {L : Language} {Γ : Sequent L} {φ : Propositionᵢ L} (d : Γ ⊢ᴸᴶ¹ some (∼∼φ)) (h : Semiformulaᵢ.IsNegative φ) : Γ ⊢ᴸᴶ¹ some φ

The of DNOf Negative construction in FFL.FirstOrder.LJ.Derivation.

Equations

• d.ofDNOfNegative h = d.cutOne (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.dneOfNegative h)

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation (L : Language) (φ ψ : Propositionᵢ L) : Type u

Mutual LJ derivability from singleton antecedents.

Equations

• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation L φ ψ = (⦃φ⦄ ⊢ᴸᴶ¹ some ψ × ⦃ψ⦄ ⊢ᴸᴶ¹ some φ)

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.refl {L : Language} (φ : Propositionᵢ L) : InterDerivation L φ φ

The refl construction in FFL.FirstOrder.LJ.Derivation.InterDerivation.

Equations

• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.refl φ = (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta φ, PointwiseComposition.FFL.FirstOrder.LJ.Derivation.eta φ)

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.symm {L : Language} {φ ψ : Propositionᵢ L} (d : InterDerivation L φ ψ) : InterDerivation L ψ φ

The symm construction in FFL.FirstOrder.LJ.Derivation.InterDerivation.

Equations

• d.symm = (d.2, d.1)

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.trans {L : Language} {φ ψ χ : Propositionᵢ L} (d₁ : InterDerivation L φ ψ) (d₂ : InterDerivation L ψ χ) : InterDerivation L φ χ

The trans construction in FFL.FirstOrder.LJ.Derivation.InterDerivation.

Equations

• d₁.trans d₂ = (d₁.1.cutOne d₂.1, d₂.2.cutOne d₁.2)

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.neg {L : Language} {φ ψ : Propositionᵢ L} (d : InterDerivation L φ ψ) : InterDerivation L (∼φ) (∼ψ)

The neg construction in FFL.FirstOrder.LJ.Derivation.InterDerivation.

Equations

• d.neg = (d.2.contrapose, d.1.contrapose)

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.and {L : Language} {φ₁ φ₂ ψ₁ ψ₂ : Propositionᵢ L} (dφ : InterDerivation L φ₁ φ₂) (dψ : InterDerivation L ψ₁ ψ₂) : InterDerivation L (φ₁ ⋏ ψ₁) (φ₂ ⋏ ψ₂)

The and construction in FFL.FirstOrder.LJ.Derivation.InterDerivation.

Equations

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

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.all {L : Language} {φ ψ : Semipropositionᵢ L 1} (d : InterDerivation L (Rewriting.free φ) (Rewriting.free ψ)) : InterDerivation L (∀¹ φ) (∀¹ ψ)

The all construction in FFL.FirstOrder.LJ.Derivation.InterDerivation.

Equations

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

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.dne {L : Language} {φ : Propositionᵢ L} (h : Semiformulaᵢ.IsNegative φ) : InterDerivation L (∼∼φ) φ

The dne construction in FFL.FirstOrder.LJ.Derivation.InterDerivation.

Equations

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

def PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.iffnegOfNegIff {L : Language} {φ ψ : Propositionᵢ L} (h : Semiformulaᵢ.IsNegative φ) (d : InterDerivation L (∼φ) ψ) : InterDerivation L φ (∼ψ)

The iffneg Of Neg Iff construction in FFL.FirstOrder.LJ.Derivation.InterDerivation.

Equations

• PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.iffnegOfNegIff h d = (PointwiseComposition.FFL.FirstOrder.LJ.Derivation.InterDerivation.dne h).symm.trans d.neg

inductive PointwiseComposition.FFL.FirstOrder.LJ (L : Language) : Type

Data and laws for LJ in FFL.FirstOrder.

• symbol {L : Language} : LJ 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.LJ.Proof {L : Language} (φ : Propositionᵢ L) : Type u

The Proof construction in FFL.FirstOrder.LJ.

Equations

• PointwiseComposition.FFL.FirstOrder.LJ.Proof φ = (0 ⊢ᴸᴶ¹ some φ)

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instEntailmentLJPropositionᵢ {L : Language} : Entailment (LJ L) (Propositionᵢ L)

Equations

• PointwiseComposition.FFL.FirstOrder.instEntailmentLJPropositionᵢ = { Prf := fun (x : PointwiseComposition.FFL.FirstOrder.LJ L) => PointwiseComposition.FFL.FirstOrder.LJ.Proof }

theorem PointwiseComposition.FFL.FirstOrder.LJ.Proof.def_eq {L : Language} (φ : Propositionᵢ L) : (𝐋𝐉¹ ⊢! φ) = (0 ⊢ᴸᴶ¹ some φ)

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

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 : Multiset.map (⇑Rewriting.emb) self.axioms ⊢ᴸᴶ¹ some (Rewriting.emb σ)

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instEntailmentTheoryᵢSentenceᵢ {L : Language} : Entailment (Theoryᵢ L) (Sentenceᵢ L)

Equations

• PointwiseComposition.FFL.FirstOrder.instEntailmentTheoryᵢSentenceᵢ = { Prf := PointwiseComposition.FFL.FirstOrder.Theoryᵢ.Proof }

def PointwiseComposition.FFL.FirstOrder.Theoryᵢ.Proof.weakening {L : Language} {T U : Theoryᵢ L} {σ : Sentenceᵢ L} (ss : T ⊆ U) : T ⊢! σ → U ⊢! σ

The weakening construction in FFL.FirstOrder.Theoryᵢ.Proof.

Equations

• PointwiseComposition.FFL.FirstOrder.Theoryᵢ.Proof.weakening ss { axioms := Γ, axioms_mem := hΓ, derivation := d } = { axioms := Γ, axioms_mem := ⋯, derivation := d }

@[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.

def PointwiseComposition.FFL.FirstOrder.Theoryᵢ.Proof.deduct {L : Language} {T : Theoryᵢ L} [L.DecidableEq] {φ ψ : Sentenceᵢ L} : adjoin φ T ⊢! ψ → T ⊢! φ ⇒ₗ ψ

The deduct construction in FFL.FirstOrder.Theoryᵢ.Proof.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Theoryᵢ.Proof.deductInv {L : Language} {T : Theoryᵢ L} {φ ψ : Sentenceᵢ L} : T ⊢! φ ⇒ₗ ψ → adjoin φ T ⊢! ψ

The deduct Inv construction in FFL.FirstOrder.Theoryᵢ.Proof.

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Theoryᵢ.Proof.instDeductionSentenceᵢ {L : Language} [L.DecidableEq] : Entailment.Deduction (Theoryᵢ L)

Equations

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