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

• axioms : Theory α

Instances For

• LO.IntProp.Hilbert.instSystemFormula

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

• include_EFQ : 𝗘𝗙𝗤 ⊆ H.axioms

Instances

• LO.IntProp.Hilbert.instIncludeEFQCl
• LO.IntProp.Hilbert.instIncludeEFQInt
• LO.IntProp.Hilbert.instIncludeEFQKC
• LO.IntProp.Hilbert.instIncludeEFQLC

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

• include_LEM : 𝗟𝗘𝗠 ⊆ H.axioms

Instances

• LO.IntProp.Hilbert.instIncludeLEMCl

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

• include_DNE : 𝗗𝗡𝗘 ⊆ H.axioms

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

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

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

Equations

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

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

Equations

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

instance LO.IntProp.Hilbert.instHasAxiomEFQFormulaOfIncludeEFQ {α : Type u} {H : Hilbert α} [H.IncludeEFQ] : 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 : Hilbert α} [H.IncludeLEM] : 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 : Hilbert α} [H.IncludeDNE] : 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 : Hilbert α} [H.IncludeEFQ] : System.Intuitionistic H

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

• H.theorems = LO.System.theory H

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.IntProp.Hilbert.Int.Kripke.complete
• LO.IntProp.Hilbert.Int.Kripke.sound
• LO.IntProp.Hilbert.Int.instConsistentNat
• LO.IntProp.Hilbert.Int.instDisjunctiveFormulaNat
• LO.IntProp.Hilbert.instIncludeEFQInt
• LO.IntProp.Hilbert.instIntuitionisticFormulaInt
• LO.Modal.instModalCompanionNatIntS4

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

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

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.IntProp.Hilbert.Cl.Kripke.sound
• LO.IntProp.Hilbert.Cl.instConsistentNat
• LO.IntProp.Hilbert.instIncludeEFQCl
• LO.IntProp.Hilbert.instIncludeLEMCl

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

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

@[reducible, inline]

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

KC from Chagrov & Zakharyaschev (1997)

Equations

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

Instances For

• LO.IntProp.Hilbert.KC.Kripke.complete
• LO.IntProp.Hilbert.KC.Kripke.sound
• LO.IntProp.Hilbert.KC.instConsistentNat
• LO.IntProp.Hilbert.instHasAxiomWeakLEMFormulaKC
• LO.IntProp.Hilbert.instIncludeEFQKC

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

instance LO.IntProp.Hilbert.instHasAxiomWeakLEMFormulaKC (α : Type u) : System.HasAxiomWeakLEM (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) : Hilbert α

LC from Chagrov & Zakharyaschev (1997)

Equations

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

Instances For

• LO.IntProp.Hilbert.LC.Kripke.complete
• LO.IntProp.Hilbert.LC.Kripke.sound
• LO.IntProp.Hilbert.LC.instConsistentNat
• LO.IntProp.Hilbert.instHasAxiomDummettFormulaLC
• LO.IntProp.Hilbert.instIncludeEFQLC

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

instance LO.IntProp.Hilbert.instHasAxiomDummettFormulaLC (α : Type u) : System.HasAxiomDummett (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) : Hilbert α

WeakMinimal from Ariola (2007)

Equations

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

@[reducible, inline]

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

WeakClassical from Ariola (2007)

Equations

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

@[reducible, inline]

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

Equations

• H.Consistent = LO.System.Consistent H

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

noncomputable def LO.IntProp.Hilbert.Deduction.rec! {α : Type u} {H : Hilbert α} {motive : (a : Formula α) → H ⊢! a → Sort u_1} (eaxm : {φ : Formula α} → (a : φ ∈ H.axioms) → motive φ ⋯) (mdp : {φ ψ : Formula α} → {hpq : H ⊢! φ ➝ ψ} → {hp : H ⊢! φ} → motive (φ ➝ ψ) hpq → motive φ hp → motive ψ ⋯) (verum : motive ⊤ ⋯) (imply₁ : {φ ψ : Formula α} → motive (φ ➝ ψ ➝ φ) ⋯) (imply₂ : {φ ψ χ : Formula α} → motive ((φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ) ⋯) (and₁ : {φ ψ : Formula α} → motive (φ ⋏ ψ ➝ φ) ⋯) (and₂ : {φ ψ : Formula α} → motive (φ ⋏ ψ ➝ ψ) ⋯) (and₃ : {φ ψ : Formula α} → motive (φ ➝ ψ ➝ φ ⋏ ψ) ⋯) (or₁ : {φ ψ : Formula α} → motive (φ ➝ φ ⋎ ψ) ⋯) (or₂ : {φ ψ : Formula α} → motive (ψ ➝ φ ⋎ ψ) ⋯) (or₃ : {φ ψ χ : Formula α} → motive ((φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ) ⋯) (neg_equiv : {φ : Formula α} → motive (Axioms.NegEquiv φ) ⋯) {a : 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₂ : Hilbert α} (hMaxm : ∀ {φ : Formula α}, φ ∈ H₁.axioms → H₂ ⊢! φ) : H₁ ≤ₛ H₂

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

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

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

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

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

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

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