structure LO.IntProp.Hilbert (α : Type u_1) : Type u_1

• axioms : LO.IntProp.Theory α

class LO.IntProp.Hilbert.IncludeEFQ {α : Type u} (H : LO.IntProp.Hilbert α) : Prop

• include_EFQ : 𝗘𝗙𝗤 ⊆ H.axioms

class LO.IntProp.Hilbert.IncludeLEM {α : Type u} (H : LO.IntProp.Hilbert α) : Prop

• include_LEM : 𝗟𝗘𝗠 ⊆ H.axioms

class LO.IntProp.Hilbert.IncludeDNE {α : Type u} (H : LO.IntProp.Hilbert α) : Prop

• include_DNE : 𝗗𝗡𝗘 ⊆ H.axioms

inductive LO.IntProp.Hilbert.Deduction {α : Type u} (H : LO.IntProp.Hilbert α) : LO.IntProp.Formula α → Type u

• eaxm: {α : Type u} → {H : LO.IntProp.Hilbert α} → {φ : LO.IntProp.Formula α} → φ ∈ H.axioms → H.Deduction φ
• mdp: {α : Type u} → {H : LO.IntProp.Hilbert α} → {φ ψ : LO.IntProp.Formula α} → H.Deduction (φ ➝ ψ) → H.Deduction φ → H.Deduction ψ
• verum: {α : Type u} → {H : LO.IntProp.Hilbert α} → H.Deduction ⊤
• imply₁: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ ψ : LO.IntProp.Formula α) → H.Deduction (φ ➝ ψ ➝ φ)
• imply₂: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ ψ χ : LO.IntProp.Formula α) → H.Deduction ((φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ)
• and₁: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ ψ : LO.IntProp.Formula α) → H.Deduction (φ ⋏ ψ ➝ φ)
• and₂: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ ψ : LO.IntProp.Formula α) → H.Deduction (φ ⋏ ψ ➝ ψ)
• and₃: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ ψ : LO.IntProp.Formula α) → H.Deduction (φ ➝ ψ ➝ φ ⋏ ψ)
• or₁: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ ψ : LO.IntProp.Formula α) → H.Deduction (φ ➝ φ ⋎ ψ)
• or₂: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ ψ : LO.IntProp.Formula α) → H.Deduction (ψ ➝ φ ⋎ ψ)
• or₃: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ ψ χ : LO.IntProp.Formula α) → H.Deduction ((φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ)
• neg_equiv: {α : Type u} → {H : LO.IntProp.Hilbert α} → (φ : LO.IntProp.Formula α) → H.Deduction (LO.Axioms.NegEquiv φ)

instance LO.IntProp.Hilbert.instSystemFormula {α : Type u} : LO.System (LO.IntProp.Formula α) (LO.IntProp.Hilbert α)

Equations

• LO.IntProp.Hilbert.instSystemFormula = { Prf := LO.IntProp.Hilbert.Deduction }

instance LO.IntProp.Hilbert.instMinimalFormula {α : Type u} {H : LO.IntProp.Hilbert α} : LO.System.Minimal H

Equations

• LO.IntProp.Hilbert.instMinimalFormula = LO.System.Minimal.mk

instance LO.IntProp.Hilbert.instHasAxiomEFQFormulaOfIncludeEFQ {α : Type u} {H : LO.IntProp.Hilbert α} [H.IncludeEFQ] : LO.System.HasAxiomEFQ H

Equations

• LO.IntProp.Hilbert.instHasAxiomEFQFormulaOfIncludeEFQ = { efq := fun (x : LO.IntProp.Formula α) => LO.IntProp.Hilbert.Deduction.eaxm ⋯ }

instance LO.IntProp.Hilbert.instHasAxiomLEMFormulaOfIncludeLEM {α : Type u} {H : LO.IntProp.Hilbert α} [H.IncludeLEM] : LO.System.HasAxiomLEM H

Equations

• LO.IntProp.Hilbert.instHasAxiomLEMFormulaOfIncludeLEM = { lem := fun (x : LO.IntProp.Formula α) => LO.IntProp.Hilbert.Deduction.eaxm ⋯ }

instance LO.IntProp.Hilbert.instHasAxiomDNEFormulaOfIncludeDNE {α : Type u} {H : LO.IntProp.Hilbert α} [H.IncludeDNE] : LO.System.HasAxiomDNE H

Equations

• LO.IntProp.Hilbert.instHasAxiomDNEFormulaOfIncludeDNE = { dne := fun (x : LO.IntProp.Formula α) => LO.IntProp.Hilbert.Deduction.eaxm ⋯ }

instance LO.IntProp.Hilbert.instIntuitionisticFormulaOfIncludeEFQ {α : Type u} {H : LO.IntProp.Hilbert α} [H.IncludeEFQ] : LO.System.Intuitionistic H

Equations

• LO.IntProp.Hilbert.instIntuitionisticFormulaOfIncludeEFQ = LO.System.Intuitionistic.mk

instance LO.IntProp.Hilbert.instClassicalFormulaOfIncludeDNE {α : Type u} {H : LO.IntProp.Hilbert α} [H.IncludeDNE] : LO.System.Classical H

Equations

• LO.IntProp.Hilbert.instClassicalFormulaOfIncludeDNE = LO.System.Classical.mk

instance LO.IntProp.Hilbert.instClassicalFormulaOfDecidableEqOfIncludeEFQOfIncludeLEM {α : Type u} {H : LO.IntProp.Hilbert α} [DecidableEq α] [H.IncludeEFQ] [H.IncludeLEM] : LO.System.Classical H

Equations

• LO.IntProp.Hilbert.instClassicalFormulaOfDecidableEqOfIncludeEFQOfIncludeLEM = LO.System.Classical.mk

@[reducible, inline]

abbrev LO.IntProp.Hilbert.theorems {α : Type u} (H : LO.IntProp.Hilbert α) : Set (LO.IntProp.Formula α)

Equations

• H.theorems = LO.System.theory H

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Minimal (α : Type u) : LO.IntProp.Hilbert α

Equations

• LO.IntProp.Hilbert.Minimal α = { axioms := ∅ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Int (α : Type u) : LO.IntProp.Hilbert α

Equations

• LO.IntProp.Hilbert.Int α = { axioms := 𝗘𝗙𝗤 }

instance LO.IntProp.Hilbert.instIncludeEFQInt (α : Type u) : (LO.IntProp.Hilbert.Int α).IncludeEFQ

Equations

• ⋯ = ⋯

instance LO.IntProp.Hilbert.instIntuitionisticFormulaInt (α : Type u) : LO.System.Intuitionistic (LO.IntProp.Hilbert.Int α)

Equations

• LO.IntProp.Hilbert.instIntuitionisticFormulaInt α = LO.System.Intuitionistic.mk

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Cl (α : Type u) : LO.IntProp.Hilbert α

Equations

• LO.IntProp.Hilbert.Cl α = { axioms := 𝗘𝗙𝗤 ∪ 𝗟𝗘𝗠 }

instance LO.IntProp.Hilbert.instIncludeLEMCl (α : Type u) : (LO.IntProp.Hilbert.Cl α).IncludeLEM

Equations

• ⋯ = ⋯

instance LO.IntProp.Hilbert.instIncludeEFQCl (α : Type u) : (LO.IntProp.Hilbert.Cl α).IncludeEFQ

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev LO.IntProp.Hilbert.KC (α : Type u) : LO.IntProp.Hilbert α

KC from Chagrov & Zakharyaschev (1997)

Equations

• LO.IntProp.Hilbert.KC α = { axioms := 𝗘𝗙𝗤 ∪ 𝗪𝗟𝗘𝗠 }

instance LO.IntProp.Hilbert.instIncludeEFQKC (α : Type u) : (LO.IntProp.Hilbert.KC α).IncludeEFQ

Equations

• ⋯ = ⋯

instance LO.IntProp.Hilbert.instHasAxiomWeakLEMFormulaKC (α : Type u) : LO.System.HasAxiomWeakLEM (LO.IntProp.Hilbert.KC α)

Equations

• LO.IntProp.Hilbert.instHasAxiomWeakLEMFormulaKC α = { wlem := fun (φ : LO.IntProp.Formula α) => LO.IntProp.Hilbert.Deduction.eaxm ⋯ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.LC (α : Type u) : LO.IntProp.Hilbert α

LC from Chagrov & Zakharyaschev (1997)

Equations

• LO.IntProp.Hilbert.LC α = { axioms := 𝗘𝗙𝗤 ∪ 𝗗𝘂𝗺 }

instance LO.IntProp.Hilbert.instIncludeEFQLC (α : Type u) : (LO.IntProp.Hilbert.LC α).IncludeEFQ

Equations

• ⋯ = ⋯

instance LO.IntProp.Hilbert.instHasAxiomDummettFormulaLC (α : Type u) : LO.System.HasAxiomDummett (LO.IntProp.Hilbert.LC α)

Equations

• LO.IntProp.Hilbert.instHasAxiomDummettFormulaLC α = { dummett := fun (φ ψ : LO.IntProp.Formula α) => LO.IntProp.Hilbert.Deduction.eaxm ⋯ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.WeakMinimal (α : Type u) : LO.IntProp.Hilbert α

WeakMinimal from Ariola (2007)

Equations

• LO.IntProp.Hilbert.WeakMinimal α = { axioms := 𝗟𝗘𝗠 }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.WeakClassical (α : Type u) : LO.IntProp.Hilbert α

WeakClassical from Ariola (2007)

Equations

• LO.IntProp.Hilbert.WeakClassical α = { axioms := 𝗣𝗲 }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Consistent {α : Type u} (H : LO.IntProp.Hilbert α) : Prop

Equations

• H.Consistent = LO.System.Consistent H

theorem LO.IntProp.Hilbert.Deduction.eaxm! {α : Type u} {H : LO.IntProp.Hilbert α} {φ : LO.IntProp.Formula α} (h : φ ∈ H.axioms) : H ⊢! φ

noncomputable def LO.IntProp.Hilbert.Deduction.rec! {α : Type u} {H : LO.IntProp.Hilbert α} {motive : (a : LO.IntProp.Formula α) → H ⊢! a → Sort u_1} (eaxm : {φ : LO.IntProp.Formula α} → (a : φ ∈ H.axioms) → motive φ ⋯) (mdp : {φ ψ : LO.IntProp.Formula α} → {hpq : H ⊢! φ ➝ ψ} → {hp : H ⊢! φ} → motive (φ ➝ ψ) hpq → motive φ hp → motive ψ ⋯) (verum : motive ⊤ ⋯) (imply₁ : {φ ψ : LO.IntProp.Formula α} → motive (φ ➝ ψ ➝ φ) ⋯) (imply₂ : {φ ψ χ : LO.IntProp.Formula α} → motive ((φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ) ⋯) (and₁ : {φ ψ : LO.IntProp.Formula α} → motive (φ ⋏ ψ ➝ φ) ⋯) (and₂ : {φ ψ : LO.IntProp.Formula α} → motive (φ ⋏ ψ ➝ ψ) ⋯) (and₃ : {φ ψ : LO.IntProp.Formula α} → motive (φ ➝ ψ ➝ φ ⋏ ψ) ⋯) (or₁ : {φ ψ : LO.IntProp.Formula α} → motive (φ ➝ φ ⋎ ψ) ⋯) (or₂ : {φ ψ : LO.IntProp.Formula α} → motive (ψ ➝ φ ⋎ ψ) ⋯) (or₃ : {φ ψ χ : LO.IntProp.Formula α} → motive ((φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ) ⋯) (neg_equiv : {φ : LO.IntProp.Formula α} → motive (LO.Axioms.NegEquiv φ) ⋯) {a : LO.IntProp.Formula α} (t : H ⊢! a) : motive a t

Equations

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

theorem LO.IntProp.Hilbert.weaker_than_of_subset_axiomset' {α : Type u} {H₁ H₂ : LO.IntProp.Hilbert α} (hMaxm : ∀ {φ : LO.IntProp.Formula α}, φ ∈ H₁.axioms → H₂ ⊢! φ) : H₁ ≤ₛ H₂

theorem LO.IntProp.Hilbert.weaker_than_of_subset_axiomset {α : Type u} {H₁ H₂ : LO.IntProp.Hilbert α} (hSubset : H₁.axioms ⊆ H₂.axioms := by aesop) : H₁ ≤ₛ H₂

theorem LO.IntProp.Hilbert.Int_weaker_than_Cl {α : Type u} : LO.IntProp.Hilbert.Int α ≤ₛ LO.IntProp.Hilbert.Cl α

theorem LO.IntProp.Hilbert.Int_weaker_than_KC {α : Type u} : LO.IntProp.Hilbert.Int α ≤ₛ LO.IntProp.Hilbert.KC α

theorem LO.IntProp.Hilbert.Int_weaker_than_LC {α : Type u} : LO.IntProp.Hilbert.Int α ≤ₛ LO.IntProp.Hilbert.LC α

theorem LO.IntProp.Hilbert.KC_weaker_than_Cl {α : Type u} : LO.IntProp.Hilbert.KC α ≤ₛ LO.IntProp.Hilbert.Cl α

theorem LO.IntProp.Hilbert.LC_weaker_than_Cl {α : Type u} [DecidableEq α] : LO.IntProp.Hilbert.LC α ≤ₛ LO.IntProp.Hilbert.Cl α

theorem LO.IntProp.Hilbert.KC_weaker_than_LC {α : Type u} [DecidableEq α] : LO.IntProp.Hilbert.KC α ≤ₛ LO.IntProp.Hilbert.LC α