Foundation.FirstOrder.Intuitionistic.Deduction

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

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.Hilbertᵢ.instSetLikeSyntacticFormulaᵢ {L : Language} :

SetLike (Hilbertᵢ L) (SyntacticFormulaᵢ L)

Equations

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

source

@[simp]

theorem LO.FirstOrder.Hilbertᵢ.mem_mk {L : Language} {φ : SyntacticFormulaᵢ L} (s : Set (SyntacticFormulaᵢ L)) (h : ∀ {φ : SyntacticFormulaᵢ L}, φ ∈ s → ∀ (f : ℕ → SyntacticTerm L), (Rewriting.app (Rew.rewrite f)) φ ∈ s) :

φ ∈ { axiomSet := s, rewrite_closed := h } ↔ φ ∈ s

source

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

Hilbertᵢ L

Equations

𝗠𝗶𝗻¹ = { axiomSet := ∅, rewrite_closed := ⋯ }

Instances For

source

def LO.FirstOrder.Hilbertᵢ.«term𝗠𝗶𝗻¹» :

Lean.ParserDescr

Equations

LO.FirstOrder.Hilbertᵢ.«term𝗠𝗶𝗻¹» = Lean.ParserDescr.node `LO.FirstOrder.Hilbertᵢ.«term𝗠𝗶𝗻¹» 1024 (Lean.ParserDescr.symbol "𝗠𝗶𝗻¹")

Instances For

source

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

Hilbertᵢ L

Equations

𝗜𝗻𝘁¹ = { axiomSet := {x : LO.FirstOrder.SyntacticFormulaᵢ L | ∃ (φ : LO.FirstOrder.SyntacticFormulaᵢ L), LO.Axioms.EFQ φ = x}, rewrite_closed := ⋯ }

Instances For

source

def LO.FirstOrder.Hilbertᵢ.«term𝗜𝗻𝘁¹» :

Lean.ParserDescr

Equations

LO.FirstOrder.Hilbertᵢ.«term𝗜𝗻𝘁¹» = Lean.ParserDescr.node `LO.FirstOrder.Hilbertᵢ.«term𝗜𝗻𝘁¹» 1024 (Lean.ParserDescr.symbol "𝗜𝗻𝘁¹")

Instances For

source

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

Hilbertᵢ L

Equations

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

Instances For

source

def LO.FirstOrder.Hilbertᵢ.«term𝗖𝗹¹» :

Lean.ParserDescr

Equations

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

Instances For

source

@[simp]

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

𝗠𝗶𝗻¹ ≤ Λ

source

@[simp]

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

𝗜𝗻𝘁¹ ≤ 𝗖𝗹¹

source

inductive LO.FirstOrder.HilbertProofᵢ {L : Language} (Λ : Hilbertᵢ L) :

SyntacticFormulaᵢ L → Type u

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

Instances For

source

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

Entailment (Hilbertᵢ L) (SyntacticFormulaᵢ L)

Equations

LO.FirstOrder.instEntailmentHilbertᵢSyntacticFormulaᵢ = { Prf := LO.FirstOrder.HilbertProofᵢ }

source

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

Entailment.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) :

Entailment.HasAxiomAndInst Λ

Equations

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

source

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

Entailment.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) :

Entailment.HasAxiomImply₂ Λ

Equations

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

source

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

Entailment.Minimal Λ

Equations

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

source

instance LO.FirstOrder.HilbertProofᵢ.instIntHilbertᵢSyntacticFormulaᵢIntuitionistic {L : Language} :

Entailment.Int 𝗜𝗻𝘁¹

Equations

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

source

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

Λ ⊢! ψ

Equations

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

Instances For

source

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

Λ ⊢! φ → ℕ

Equations

(b.mdp d).depth = max b.depth d.depth + 1
b.gen.depth = b.depth + 1
LO.FirstOrder.HilbertProofᵢ.depth x✝ = 0

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

@[simp]

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

(eaxm h).depth = 0

source

@[simp]

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

(mdp b d).depth = max (depth b) (depth d) + 1

source

@[simp]

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

(gen b).depth = depth b + 1

source

@[simp]

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

verum.depth = 0

source

@[simp]

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

(imply₁ φ ψ).depth = 0

source

@[simp]

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

(imply₂ φ ψ χ).depth = 0

source

@[simp]

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

(and₁ φ ψ).depth = 0

source

@[simp]

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

(and₂ φ ψ).depth = 0

source

@[simp]

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

(and₃ φ ψ).depth = 0

source

@[simp]

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

(or₁ φ ψ).depth = 0

source

@[simp]

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

(or₂ φ ψ).depth = 0

source

@[simp]

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

(or₃ φ ψ χ).depth = 0

source

@[simp]

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

(all₁ φ t).depth = 0

source

@[simp]

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

(all₂ φ ψ).depth = 0

source

@[simp]

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

(ex₁ t φ).depth = 0

source

@[simp]

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

(ex₂ φ ψ).depth = 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) = max (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

Instances For

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

Instances For

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.Entailment.FiniteContext.ofDef (LO.FirstOrder.HilbertProofᵢ.implyAll (⋯.mpr (LO.Entailment.FiniteContext.toDef b)))

Instances For

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.Entailment.FiniteContext.ofDef (LO.Entailment.C_trans (LO.Entailment.FiniteContext.toDef b) (LO.FirstOrder.HilbertProofᵢ.all₁ φ t))

Instances For

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.

Instances For

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.

Instances For

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.Entailment.CNNOO

Instances For

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.Entailment.C_trans (LO.Entailment.FiniteContext.toDef b) (LO.FirstOrder.HilbertProofᵢ.dneOfNegative h)

Instances For

source

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

Λ ⊢! ∼∼φ ⭤ φ

Equations

LO.FirstOrder.HilbertProofᵢ.DN_of_isNegative h = LO.Entailment.K_intro (LO.FirstOrder.HilbertProofᵢ.dneOfNegative h) LO.Entailment.dni

Instances For

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.Entailment.E_trans (LO.Entailment.E_symm (LO.FirstOrder.HilbertProofᵢ.DN_of_isNegative h)) (LO.Entailment.ENN_of_E b)

Instances For

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

Instances For

source

@[simp]

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

depth (rewrite f b) = depth b

source

def LO.FirstOrder.HilbertProofᵢ.ofLE {L : Language} {φ : SyntacticFormulaᵢ L} {Λ₁ Λ₂ : Hilbertᵢ L} (h : Λ₁ ≤ Λ₂) :

Λ₁ ⊢! φ → Λ₂ ⊢! φ

Equations

LO.FirstOrder.HilbertProofᵢ.ofLE h (b.mdp d) = LO.FirstOrder.HilbertProofᵢ.mdp (LO.FirstOrder.HilbertProofᵢ.ofLE h b) (LO.FirstOrder.HilbertProofᵢ.ofLE h d)
LO.FirstOrder.HilbertProofᵢ.ofLE h b.gen = LO.FirstOrder.HilbertProofᵢ.gen (LO.FirstOrder.HilbertProofᵢ.ofLE h b)
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.eaxm h_1) = LO.FirstOrder.HilbertProofᵢ.eaxm ⋯
LO.FirstOrder.HilbertProofᵢ.ofLE h LO.FirstOrder.HilbertProofᵢ.verum = LO.FirstOrder.HilbertProofᵢ.verum
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.imply₁ φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.imply₁ φ_2 ψ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.imply₂ φ_2 ψ χ) = LO.FirstOrder.HilbertProofᵢ.imply₂ φ_2 ψ χ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.and₁ φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.and₁ φ_2 ψ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.and₂ φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.and₂ φ_2 ψ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.and₃ φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.and₃ φ_2 ψ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.or₁ φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.or₁ φ_2 ψ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.or₂ φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.or₂ φ_2 ψ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.or₃ φ_2 ψ χ) = LO.FirstOrder.HilbertProofᵢ.or₃ φ_2 ψ χ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.all₁ φ_2 t) = LO.FirstOrder.HilbertProofᵢ.all₁ φ_2 t
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.all₂ φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.all₂ φ_2 ψ
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.ex₁ t φ_2) = LO.FirstOrder.HilbertProofᵢ.ex₁ t φ_2
LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.ex₂ φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.ex₂ φ_2 ψ

Instances For

source

theorem LO.FirstOrder.HilbertProofᵢ.of_le {L : Language} {φ : SyntacticFormulaᵢ L} {Λ₁ Λ₂ : Hilbertᵢ L} (h : Λ₁ ≤ Λ₂) :

Λ₁ ⊢ φ → Λ₂ ⊢ φ

source

structure LO.FirstOrder.Theoryᵢ (L : Language) (𝓗 : Hilbertᵢ L) :

Type u

theory : Set (Sentenceᵢ L)

Instances For

source

theorem LO.FirstOrder.Theoryᵢ.ext_iff {L : Language} {𝓗 : Hilbertᵢ L} {x y : Theoryᵢ L 𝓗} :

x = y ↔ x.theory = y.theory

source

theorem LO.FirstOrder.Theoryᵢ.ext {L : Language} {𝓗 : Hilbertᵢ L} {x y : Theoryᵢ L 𝓗} (theory : x.theory = y.theory) :

x = y

source

instance LO.FirstOrder.Theoryᵢ.instSetLikeSentenceᵢ {L : Language} {𝓗 : Hilbertᵢ L} :

SetLike (Theoryᵢ L 𝓗) (Sentenceᵢ L)

Equations

LO.FirstOrder.Theoryᵢ.instSetLikeSentenceᵢ = { coe := LO.FirstOrder.Theoryᵢ.theory, coe_injective' := ⋯ }

source

theorem LO.FirstOrder.Theoryᵢ.mem_def {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} {φ : Sentenceᵢ L} :

φ ∈ T ↔ φ ∈ T.theory

source

@[simp]

theorem LO.FirstOrder.Theoryᵢ.mem_mk_iff {L : Language} {𝓗 : Hilbertᵢ L} {φ : Sentenceᵢ L} (s : Set (Sentenceᵢ L)) :

φ ∈ { theory := s } ↔ φ ∈ s

source

instance LO.FirstOrder.Theoryᵢ.instAdjunctiveSetSentenceᵢ {L : Language} {𝓗 : Hilbertᵢ L} :

AdjunctiveSet (Sentenceᵢ L) (Theoryᵢ L 𝓗)

Equations

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

source

@[simp]

theorem LO.FirstOrder.Theoryᵢ.empty_eq_empty {L : Language} {𝓗 : Hilbertᵢ L} :

↑∅ = ∅

source

@[simp]

theorem LO.FirstOrder.Theoryᵢ.adjoin_theory_def {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} {φ : Sentenceᵢ L} :

(adjoin φ T).theory = insert φ T.theory

source

def LO.FirstOrder.Theoryᵢ.Proof {L : Language} {𝓗 : Hilbertᵢ L} (T : Theoryᵢ L 𝓗) (φ : Sentenceᵢ L) :

Type u

Equations

T.Proof φ = (LO.FirstOrder.Rewriting.emb '' T.theory) *⊢[𝓗]! ↑φ

Instances For

source

instance LO.FirstOrder.Theoryᵢ.instEntailmentSentenceᵢ {L : Language} {𝓗 : Hilbertᵢ L} :

Entailment (Theoryᵢ L 𝓗) (Sentenceᵢ L)

Equations

LO.FirstOrder.Theoryᵢ.instEntailmentSentenceᵢ = { Prf := LO.FirstOrder.Theoryᵢ.Proof }

source

theorem LO.FirstOrder.Theoryᵢ.provable_def {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} {φ : Sentenceᵢ L} :

T ⊢ φ ↔ (Rewriting.emb '' T.theory) *⊢[𝓗] ↑φ

source

def LO.FirstOrder.Theoryᵢ.Proof.cast! {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} {φ ψ : Sentenceᵢ L} (e : φ = ψ) :

T ⊢! φ → T ⊢! ψ

Equations

LO.FirstOrder.Theoryᵢ.Proof.cast! e b = e ▸ b

Instances For

source

def LO.FirstOrder.Theoryᵢ.Proof.weakening! {L : Language} {𝓗 : Hilbertᵢ L} {T U : Theoryᵢ L 𝓗} {φ : Sentenceᵢ L} [L.DecidableEq] (ss : T ⊆ U) :

T ⊢! φ → U ⊢! φ

Equations

LO.FirstOrder.Theoryᵢ.Proof.weakening! ss = LO.Entailment.Context.weakening ⋯

Instances For

source

instance LO.FirstOrder.Theoryᵢ.instAxiomatizedSentenceᵢ {L : Language} {𝓗 : Hilbertᵢ L} [L.DecidableEq] :

Entailment.Axiomatized (Theoryᵢ L 𝓗)

Equations

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

source

def LO.FirstOrder.Theoryᵢ.ofHilbert {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} {φ : Sentenceᵢ L} :

𝓗 ⊢! ↑φ → T ⊢! φ

Equations

LO.FirstOrder.Theoryᵢ.ofHilbert = LO.Entailment.Context.of

Instances For

source

def LO.FirstOrder.Theoryᵢ.deduct! {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} [L.DecidableEq] {φ ψ : Sentenceᵢ L} (b : adjoin φ T ⊢! ψ) :

T ⊢! φ ➝ ψ

Equations

LO.FirstOrder.Theoryᵢ.deduct! b = LO.Entailment.Context.deduct (LO.Entailment.Context.weakening ⋯ b)

Instances For

source

def LO.FirstOrder.Theoryᵢ.deductInv! {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} [L.DecidableEq] {φ ψ : Sentenceᵢ L} (b : T ⊢! φ ➝ ψ) :

adjoin φ T ⊢! ψ

Equations

LO.FirstOrder.Theoryᵢ.deductInv! b = LO.Entailment.Context.weakening ⋯ (LO.Entailment.Context.deductInv b)

Instances For

source

instance LO.FirstOrder.Theoryᵢ.instDeductionSentenceᵢ {L : Language} {𝓗 : Hilbertᵢ L} [L.DecidableEq] :

Entailment.Deduction (Theoryᵢ L 𝓗)

Equations

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

source

instance LO.FirstOrder.Theoryᵢ.instMinimalSentenceᵢ {L : Language} (𝓗 : Hilbertᵢ L) {T : Theoryᵢ L 𝓗} [L.DecidableEq] :

Entailment.Minimal T

Equations

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

source

instance LO.FirstOrder.Theoryᵢ.minimal {L : Language} (𝓗 : Hilbertᵢ L) {T : Theoryᵢ L 𝓗} [L.DecidableEq] [Entailment.Int 𝓗] :

Entailment.Int T

Equations

LO.FirstOrder.Theoryᵢ.minimal 𝓗 = { toMinimal := LO.FirstOrder.Theoryᵢ.instMinimalSentenceᵢ 𝓗, efq := fun (x : LO.FirstOrder.Sentenceᵢ L) => LO.FirstOrder.Theoryᵢ.ofHilbert LO.Entailment.efq }

source

instance LO.FirstOrder.Theoryᵢ.cl {L : Language} (𝓗 : Hilbertᵢ L) {T : Theoryᵢ L 𝓗} [L.DecidableEq] [Entailment.Cl 𝓗] :

Entailment.Cl T

Equations

LO.FirstOrder.Theoryᵢ.cl 𝓗 = { toMinimal := LO.FirstOrder.Theoryᵢ.instMinimalSentenceᵢ 𝓗, dne := fun (x : LO.FirstOrder.Sentenceᵢ L) => LO.FirstOrder.Theoryᵢ.ofHilbert LO.Entailment.dne }