Hilbert-style deduction system for first-order intuitionistic logic

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• LO.FirstOrder.Schemaᵢ L = Set (LO.FirstOrder.Propositionᵢ L)

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

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

@[implicit_reducible]

instance LO.FirstOrder.Hilbertᵢ.instSetLikePropositionᵢ {L : Language} : SetLike (Hilbertᵢ L) (Propositionᵢ L)

Equations

• LO.FirstOrder.Hilbertᵢ.instSetLikePropositionᵢ = { coe := LO.FirstOrder.Hilbertᵢ.axiomSet, coe_injective := ⋯ }

@[implicit_reducible]

instance LO.FirstOrder.Hilbertᵢ.instLE {L : Language} : LE (Hilbertᵢ L)

Equations

• LO.FirstOrder.Hilbertᵢ.instLE = { le := fun (Λ₁ Λ₂ : LO.FirstOrder.Hilbertᵢ L) => ↑Λ₁ ⊆ ↑Λ₂ }

instance LO.FirstOrder.Hilbertᵢ.instIsConcreteLEPropositionᵢ {L : Language} : IsConcreteLE (Hilbertᵢ L) (Propositionᵢ L)

@[simp]

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

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.Propositionᵢ L | ∃ (φ : LO.FirstOrder.Propositionᵢ L), LO.Axioms.EFQ φ = 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 "𝗖𝗹¹")

@[simp]

theorem LO.FirstOrder.Hilbertᵢ.minimal_le {L : Language} (Λ : Hilbertᵢ L) : 𝗠𝗶𝗻¹ ≤ Λ

@[simp]

theorem LO.FirstOrder.Hilbertᵢ.intuitionistic_le_classical {L : Language} : 𝗜𝗻𝘁¹ ≤ 𝗖𝗹¹

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

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

@[implicit_reducible]

instance LO.FirstOrder.instEntailmentHilbertᵢPropositionᵢ {L : Language} : Entailment (Hilbertᵢ L) (Propositionᵢ L)

Equations

• LO.FirstOrder.instEntailmentHilbertᵢPropositionᵢ = { Prf := LO.FirstOrder.HilbertProofᵢ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• LO.FirstOrder.HilbertProofᵢ.instHasAxiomAndInstHilbertᵢPropositionᵢ Λ = { and₃ := fun {φ ψ : LO.FirstOrder.Propositionᵢ L} => LO.FirstOrder.HilbertProofᵢ.and₃ φ ψ }

@[implicit_reducible]

instance LO.FirstOrder.HilbertProofᵢ.instHasAxiomImplyKHilbertᵢPropositionᵢ {L : Language} (Λ : Hilbertᵢ L) : Entailment.HasAxiomImplyK Λ

Equations

• LO.FirstOrder.HilbertProofᵢ.instHasAxiomImplyKHilbertᵢPropositionᵢ Λ = { implyK := fun {φ ψ : LO.FirstOrder.Propositionᵢ L} => LO.FirstOrder.HilbertProofᵢ.implyK φ ψ }

@[implicit_reducible]

instance LO.FirstOrder.HilbertProofᵢ.instHasAxiomImplySHilbertᵢPropositionᵢ {L : Language} (Λ : Hilbertᵢ L) : Entailment.HasAxiomImplyS Λ

Equations

• LO.FirstOrder.HilbertProofᵢ.instHasAxiomImplySHilbertᵢPropositionᵢ Λ = { implyS := fun {φ ψ χ : LO.FirstOrder.Propositionᵢ L} => LO.FirstOrder.HilbertProofᵢ.implyS φ ψ χ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.HilbertProofᵢ.instIntPropositionᵢHilbertᵢIntuitionistic {L : Language} : Entailment.Int 𝗜𝗻𝘁¹

Equations

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

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

Equations

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

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

Equations

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

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} {φ : Propositionᵢ L} (h : φ ∈ Λ) : (eaxm h).depth = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_mdp {L : Language} {Λ : Hilbertᵢ L} {φ ψ : Propositionᵢ L} (b : Λ ⊢! φ 🡒 ψ) (d : Λ ⊢! φ) : (mdp b d).depth = max (depth b) (depth d) + 1

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_implyK {L : Language} {Λ : Hilbertᵢ L} (φ ψ : Propositionᵢ L) : (implyK φ ψ).depth = 0

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_implyS {L : Language} {Λ : Hilbertᵢ L} (φ ψ χ : Propositionᵢ L) : (implyS φ ψ χ).depth = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.HilbertProofᵢ.depth_mdp' {L : Language} {Λ : Hilbertᵢ L} {φ ψ : Propositionᵢ L} (b : Λ ⊢! φ 🡒 ψ) (d : Λ ⊢! φ) : depth (b⨀!d) = max (depth b) (depth d) + 1

def LO.FirstOrder.HilbertProofᵢ.specialize {L : Language} {Λ : Hilbertᵢ L} {φ : Semipropositionᵢ 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} {φ : Semipropositionᵢ L 0} {ψ : Semipropositionᵢ 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 (Semipropositionᵢ L 0)} {φ : Semipropositionᵢ 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)))

def LO.FirstOrder.HilbertProofᵢ.specializeOverContext {L : Language} {Λ : Hilbertᵢ L} {Γ : List (Semipropositionᵢ L 0)} {φ : Semipropositionᵢ 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))

def LO.FirstOrder.HilbertProofᵢ.allImplyAllOfAllImply {L : Language} {Λ : Hilbertᵢ L} (φ ψ : Semipropositionᵢ 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} {φ ψ : Semipropositionᵢ 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] {φ : Propositionᵢ 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

def LO.FirstOrder.HilbertProofᵢ.ofDNOfNegative {L : Language} {Λ : Hilbertᵢ L} [L.DecidableEq] {φ : Propositionᵢ L} {Γ : List (Propositionᵢ 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)

def LO.FirstOrder.HilbertProofᵢ.DN_of_isNegative {L : Language} {Λ : Hilbertᵢ L} [L.DecidableEq] {φ : Propositionᵢ L} (h : Semiformulaᵢ.IsNegative φ) : Λ ⊢! ∼∼φ 🡘 φ

Equations

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

@[irreducible]

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

Equations

• LO.FirstOrder.HilbertProofᵢ.efqOfNegative x_2 = LO.Entailment.C_id
• LO.FirstOrder.HilbertProofᵢ.efqOfNegative h = LO.Entailment.CK_of_C_of_C (LO.FirstOrder.HilbertProofᵢ.efqOfNegative ⋯) (LO.FirstOrder.HilbertProofᵢ.efqOfNegative ⋯)
• LO.FirstOrder.HilbertProofᵢ.efqOfNegative h = LO.Entailment.C_trans (LO.FirstOrder.HilbertProofᵢ.efqOfNegative ⋯) LO.Entailment.implyK
• LO.FirstOrder.HilbertProofᵢ.efqOfNegative h = LO.FirstOrder.HilbertProofᵢ.implyAll (LO.Entailment.cast (LO.FirstOrder.HilbertProofᵢ.efqOfNegative ⋯) ⋯)

def LO.FirstOrder.HilbertProofᵢ.iffnegOfNegIff {L : Language} {Λ : Hilbertᵢ L} [L.DecidableEq] {φ ψ : Propositionᵢ 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)

def LO.FirstOrder.HilbertProofᵢ.rewrite {L : Language} {Λ : Hilbertᵢ L} {φ : Propositionᵢ 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} {φ : Propositionᵢ L} (f : ℕ → SyntacticTerm L) (b : Λ ⊢! φ) : depth (rewrite f b) = depth b

def LO.FirstOrder.HilbertProofᵢ.ofLE {L : Language} {φ : Propositionᵢ 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ᵢ.implyK φ_2 ψ) = LO.FirstOrder.HilbertProofᵢ.implyK φ_2 ψ
• LO.FirstOrder.HilbertProofᵢ.ofLE h (LO.FirstOrder.HilbertProofᵢ.implyS φ_2 ψ χ) = LO.FirstOrder.HilbertProofᵢ.implyS φ_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 ψ

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

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

• theory : Set (Sentenceᵢ L)

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

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

@[implicit_reducible]

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 := ⋯ }

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

@[simp]

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

@[implicit_reducible]

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.

@[simp]

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

@[simp]

theorem LO.FirstOrder.Theoryᵢ.adjoin_theory_def {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} {φ : Sentenceᵢ L} : (adjoin φ T).theory = insert φ T.theory

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) *⊢[𝓗]! LO.FirstOrder.Rewriting.emb φ

@[implicit_reducible]

instance LO.FirstOrder.Theoryᵢ.instEntailmentSentenceᵢ {L : Language} {𝓗 : Hilbertᵢ L} : Entailment (Theoryᵢ L 𝓗) (Sentenceᵢ L)

Equations

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

theorem LO.FirstOrder.Theoryᵢ.provable_def {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} {φ : Sentenceᵢ L} : T ⊢ φ ↔ (⇑Rewriting.emb '' T.theory) *⊢[𝓗] Rewriting.emb φ

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

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 ⋯

@[implicit_reducible]

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.

def LO.FirstOrder.Theoryᵢ.ofHilbert {L : Language} {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} {φ : Sentenceᵢ L} : 𝓗 ⊢! Rewriting.emb φ → T ⊢! φ

Equations

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

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)

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)

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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 {φ : LO.FirstOrder.Sentenceᵢ L} => LO.FirstOrder.Theoryᵢ.ofHilbert LO.Entailment.efq }

@[implicit_reducible]

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 {φ : LO.FirstOrder.Sentenceᵢ L} => LO.FirstOrder.Theoryᵢ.ofHilbert LO.Entailment.dne }