First-order $\mathbf{LJ}$

@[reducible, inline]

abbrev FFL.FirstOrder.Theoryᵢ (L : Language) : Type u

Equations

• FFL.FirstOrder.Theoryᵢ L = Set (FFL.FirstOrder.Sentenceᵢ L)

@[reducible, inline]

abbrev FFL.FirstOrder.LJ.Sequent (L : Language) : Type u

Equations

• FFL.FirstOrder.LJ.Sequent L = Multiset (FFL.FirstOrder.Propositionᵢ L)

@[reducible, inline]

abbrev FFL.FirstOrder.LJ.Head (L : Language) : Type u

Equations

• FFL.FirstOrder.LJ.Head L = Option (FFL.FirstOrder.Propositionᵢ L)

def FFL.FirstOrder.LJ.Head.shift {L : Language} (Ξ : Head L) : Head L

Equations

• Ξ.shift = Option.map (⇑FFL.FirstOrder.Rewriting.shift) Ξ

def FFL.FirstOrder.LJ.Head.rewrite {L : Language} (f : ℕ → SyntacticTerm L) (Ξ : Head L) : Head L

Equations

• FFL.FirstOrder.LJ.Head.rewrite f Ξ = Option.map (fun (x : FFL.FirstOrder.Semipropositionᵢ L 0) => (FFL.FirstOrder.Rewriting.app (FFL.FirstOrder.Rew.rewrite f)) x) Ξ

@[simp]

theorem FFL.FirstOrder.LJ.Head.shift_none {L : Language} : shift none = none

@[simp]

theorem FFL.FirstOrder.LJ.Head.shift_some {L : Language} (φ : Propositionᵢ L) : shift (some φ) = some (Rewriting.shift φ)

@[simp]

theorem FFL.FirstOrder.LJ.Head.rewrite_none {L : Language} (f : ℕ → SyntacticTerm L) : rewrite f none = none

@[simp]

theorem FFL.FirstOrder.LJ.Head.rewrite_some {L : Language} (f : ℕ → SyntacticTerm L) (φ : Propositionᵢ L) : rewrite f (some φ) = some ((Rewriting.app (Rew.rewrite f)) φ)

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

• 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 FFL.FirstOrder.LJ.«term_⊢ᴸᴶ¹_» : Lean.TrailingParserDescr

Equations

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

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

Equations

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

@[instance_reducible]

instance 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 FFL.FirstOrder.LJ.Derivation.traversal {L : Language} [L.DecidableEq] {Γ : Sequent L} {Ξ : Head L} : Γ ⊢ᴸᴶ¹ Ξ → Multiset.Traversal Γ

Equations

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

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

Equations

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

@[irreducible]

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

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.LJ.Derivation.eta (FFL.FirstOrder.Semiformulaᵢ.rel R v) = FFL.FirstOrder.LJ.Derivation.identity R v
• FFL.FirstOrder.LJ.Derivation.eta FFL.FirstOrder.Semiformulaᵢ.falsum = FFL.FirstOrder.LJ.Derivation.falsum.weakeningRight
• FFL.FirstOrder.LJ.Derivation.eta (FFL.FirstOrder.Semiformulaᵢ.all φ) = (((FFL.FirstOrder.LJ.Derivation.eta (FFL.FirstOrder.Rewriting.free φ)).cast ⋯ ⋯).negativeForall.cast ⋯ ⋯).positiveForall
• FFL.FirstOrder.LJ.Derivation.eta (FFL.FirstOrder.Semiformulaᵢ.exs φ) = (((FFL.FirstOrder.LJ.Derivation.eta (FFL.FirstOrder.Rewriting.free φ)).cast ⋯ ⋯).positiveExists.cast ⋯ ⋯).negativeExists

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

Equations

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

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

Equations

• d.positiveNeg = d.positiveImply

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

Equations

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

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

Equations

• di.modusPonens dφ = (FFL.Structural.contractMany di.traversal ((di.cut ((dφ.negativeImply ((FFL.FirstOrder.LJ.Derivation.eta ψ).cast ⋯ ⋯)).cast ⋯ ⋯)).cast ⋯ ⋯)).cast ⋯ ⋯

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def 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 Ξ

Equations

• One or more equations did not get rendered due to their size.
• FFL.FirstOrder.LJ.Derivation.rewrite f (FFL.FirstOrder.LJ.Derivation.identity R v) = FFL.FirstOrder.LJ.Derivation.identity R (⇑(FFL.FirstOrder.Rew.rewrite f) ∘ v)
• FFL.FirstOrder.LJ.Derivation.rewrite f (d.cut e) = (((FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).cut ((FFL.FirstOrder.LJ.Derivation.rewrite f e).cast ⋯ ⋯)).cast ⋯ ⋯
• FFL.FirstOrder.LJ.Derivation.rewrite f d.contraction = ((FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).contraction.cast ⋯ ⋯
• FFL.FirstOrder.LJ.Derivation.rewrite f d.weakening = (FFL.FirstOrder.LJ.Derivation.rewrite f d).weakening.cast ⋯ ⋯
• FFL.FirstOrder.LJ.Derivation.rewrite f d.weakeningRight = (FFL.FirstOrder.LJ.Derivation.rewrite f d).weakeningRight.cast ⋯ ⋯
• FFL.FirstOrder.LJ.Derivation.rewrite f FFL.FirstOrder.LJ.Derivation.verum = FFL.FirstOrder.LJ.Derivation.verum
• FFL.FirstOrder.LJ.Derivation.rewrite f FFL.FirstOrder.LJ.Derivation.falsum = FFL.FirstOrder.LJ.Derivation.falsum
• FFL.FirstOrder.LJ.Derivation.rewrite f d.positiveImply = ((FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).positiveImply.cast ⋯ ⋯
• FFL.FirstOrder.LJ.Derivation.rewrite f (d.positiveAnd a) = (FFL.FirstOrder.LJ.Derivation.rewrite f d).positiveAnd (FFL.FirstOrder.LJ.Derivation.rewrite f a)
• FFL.FirstOrder.LJ.Derivation.rewrite f d.negativeAnd = ((FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).negativeAnd.cast ⋯ ⋯
• FFL.FirstOrder.LJ.Derivation.rewrite f d.positiveOrLeft = (FFL.FirstOrder.LJ.Derivation.rewrite f d).positiveOrLeft
• FFL.FirstOrder.LJ.Derivation.rewrite f d.positiveOrRight = (FFL.FirstOrder.LJ.Derivation.rewrite f d).positiveOrRight
• FFL.FirstOrder.LJ.Derivation.rewrite f d.negativeForall = ((FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).negativeForall.cast ⋯ ⋯
• FFL.FirstOrder.LJ.Derivation.rewrite f d.positiveExists = ((FFL.FirstOrder.LJ.Derivation.rewrite f d).cast ⋯ ⋯).positiveExists.cast ⋯ ⋯

def 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

• (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
• FFL.FirstOrder.LJ.Derivation.verum.height = 0
• 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 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 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 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) Ξ

Equations

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

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

Equations

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

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

Equations

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

def 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 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 FFL.FirstOrder.LJ.Derivation.dneOfNegative {L : Language} {φ : Propositionᵢ L} : Semiformulaᵢ.IsNegative φ → ⦃∼∼φ⦄ ⊢ᴸᴶ¹ some φ

Equations

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

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

Equations

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

@[reducible, inline]

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

Mutual LJ derivability from singleton antecedents.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• FFL.FirstOrder.LJ.Derivation.InterDerivation.dne h = (FFL.FirstOrder.LJ.Derivation.dneOfNegative h, (FFL.FirstOrder.LJ.Derivation.eta φ).dni)

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

Equations

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

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

• symbol {L : Language} : LJ L

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev FFL.FirstOrder.LJ.Proof {L : Language} (φ : Propositionᵢ L) : Type u

Equations

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

@[instance_reducible]

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

Equations

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

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

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

• axioms : Multiset (Sentenceᵢ L)
• axioms_mem (ψ : Sentenceᵢ L) : ψ ∈ self.axioms → ψ ∈ T
• derivation : Multiset.map (⇑Rewriting.emb) self.axioms ⊢ᴸᴶ¹ some (Rewriting.emb σ)

@[instance_reducible]

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

Equations

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

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

Equations

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

@[instance_reducible]

instance 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 FFL.FirstOrder.Theoryᵢ.Proof.deduct {L : Language} {T : Theoryᵢ L} [L.DecidableEq] {φ ψ : Sentenceᵢ L} : adjoin φ T ⊢! ψ → T ⊢! φ 🡒 ψ

Equations

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

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

Equations

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

@[instance_reducible]

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