@[reducible, inline]

abbrev LO.FirstOrder.Sequentᵢ (L : Language) : Type u_1

Equations

• LO.FirstOrder.Sequentᵢ L = List (LO.FirstOrder.SyntacticFormulaᵢ L)

structure LO.FirstOrder.Hilbertᵢ (L : Language) : Type u_1

• axiomSet : Set (SyntacticFormulaᵢ L)
• rewrite_closed {φ : SyntacticFormulaᵢ L} : φ ∈ self.axiomSet → ∀ (f : ℕ → SyntacticTerm L), (Rewriting.app (Rew.rewrite f)) φ ∈ self.axiomSet

instance LO.FirstOrder.instSetLikeHilbertᵢSyntacticFormulaᵢ {L : Language} : SetLike (Hilbertᵢ L) (SyntacticFormulaᵢ L)

Equations

• LO.FirstOrder.instSetLikeHilbertᵢSyntacticFormulaᵢ = { coe := LO.FirstOrder.Hilbertᵢ.axiomSet, coe_injective' := ⋯ }

def LO.FirstOrder.Hilbertᵢ.Minimal {L : Language} : Hilbertᵢ L

Equations

• 𝐌𝐢𝐧¹ = { axiomSet := ∅, rewrite_closed := ⋯ }

def LO.FirstOrder.Hilbertᵢ.«term𝐌𝐢𝐧¹» : Lean.ParserDescr

Equations

• LO.FirstOrder.Hilbertᵢ.«term𝐌𝐢𝐧¹» = Lean.ParserDescr.node `LO.FirstOrder.Hilbertᵢ.«term𝐌𝐢𝐧¹» 1024 (Lean.ParserDescr.symbol "𝐌𝐢𝐧¹")

def LO.FirstOrder.Hilbertᵢ.Intuitionistic {L : Language} : Hilbertᵢ L

Equations

• 𝐈𝐧𝐭¹ = { axiomSet := {x : LO.FirstOrder.SyntacticFormulaᵢ L | ∃ (φ : LO.FirstOrder.SyntacticFormulaᵢ L), ⊥ ➝ φ = x}, rewrite_closed := ⋯ }

def LO.FirstOrder.Hilbertᵢ.«term𝐈𝐧𝐭¹» : Lean.ParserDescr

Equations

• LO.FirstOrder.Hilbertᵢ.«term𝐈𝐧𝐭¹» = Lean.ParserDescr.node `LO.FirstOrder.Hilbertᵢ.«term𝐈𝐧𝐭¹» 1024 (Lean.ParserDescr.symbol "𝐈𝐧𝐭¹")

def LO.FirstOrder.Hilbertᵢ.Classical {L : Language} : Hilbertᵢ L

Equations

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

def LO.FirstOrder.Hilbertᵢ.«term𝐂𝐥¹» : Lean.ParserDescr

Equations

• LO.FirstOrder.Hilbertᵢ.«term𝐂𝐥¹» = Lean.ParserDescr.node `LO.FirstOrder.Hilbertᵢ.«term𝐂𝐥¹» 1024 (Lean.ParserDescr.symbol "𝐂𝐥¹")

theorem LO.FirstOrder.Hilbertᵢ.minimal_le {L : Language} (Λ : Hilbertᵢ L) : 𝐌𝐢𝐧¹ ≤ Λ

theorem LO.FirstOrder.Hilbertᵢ.intuitionistic_le_classical {L : Language} : 𝐈𝐧𝐭¹ ≤ 𝐂𝐥¹

inductive LO.FirstOrder.HilbertProofᵢ {L : Language} (Λ : Hilbertᵢ L) : SyntacticFormulaᵢ L → Type u_1

• eaxm {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticFormulaᵢ L} : φ ∈ Λ → HilbertProofᵢ Λ φ
• mdp {L : Language} {Λ : Hilbertᵢ L} {φ ψ : SyntacticFormulaᵢ L} : HilbertProofᵢ Λ (φ ➝ ψ) → HilbertProofᵢ Λ φ → HilbertProofᵢ Λ ψ
• gen {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticSemiformulaᵢ L (0 + 1)} : HilbertProofᵢ Λ (Rewriting.free φ) → HilbertProofᵢ Λ (∀' φ)
• verum {L : Language} {Λ : Hilbertᵢ L} : HilbertProofᵢ Λ ⊤
• imply₁ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : HilbertProofᵢ Λ (φ ➝ ψ ➝ φ)
• imply₂ {L : Language} {Λ : Hilbertᵢ L} (φ ψ χ : SyntacticFormulaᵢ L) : HilbertProofᵢ Λ ((φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ)
• and₁ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : HilbertProofᵢ Λ (φ ⋏ ψ ➝ φ)
• and₂ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : HilbertProofᵢ Λ (φ ⋏ ψ ➝ ψ)
• and₃ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : HilbertProofᵢ Λ (φ ➝ ψ ➝ φ ⋏ ψ)
• or₁ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : HilbertProofᵢ Λ (φ ➝ φ ⋎ ψ)
• or₂ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : HilbertProofᵢ Λ (ψ ➝ φ ⋎ ψ)
• or₃ {L : Language} {Λ : Hilbertᵢ L} (φ ψ χ : SyntacticFormulaᵢ L) : HilbertProofᵢ Λ ((φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ)
• all₁ {L : Language} {Λ : Hilbertᵢ L} (φ : SyntacticSemiformulaᵢ L (0 + 1)) (t : Semiterm L ℕ 0) : HilbertProofᵢ Λ (∀' φ ➝ φ/[t])
• all₂ {L : Language} {Λ : Hilbertᵢ L} (φ : SyntacticSemiformulaᵢ L 0) (ψ : SyntacticSemiformulaᵢ L (0 + 1)) : HilbertProofᵢ Λ (∀' (φ/[] ➝ ψ) ➝ φ ➝ ∀' ψ)
• ex₁ {L : Language} {Λ : Hilbertᵢ L} (t : Semiterm L ℕ 0) (φ : SyntacticSemiformulaᵢ L (Nat.succ 0)) : HilbertProofᵢ Λ (φ/[t] ➝ ∃' φ)
• ex₂ {L : Language} {Λ : Hilbertᵢ L} (φ : SyntacticSemiformulaᵢ L (0 + 1)) (ψ : SyntacticSemiformulaᵢ L 0) : HilbertProofᵢ Λ (∀' (φ ➝ ψ/[]) ➝ ∃' φ ➝ ψ)

instance LO.FirstOrder.instSystemSyntacticFormulaᵢHilbertᵢ {L : Language} : System (SyntacticFormulaᵢ L) (Hilbertᵢ L)

Equations

• LO.FirstOrder.instSystemSyntacticFormulaᵢHilbertᵢ = { Prf := LO.FirstOrder.HilbertProofᵢ }

instance LO.FirstOrder.HilbertProofᵢ.instModusPonensHilbertᵢSyntacticFormulaᵢ {L : Language} (Λ : Hilbertᵢ L) : System.ModusPonens Λ

Equations

• LO.FirstOrder.HilbertProofᵢ.instModusPonensHilbertᵢSyntacticFormulaᵢ Λ = { mdp := fun {φ ψ : LO.FirstOrder.SyntacticFormulaᵢ L} => LO.FirstOrder.HilbertProofᵢ.mdp }

instance LO.FirstOrder.HilbertProofᵢ.instHasAxiomAndInstHilbertᵢSyntacticFormulaᵢ {L : Language} (Λ : Hilbertᵢ L) : System.HasAxiomAndInst Λ

Equations

• LO.FirstOrder.HilbertProofᵢ.instHasAxiomAndInstHilbertᵢSyntacticFormulaᵢ Λ = { and₃ := LO.FirstOrder.HilbertProofᵢ.and₃ }

instance LO.FirstOrder.HilbertProofᵢ.instHasAxiomImply₁HilbertᵢSyntacticFormulaᵢ {L : Language} (Λ : Hilbertᵢ L) : System.HasAxiomImply₁ Λ

Equations

• LO.FirstOrder.HilbertProofᵢ.instHasAxiomImply₁HilbertᵢSyntacticFormulaᵢ Λ = { imply₁ := LO.FirstOrder.HilbertProofᵢ.imply₁ }

instance LO.FirstOrder.HilbertProofᵢ.instHasAxiomImply₂HilbertᵢSyntacticFormulaᵢ {L : Language} (Λ : Hilbertᵢ L) : System.HasAxiomImply₂ Λ

Equations

• LO.FirstOrder.HilbertProofᵢ.instHasAxiomImply₂HilbertᵢSyntacticFormulaᵢ Λ = { imply₂ := LO.FirstOrder.HilbertProofᵢ.imply₂ }

instance LO.FirstOrder.HilbertProofᵢ.instMinimalHilbertᵢSyntacticFormulaᵢ {L : Language} (Λ : Hilbertᵢ L) : System.Minimal Λ

Equations

• LO.FirstOrder.HilbertProofᵢ.instMinimalHilbertᵢSyntacticFormulaᵢ Λ = LO.System.Minimal.mk

def LO.FirstOrder.HilbertProofᵢ.cast {L : Language} {Λ : Hilbertᵢ L} {φ ψ : SyntacticFormulaᵢ L} (b : Λ ⊢ φ) (e : φ = ψ) : Λ ⊢ ψ

Equations

• LO.FirstOrder.HilbertProofᵢ.cast b e = e ▸ b

def LO.FirstOrder.HilbertProofᵢ.depth {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticFormulaᵢ L} : Λ ⊢ φ → ℕ

def LO.FirstOrder.HilbertProofᵢ.«term‖_‖» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_eaxm {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticFormulaᵢ L} (h : φ ∈ Λ) : depth (eaxm h) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_mdp {L : Language} {Λ : Hilbertᵢ L} {φ ψ : SyntacticFormulaᵢ L} (b : Λ ⊢ φ ➝ ψ) (d : Λ ⊢ φ) : depth (mdp b d) = depth b ⊔ depth d + 1

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_gen {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticSemiformulaᵢ L (0 + 1)} (b : Λ ⊢ Rewriting.free φ) : depth (gen b) = depth b + 1

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_verum {L : Language} {Λ : Hilbertᵢ L} : depth verum = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_imply₁ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : depth (imply₁ φ ψ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_imply₂ {L : Language} {Λ : Hilbertᵢ L} (φ ψ χ : SyntacticFormulaᵢ L) : depth (imply₂ φ ψ χ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_and₁ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : depth (and₁ φ ψ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_and₂ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : depth (and₂ φ ψ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_and₃ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : depth (and₃ φ ψ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_or₁ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : depth (or₁ φ ψ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_or₂ {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticFormulaᵢ L) : depth (or₂ φ ψ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_or₃ {L : Language} {Λ : Hilbertᵢ L} (φ ψ χ : SyntacticFormulaᵢ L) : depth (or₃ φ ψ χ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_all₁ {L : Language} {Λ : Hilbertᵢ L} (φ : SyntacticSemiformulaᵢ L (0 + 1)) (t : Semiterm L ℕ 0) : depth (all₁ φ t) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_all₂ {L : Language} {Λ : Hilbertᵢ L} (φ : SyntacticSemiformulaᵢ L 0) (ψ : SyntacticSemiformulaᵢ L (0 + 1)) : depth (all₂ φ ψ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_ex₁ {L : Language} {Λ : Hilbertᵢ L} (t : Semiterm L ℕ 0) (φ : SyntacticSemiformulaᵢ L (Nat.succ 0)) : depth (ex₁ t φ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_ex₂ {L : Language} {Λ : Hilbertᵢ L} (φ : SyntacticSemiformulaᵢ L (0 + 1)) (ψ : SyntacticSemiformulaᵢ L 0) : depth (ex₂ φ ψ) = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_cast {L : Language} {Λ : Hilbertᵢ L} {φ ψ : SyntacticFormulaᵢ L} (b : Λ ⊢ φ) (e : φ = ψ) : depth (HilbertProofᵢ.cast b e) = depth b

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_mdp' {L : Language} {Λ : Hilbertᵢ L} {φ ψ : SyntacticFormulaᵢ L} (b : Λ ⊢ φ ➝ ψ) (d : Λ ⊢ φ) : depth (b⨀d) = depth b ⊔ depth d + 1

def LO.FirstOrder.HilbertProofᵢ.specialize {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticSemiformulaᵢ L (0 + 1)} (b : Λ ⊢ ∀' φ) (t : Semiterm L ℕ 0) : Λ ⊢ φ/[t]

Equations

• LO.FirstOrder.HilbertProofᵢ.specialize b t = LO.FirstOrder.HilbertProofᵢ.all₁ φ t⨀b

def LO.FirstOrder.HilbertProofᵢ.implyAll {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticSemiformulaᵢ L 0} {ψ : SyntacticSemiformulaᵢ L (0 + 1)} (b : Λ ⊢ Rewriting.shift φ ➝ Rewriting.free ψ) : Λ ⊢ φ ➝ ∀' ψ

Equations

• LO.FirstOrder.HilbertProofᵢ.implyAll b = LO.FirstOrder.HilbertProofᵢ.all₂ φ ψ⨀(⋯.mpr b).gen

def LO.FirstOrder.HilbertProofᵢ.genOverFiniteContext {L : Language} {Λ : Hilbertᵢ L} {Γ : List (SyntacticSemiformulaᵢ L 0)} {φ : SyntacticSemiformulaᵢ L (0 + 1)} (b : Rewriting.shifts Γ ⊢[Λ] Rewriting.free φ) : Γ ⊢[Λ] ∀' φ

Equations

• LO.FirstOrder.HilbertProofᵢ.genOverFiniteContext b = LO.System.FiniteContext.ofDef (LO.FirstOrder.HilbertProofᵢ.implyAll (⋯.mpr (LO.System.FiniteContext.toDef b)))

def LO.FirstOrder.HilbertProofᵢ.specializeOverContext {L : Language} {Λ : Hilbertᵢ L} {Γ : List (SyntacticSemiformulaᵢ L 0)} {φ : SyntacticSemiformulaᵢ L (0 + 1)} (b : Γ ⊢[Λ] ∀' φ) (t : Semiterm L ℕ 0) : Γ ⊢[Λ] φ/[t]

Equations

• LO.FirstOrder.HilbertProofᵢ.specializeOverContext b t = LO.System.FiniteContext.ofDef (LO.System.impTrans'' (LO.System.FiniteContext.toDef b) (LO.FirstOrder.HilbertProofᵢ.all₁ φ t))

def LO.FirstOrder.HilbertProofᵢ.allImplyAllOfAllImply {L : Language} {Λ : Hilbertᵢ L} (φ ψ : SyntacticSemiformulaᵢ L (0 + 1)) : Λ ⊢ ∀' (φ ➝ ψ) ➝ ∀' φ ➝ ∀' ψ

Equations

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

def LO.FirstOrder.HilbertProofᵢ.allIffAllOfIff {L : Language} {Λ : Hilbertᵢ L} {φ ψ : SyntacticSemiformulaᵢ L (0 + 1)} (b : Λ ⊢ Rewriting.free φ ⭤ Rewriting.free ψ) : Λ ⊢ ∀' φ ⭤ ∀' ψ

Equations

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

@[irreducible]

def LO.FirstOrder.HilbertProofᵢ.dneOfNegative {L : Language} {Λ : Hilbertᵢ L} [L.DecidableEq] {φ : SyntacticFormulaᵢ L} : Semiformulaᵢ.IsNegative φ → Λ ⊢ ∼∼φ ➝ φ

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.HilbertProofᵢ.dneOfNegative x_2 = LO.System.falsumDNE

def LO.FirstOrder.HilbertProofᵢ.ofDNOfNegative {L : Language} {Λ : Hilbertᵢ L} [L.DecidableEq] {φ : SyntacticFormulaᵢ L} {Γ : List (SyntacticFormulaᵢ L)} (b : Γ ⊢[Λ] ∼∼φ) (h : Semiformulaᵢ.IsNegative φ) : Γ ⊢[Λ] φ

Equations

• LO.FirstOrder.HilbertProofᵢ.ofDNOfNegative b h = LO.System.impTrans'' (LO.System.FiniteContext.toDef b) (LO.FirstOrder.HilbertProofᵢ.dneOfNegative h)

def LO.FirstOrder.HilbertProofᵢ.dnOfNegative {L : Language} {Λ : Hilbertᵢ L} [L.DecidableEq] {φ : SyntacticFormulaᵢ L} (h : Semiformulaᵢ.IsNegative φ) : Λ ⊢ ∼∼φ ⭤ φ

Equations

• LO.FirstOrder.HilbertProofᵢ.dnOfNegative h = LO.System.andIntro (LO.FirstOrder.HilbertProofᵢ.dneOfNegative h) LO.System.dni

@[irreducible]

def LO.FirstOrder.HilbertProofᵢ.efqOfNegative {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticFormulaᵢ L} : Semiformulaᵢ.IsNegative φ → Λ ⊢ ⊥ ➝ φ

Equations

• LO.FirstOrder.HilbertProofᵢ.efqOfNegative x_2 = LO.System.impId ⊥
• LO.FirstOrder.HilbertProofᵢ.efqOfNegative h = LO.System.implyAnd (LO.FirstOrder.HilbertProofᵢ.efqOfNegative ⋯) (LO.FirstOrder.HilbertProofᵢ.efqOfNegative ⋯)
• LO.FirstOrder.HilbertProofᵢ.efqOfNegative h = LO.System.impTrans'' (LO.FirstOrder.HilbertProofᵢ.efqOfNegative ⋯) LO.System.imply₁
• LO.FirstOrder.HilbertProofᵢ.efqOfNegative h = LO.FirstOrder.HilbertProofᵢ.implyAll (LO.System.cast ⋯ (LO.FirstOrder.HilbertProofᵢ.efqOfNegative ⋯))

def LO.FirstOrder.HilbertProofᵢ.iffnegOfNegIff {L : Language} {Λ : Hilbertᵢ L} [L.DecidableEq] {φ ψ : SyntacticFormulaᵢ L} (h : Semiformulaᵢ.IsNegative φ) (b : Λ ⊢ ∼φ ⭤ ψ) : Λ ⊢ φ ⭤ ∼ψ

Equations

• LO.FirstOrder.HilbertProofᵢ.iffnegOfNegIff h b = LO.System.iffTrans'' (LO.System.iffComm' (LO.FirstOrder.HilbertProofᵢ.dnOfNegative h)) (LO.System.negReplaceIff' b)

def LO.FirstOrder.HilbertProofᵢ.rewrite {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticFormulaᵢ L} (f : ℕ → SyntacticTerm L) : Λ ⊢ φ → Λ ⊢ (Rewriting.app (Rew.rewrite f)) φ

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.HilbertProofᵢ.rewrite f (b.mdp d) = LO.FirstOrder.HilbertProofᵢ.rewrite f b⨀LO.FirstOrder.HilbertProofᵢ.rewrite f d
• LO.FirstOrder.HilbertProofᵢ.rewrite f (LO.FirstOrder.HilbertProofᵢ.eaxm h) = LO.FirstOrder.HilbertProofᵢ.eaxm ⋯
• LO.FirstOrder.HilbertProofᵢ.rewrite f LO.FirstOrder.HilbertProofᵢ.verum = LO.FirstOrder.HilbertProofᵢ.verum

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_rewrite {L : Language} {Λ : Hilbertᵢ L} {φ : SyntacticFormulaᵢ L} (f : ℕ → SyntacticTerm L) (b : Λ ⊢ φ) : depth (rewrite f b) = depth b