@[reducible, inline]

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

Equations

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

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

• axiomSet : Set (LO.FirstOrder.SyntacticFormulaᵢ L)
• shift_closed : ∀ {φ : LO.FirstOrder.SyntacticFormulaᵢ L}, φ ∈ self.axiomSet → LO.FirstOrder.Rewriting.shift φ ∈ self.axiomSet

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

Equations

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

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

Equations

• 𝐌𝐢𝐧¹ = { axiomSet := ∅, shift_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 : LO.FirstOrder.Language} : LO.FirstOrder.Hilbertᵢ L

Equations

• 𝐈𝐧𝐭¹ = { axiomSet := {x : LO.FirstOrder.SyntacticFormulaᵢ L | ∃ (φ : LO.FirstOrder.SyntacticFormulaᵢ L), ⊥ ➝ φ = x}, shift_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 : LO.FirstOrder.Language} : LO.FirstOrder.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 : LO.FirstOrder.Language} (Λ : LO.FirstOrder.Hilbertᵢ L) : 𝐌𝐢𝐧¹ ≤ Λ

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

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

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

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

Equations

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

instance LO.FirstOrder.HilbertProofᵢ.instModusPonensHilbertᵢSyntacticFormulaᵢ {L : LO.FirstOrder.Language} (Λ : LO.FirstOrder.Hilbertᵢ L) : LO.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 : LO.FirstOrder.Language} (Λ : LO.FirstOrder.Hilbertᵢ L) : LO.System.HasAxiomAndInst Λ

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def LO.FirstOrder.HilbertProofᵢ.genOverFiniteContext {L : LO.FirstOrder.Language} {Λ : LO.FirstOrder.Hilbertᵢ L} {Γ : List (LO.FirstOrder.SyntacticSemiformulaᵢ L 0)} {φ : LO.FirstOrder.SyntacticSemiformulaᵢ L (0 + 1)} (b : LO.FirstOrder.Rewriting.shifts Γ ⊢[Λ] LO.FirstOrder.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 : LO.FirstOrder.Language} {Λ : LO.FirstOrder.Hilbertᵢ L} {Γ : List (LO.FirstOrder.SyntacticSemiformulaᵢ L 0)} {φ : LO.FirstOrder.SyntacticSemiformulaᵢ L (0 + 1)} (b : Γ ⊢[Λ] ∀' φ) (t : LO.FirstOrder.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 : LO.FirstOrder.Language} {Λ : LO.FirstOrder.Hilbertᵢ L} (φ ψ : LO.FirstOrder.SyntacticSemiformulaᵢ L (0 + 1)) : Λ ⊢ ∀' (φ ➝ ψ) ➝ ∀' φ ➝ ∀' ψ

Equations

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

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

Equations

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

@[irreducible]

def LO.FirstOrder.HilbertProofᵢ.dneOfNegative {L : LO.FirstOrder.Language} {Λ : LO.FirstOrder.Hilbertᵢ L} [L.DecidableEq] {φ : LO.FirstOrder.SyntacticFormulaᵢ L} : LO.FirstOrder.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 : LO.FirstOrder.Language} {Λ : LO.FirstOrder.Hilbertᵢ L} [L.DecidableEq] {φ : LO.FirstOrder.SyntacticFormulaᵢ L} {Γ : List (LO.FirstOrder.SyntacticFormulaᵢ L)} (b : Γ ⊢[Λ] ∼∼φ) (h : LO.FirstOrder.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 : LO.FirstOrder.Language} {Λ : LO.FirstOrder.Hilbertᵢ L} [L.DecidableEq] {φ : LO.FirstOrder.SyntacticFormulaᵢ L} (h : LO.FirstOrder.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 : LO.FirstOrder.Language} {Λ : LO.FirstOrder.Hilbertᵢ L} {φ : LO.FirstOrder.SyntacticFormulaᵢ L} : LO.FirstOrder.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 : LO.FirstOrder.Language} {Λ : LO.FirstOrder.Hilbertᵢ L} [L.DecidableEq] {φ ψ : LO.FirstOrder.SyntacticFormulaᵢ L} (h : LO.FirstOrder.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)