Foundation.IntFO.Basic.Deduction

source

@[reducible, inline]

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

Type u_1

Equations

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

source

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

Instances For

source

instance LO.FirstOrder.instSetLikeHilbertᵢSyntacticFormulaᵢ {L : Language} :

SetLike (Hilbertᵢ L) (SyntacticFormulaᵢ L)

Equations

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

source

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

Hilbertᵢ L

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Hilbertᵢ L

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Hilbertᵢ L

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

theorem LO.FirstOrder.Hilbertᵢ.minimal_le {L : Language} (Λ : Hilbertᵢ L) :

𝐌𝐢𝐧¹ ≤ Λ

source

theorem LO.FirstOrder.Hilbertᵢ.intuitionistic_le_classical {L : Language} :

𝐈𝐧𝐭¹ ≤ 𝐂𝐥¹

source

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ᵢ Λ (∀' (φ ➝ ψ/[]) ➝ ∃' φ ➝ ψ)

source

instance LO.FirstOrder.instSystemSyntacticFormulaᵢHilbertᵢ {L : Language} :

System (SyntacticFormulaᵢ L) (Hilbertᵢ L)

Equations

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

source

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 }

source

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

System.HasAxiomAndInst Λ

Equations

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

source

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₁ }

source

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₂ }

source

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

System.Minimal Λ

Equations

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

source

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

Λ ⊢ ψ

Equations

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

source

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

Λ ⊢ φ → ℕ

source

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

Lean.ParserDescr

Equations

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

source

@[simp]

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

depth (eaxm h) = 0

source

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_mdp {L : Language} {Λ : Hilbertᵢ L} {φ ψ : SyntacticFormulaᵢ L} (b : Λ ⊢ φ ➝ ψ) (d : Λ ⊢ φ) :

depth (mdp b d) = depth b ⊔ depth d + 1

source

@[simp]

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

depth (gen b) = depth b + 1

source

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_verum {L : Language} {Λ : Hilbertᵢ L} :

depth verum = 0

source

@[simp]

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

depth (imply₁ φ ψ) = 0

source

@[simp]

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

depth (imply₂ φ ψ χ) = 0

source

@[simp]

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

depth (and₁ φ ψ) = 0

source

@[simp]

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

depth (and₂ φ ψ) = 0

source

@[simp]

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

depth (and₃ φ ψ) = 0

source

@[simp]

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

depth (or₁ φ ψ) = 0

source

@[simp]

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

depth (or₂ φ ψ) = 0

source

@[simp]

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

depth (or₃ φ ψ χ) = 0

source

@[simp]

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

depth (all₁ φ t) = 0

source

@[simp]

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

depth (all₂ φ ψ) = 0

source

@[simp]

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

depth (ex₁ t φ) = 0

source

@[simp]

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

depth (ex₂ φ ψ) = 0

source

@[simp]

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

depth (HilbertProofᵢ.cast b e) = depth b

source

@[simp]

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

depth (b⨀d) = depth b ⊔ depth d + 1

source

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

source

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

source

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)))

source

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))

source

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.

source

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.

source

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

source

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)

source

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

source

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)

source

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

source

@[simp]

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

depth (rewrite f b) = depth b