structure LO.Modal.InferenceRule (α : Type u_2) : Type u_2

instance of inference rule

• antecedents : List (LO.Modal.Formula α)
• antecedents_nonempty : self.antecedents ≠ []

  Empty antecedent rule can be simply regarded as axiom rule. However, union of all these rules including to Hilbert.rules would be too complex for implementation and induction, so more than one antecedent is required.

• consequence : LO.Modal.Formula α

theorem LO.Modal.InferenceRule.antecedents_nonempty {α : Type u_2} (self : LO.Modal.InferenceRule α) : self.antecedents ≠ []

Empty antecedent rule can be simply regarded as axiom rule. However, union of all these rules including to Hilbert.rules would be too complex for implementation and induction, so more than one antecedent is required.

@[reducible, inline]

abbrev LO.Modal.InferenceRules (α : Type u_2) : Type u_2

Equations

• LO.Modal.InferenceRules α = Set (LO.Modal.InferenceRule α)

@[reducible, inline]

abbrev LO.Modal.Necessitation {α : Type u_2} : LO.Modal.InferenceRules α

Equations

• ⟮Nec⟯ = {x : LO.Modal.InferenceRule α | ∃ (p : LO.Modal.Formula α), { antecedents := [p], antecedents_nonempty := ⋯, consequence := □p } = x}

def LO.Modal.«term⟮Nec⟯» : Lean.ParserDescr

Equations

• LO.Modal.«term⟮Nec⟯» = Lean.ParserDescr.node `LO.Modal.term⟮Nec⟯ 1024 (Lean.ParserDescr.symbol "⟮Nec⟯")

@[reducible, inline]

abbrev LO.Modal.LoebRule {α : Type u_2} : LO.Modal.InferenceRules α

Equations

• ⟮Loeb⟯ = {x : LO.Modal.InferenceRule α | ∃ (p : LO.Modal.Formula α), { antecedents := [□p ➝ p], antecedents_nonempty := ⋯, consequence := p } = x}

def LO.Modal.«term⟮Loeb⟯» : Lean.ParserDescr

Equations

• LO.Modal.«term⟮Loeb⟯» = Lean.ParserDescr.node `LO.Modal.term⟮Loeb⟯ 1024 (Lean.ParserDescr.symbol "⟮Loeb⟯")

@[reducible, inline]

abbrev LO.Modal.HenkinRule {α : Type u_2} : LO.Modal.InferenceRules α

Equations

• ⟮Henkin⟯ = {x : LO.Modal.InferenceRule α | ∃ (p : LO.Modal.Formula α), { antecedents := [□p ⭤ p], antecedents_nonempty := ⋯, consequence := p } = x}

def LO.Modal.«term⟮Henkin⟯» : Lean.ParserDescr

Equations

• LO.Modal.«term⟮Henkin⟯» = Lean.ParserDescr.node `LO.Modal.term⟮Henkin⟯ 1024 (Lean.ParserDescr.symbol "⟮Henkin⟯")

structure LO.Modal.Hilbert (α : Type u_2) : Type u_2

• axioms : LO.Modal.Theory α
• rules : LO.Modal.InferenceRules α

def LO.Modal.«termAx(_)» : Lean.ParserDescr

Equations

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

def LO.Modal.«termRl(_)» : Lean.ParserDescr

Equations

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

inductive LO.Modal.Deduction {α : Type u_1} (Λ : LO.Modal.Hilbert α) : LO.Modal.Formula α → Type u_1

• maxm: {α : Type u_1} → {Λ : LO.Modal.Hilbert α} → {p : LO.Modal.Formula α} → p ∈ Ax(Λ) → LO.Modal.Deduction Λ p
• rule: {α : Type u_1} → {Λ : LO.Modal.Hilbert α} → {rl : LO.Modal.InferenceRule α} → rl ∈ Rl(Λ) → ({p : LO.Modal.Formula α} → p ∈ rl.antecedents → LO.Modal.Deduction Λ p) → LO.Modal.Deduction Λ rl.consequence
• mdp: {α : Type u_1} → {Λ : LO.Modal.Hilbert α} → {p q : LO.Modal.Formula α} → LO.Modal.Deduction Λ (p ➝ q) → LO.Modal.Deduction Λ p → LO.Modal.Deduction Λ q
• imply₁: {α : Type u_1} → {Λ : LO.Modal.Hilbert α} → (p q : LO.Modal.Formula α) → LO.Modal.Deduction Λ (LO.Axioms.Imply₁ p q)
• imply₂: {α : Type u_1} → {Λ : LO.Modal.Hilbert α} → (p q r : LO.Modal.Formula α) → LO.Modal.Deduction Λ (LO.Axioms.Imply₂ p q r)
• ec: {α : Type u_1} → {Λ : LO.Modal.Hilbert α} → (p q : LO.Modal.Formula α) → LO.Modal.Deduction Λ (LO.Axioms.ElimContra p q)

instance LO.Modal.Deduction.instSystemFormulaHilbert {α : Type u_1} : LO.System (LO.Modal.Formula α) (LO.Modal.Hilbert α)

Equations

• LO.Modal.Deduction.instSystemFormulaHilbert = { Prf := LO.Modal.Deduction }

instance LO.Modal.Deduction.instLukasiewiczHilbertFormula {α : Type u_1} {Λ : LO.Modal.Hilbert α} : LO.System.Lukasiewicz Λ

Equations

• LO.Modal.Deduction.instLukasiewiczHilbertFormula = LO.System.Lukasiewicz.mk

instance LO.Modal.Deduction.instClassicalHilbertFormula {α : Type u_1} {Λ : LO.Modal.Hilbert α} : LO.System.Classical Λ

Equations

• LO.Modal.Deduction.instClassicalHilbertFormula = LO.System.Classical.mk

instance LO.Modal.Deduction.instHasDiaDualityHilbertFormula {α : Type u_1} {Λ : LO.Modal.Hilbert α} : LO.System.HasDiaDuality Λ

Equations

• LO.Modal.Deduction.instHasDiaDualityHilbertFormula = inferInstance

theorem LO.Modal.Deduction.maxm! {α : Type u_1} {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} (h : p ∈ Ax(Λ)) : Λ ⊢! p

class LO.Modal.Hilbert.HasNecessitation {α : Type u_1} (Λ : LO.Modal.Hilbert α) : Type

• has_necessitation : ⟮Nec⟯ ⊆ Rl(Λ)

theorem LO.Modal.Hilbert.HasNecessitation.has_necessitation {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasNecessitation] : ⟮Nec⟯ ⊆ Rl(Λ)

instance LO.Modal.Hilbert.instNecessitationFormulaOfHasNecessitation : {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [inst : Λ.HasNecessitation] → LO.System.Necessitation Λ

Equations

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

class LO.Modal.Hilbert.HasLoebRule {α : Type u_1} (Λ : LO.Modal.Hilbert α) : Type

• has_loeb : ⟮Loeb⟯ ⊆ Rl(Λ)

theorem LO.Modal.Hilbert.HasLoebRule.has_loeb {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasLoebRule] : ⟮Loeb⟯ ⊆ Rl(Λ)

instance LO.Modal.Hilbert.instLoebRuleFormulaOfHasLoebRule : {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [inst : Λ.HasLoebRule] → LO.System.LoebRule Λ

Equations

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

class LO.Modal.Hilbert.HasHenkinRule {α : Type u_1} (Λ : LO.Modal.Hilbert α) : Type

• has_henkin : ⟮Henkin⟯ ⊆ Rl(Λ)

theorem LO.Modal.Hilbert.HasHenkinRule.has_henkin {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasHenkinRule] : ⟮Henkin⟯ ⊆ Rl(Λ)

instance LO.Modal.Hilbert.instHenkinRuleFormulaOfHasHenkinRule : {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [inst : Λ.HasHenkinRule] → LO.System.HenkinRule Λ

Equations

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

class LO.Modal.Hilbert.HasNecOnly {α : Type u_1} (Λ : LO.Modal.Hilbert α) : Type

• has_necessitation_only : Rl(Λ) = ⟮Nec⟯

theorem LO.Modal.Hilbert.HasNecOnly.has_necessitation_only {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasNecOnly] : Rl(Λ) = ⟮Nec⟯

instance LO.Modal.Hilbert.instHasNecessitationOfHasNecOnly : {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [h : Λ.HasNecOnly] → Λ.HasNecessitation

Equations

• LO.Modal.Hilbert.instHasNecessitationOfHasNecOnly = { has_necessitation := ⋯ }

class LO.Modal.Hilbert.HasAxiomK {α : Type u_1} (Λ : LO.Modal.Hilbert α) : Type

• has_axiomK : 𝗞 ⊆ Ax(Λ)

theorem LO.Modal.Hilbert.HasAxiomK.has_axiomK {α : Type u_1} {Λ : LO.Modal.Hilbert α} [self : Λ.HasAxiomK] : 𝗞 ⊆ Ax(Λ)

instance LO.Modal.Hilbert.instHasAxiomKFormulaOfHasAxiomK : {α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [inst : Λ.HasAxiomK] → LO.System.HasAxiomK Λ

Equations

• LO.Modal.Hilbert.instHasAxiomKFormulaOfHasAxiomK = { K := fun (x x_1 : LO.Modal.Formula α) => LO.Modal.Deduction.maxm ⋯ }

class LO.Modal.Hilbert.IsNormal {α : Type u_1} (Λ : LO.Modal.Hilbert α) extends LO.Modal.Hilbert.HasNecOnly , LO.Modal.Hilbert.HasAxiomK : Type

noncomputable def LO.Modal.Deduction.inducition! {α : Type u_1} {Λ : LO.Modal.Hilbert α} {motive : (p : LO.Modal.Formula α) → Λ ⊢! p → Sort u_2} (hRules : (r : LO.Modal.InferenceRule α) → (hr : r ∈ Rl(Λ)) → (hant : ∀ {p : LO.Modal.Formula α}, p ∈ r.antecedents → Λ ⊢! p) → ({p : LO.Modal.Formula α} → (hp : p ∈ r.antecedents) → motive p ⋯) → motive r.consequence ⋯) (hMaxm : {p : LO.Modal.Formula α} → (h : p ∈ Ax(Λ)) → motive p ⋯) (hMdp : {p q : LO.Modal.Formula α} → {hpq : Λ ⊢! p ➝ q} → {hp : Λ ⊢! p} → motive (p ➝ q) hpq → motive p hp → motive q ⋯) (hImply₁ : {p q : LO.Modal.Formula α} → motive (p ➝ q ➝ p) ⋯) (hImply₂ : {p q r : LO.Modal.Formula α} → motive ((p ➝ q ➝ r) ➝ (p ➝ q) ➝ p ➝ r) ⋯) (hElimContra : {p q : LO.Modal.Formula α} → motive (LO.Axioms.ElimContra p q) ⋯) {p : LO.Modal.Formula α} (d : Λ ⊢! p) : motive p d

Equations

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

noncomputable def LO.Modal.Deduction.inducition_with_necOnly! {α : Type u_1} {Λ : LO.Modal.Hilbert α} [Λ.HasNecOnly] {motive : (p : LO.Modal.Formula α) → Λ ⊢! p → Prop} (hMaxm : ∀ {p : LO.Modal.Formula α} (h : p ∈ Ax(Λ)), motive p ⋯) (hMdp : ∀ {p q : LO.Modal.Formula α} {hpq : Λ ⊢! p ➝ q} {hp : Λ ⊢! p}, motive (p ➝ q) hpq → motive p hp → motive q ⋯) (hNec : ∀ {p : LO.Modal.Formula α} {hp : Λ ⊢! p}, motive p hp → motive (□p) ⋯) (hImply₁ : ∀ {p q : LO.Modal.Formula α}, motive (p ➝ q ➝ p) ⋯) (hImply₂ : ∀ {p q r : LO.Modal.Formula α}, motive ((p ➝ q ➝ r) ➝ (p ➝ q) ➝ p ➝ r) ⋯) (hElimContra : ∀ {p q : LO.Modal.Formula α}, motive (LO.Axioms.ElimContra p q) ⋯) {p : LO.Modal.Formula α} (d : Λ ⊢! p) : motive p d

Useful induction for normal modal logic.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev LO.Modal.Hilbert.theorems {α : Type u_1} (Λ : LO.Modal.Hilbert α) : Set (LO.Modal.Formula α)

Equations

• Λ.theorems = LO.System.theory Λ

@[reducible, inline]

abbrev LO.Modal.K {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊 = { axioms := 𝗞, rules := ⟮Nec⟯ }

def LO.Modal.«term𝐊» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊» = Lean.ParserDescr.node `LO.Modal.term𝐊 1024 (Lean.ParserDescr.symbol "𝐊")

instance LO.Modal.instIsNormalK {α : Type u_1} : 𝐊.IsNormal

Equations

• LO.Modal.instIsNormalK = LO.Modal.Hilbert.IsNormal.mk

@[reducible, inline]

abbrev LO.Modal.Normal {α : Type u_1} (Ax : LO.Modal.Theory α) : LO.Modal.Hilbert α

Equations

• 𝝂Ax = { axioms := 𝗞 ∪ Ax, rules := ⟮Nec⟯ }

instance LO.Modal.instIsNormalNormal {α : Type u_1} {Ax : LO.Modal.Theory α} : (𝝂Ax).IsNormal

Equations

• LO.Modal.instIsNormalNormal = LO.Modal.Hilbert.IsNormal.mk

def LO.Modal.«term𝝂_» : Lean.ParserDescr

Equations

• LO.Modal.«term𝝂_» = Lean.ParserDescr.node `LO.Modal.term𝝂_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝝂") (Lean.ParserDescr.cat `term 1024))

theorem LO.Modal.K_is_empty_normal {α : Type u_1} : 𝐊 = 𝝂∅

theorem LO.Modal.K_is_K_normal {α : Type u_1} : 𝐊 = 𝝂𝗞

theorem LO.Modal.Normal.def_ax {α : Type u_1} {Ax : LO.Modal.Theory α} : Ax(𝝂Ax) = 𝗞 ∪ Ax

theorem LO.Modal.Normal.maxm! {α : Type u_1} {Ax : LO.Modal.Theory α} {p : LO.Modal.Formula α} (h : p ∈ Ax) : 𝝂Ax ⊢! p

@[reducible, inline]

abbrev LO.Modal.KT {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝐓 = 𝝂𝗧

def LO.Modal.«term𝐊𝐓» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝐓» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐓 1024 (Lean.ParserDescr.symbol "𝐊𝐓")

@[reducible, inline]

abbrev LO.Modal.KB {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝐁 = 𝝂𝗕

def LO.Modal.«term𝐊𝐁» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝐁» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐁 1024 (Lean.ParserDescr.symbol "𝐊𝐁")

@[reducible, inline]

abbrev LO.Modal.KD {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝐃 = 𝝂𝗗

def LO.Modal.«term𝐊𝐃» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝐃» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐃 1024 (Lean.ParserDescr.symbol "𝐊𝐃")

instance LO.Modal.instKDHilbertFormulaKD {α : Type u_1} : LO.System.KD 𝐊𝐃

Equations

• LO.Modal.instKDHilbertFormulaKD = LO.System.KD.mk

@[reducible, inline]

abbrev LO.Modal.KD₂ {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝐃(⊥) = 𝝂𝗗(⊥)

def LO.Modal.«term𝐊𝐃(⊥)» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝐃(⊥)» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐃(⊥) 1024 (Lean.ParserDescr.symbol "𝐊𝐃(⊥)")

instance LO.Modal.instHasAxiomD₂HilbertFormulaKD₂ {α : Type u_1} : LO.System.HasAxiomD₂ 𝐊𝐃(⊥)

Equations

• LO.Modal.instHasAxiomD₂HilbertFormulaKD₂ = { D₂ := LO.Modal.Deduction.maxm ⋯ }

@[reducible, inline]

abbrev LO.Modal.KTB {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝐓𝐁 = 𝝂(𝗧 ∪ 𝗕)

def LO.Modal.«term𝐊𝐓𝐁» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝐓𝐁» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐓𝐁 1024 (Lean.ParserDescr.symbol "𝐊𝐓𝐁")

@[reducible, inline]

abbrev LO.Modal.K4 {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝟒 = 𝝂𝟰

def LO.Modal.«term𝐊𝟒» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝟒» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟒 1024 (Lean.ParserDescr.symbol "𝐊𝟒")

instance LO.Modal.instK4HilbertFormulaK4 {α : Type u_1} : LO.System.K4 𝐊𝟒

Equations

• LO.Modal.instK4HilbertFormulaK4 = LO.System.K4.mk

@[reducible, inline]

abbrev LO.Modal.K5 {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝟓 = 𝝂𝟱

def LO.Modal.«term𝐊𝟓» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝟓» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟓 1024 (Lean.ParserDescr.symbol "𝐊𝟓")

@[reducible, inline]

abbrev LO.Modal.KT4B {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝐓𝟒𝐁 = 𝝂(𝗧 ∪ 𝟰 ∪ 𝗕)

def LO.Modal.«term𝐊𝐓𝟒𝐁» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝐓𝟒𝐁» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐓𝟒𝐁 1024 (Lean.ParserDescr.symbol "𝐊𝐓𝟒𝐁")

@[reducible, inline]

abbrev LO.Modal.S4 {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐒𝟒 = 𝝂(𝗧 ∪ 𝟰)

def LO.Modal.«term𝐒𝟒» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐒𝟒» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟒 1024 (Lean.ParserDescr.symbol "𝐒𝟒")

instance LO.Modal.instS4HilbertFormulaS4 {α : Type u_1} : LO.System.S4 𝐒𝟒

Equations

• LO.Modal.instS4HilbertFormulaS4 = LO.System.S4.mk

@[reducible, inline]

abbrev LO.Modal.S4Dot2 {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐒𝟒.𝟐 = 𝝂(𝗧 ∪ 𝟰 ∪ .𝟮)

def LO.Modal.«term𝐒𝟒.𝟐» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐒𝟒.𝟐» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟒.𝟐 1024 (Lean.ParserDescr.symbol "𝐒𝟒.𝟐")

@[reducible, inline]

abbrev LO.Modal.S4Dot3 {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐒𝟒.𝟑 = 𝝂(𝗧 ∪ 𝟰 ∪ .𝟯)

def LO.Modal.«term𝐒𝟒.𝟑» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐒𝟒.𝟑» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟒.𝟑 1024 (Lean.ParserDescr.symbol "𝐒𝟒.𝟑")

@[reducible, inline]

abbrev LO.Modal.S4Grz {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐒𝟒𝐆𝐫𝐳 = 𝝂(𝗧 ∪ 𝟰 ∪ 𝗚𝗿𝘇)

def LO.Modal.«term𝐒𝟒𝐆𝐫𝐳» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐒𝟒𝐆𝐫𝐳» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟒𝐆𝐫𝐳 1024 (Lean.ParserDescr.symbol "𝐒𝟒𝐆𝐫𝐳")

@[reducible, inline]

abbrev LO.Modal.S5 {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐒𝟓 = 𝝂(𝗧 ∪ 𝟱)

def LO.Modal.«term𝐒𝟓» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐒𝟓» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟓 1024 (Lean.ParserDescr.symbol "𝐒𝟓")

instance LO.Modal.instIsNormalS5 {α : Type u_1} : 𝐒𝟓.IsNormal

Equations

• LO.Modal.instIsNormalS5 = LO.Modal.Hilbert.IsNormal.mk

@[reducible, inline]

abbrev LO.Modal.Triv {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐓𝐫𝐢𝐯 = 𝝂(𝗧 ∪ 𝗧𝗰)

def LO.Modal.«term𝐓𝐫𝐢𝐯» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐓𝐫𝐢𝐯» = Lean.ParserDescr.node `LO.Modal.term𝐓𝐫𝐢𝐯 1024 (Lean.ParserDescr.symbol "𝐓𝐫𝐢𝐯")

instance LO.Modal.instTrivHilbertFormulaTriv {α : Type u_1} : LO.System.Triv 𝐓𝐫𝐢𝐯

Equations

• LO.Modal.instTrivHilbertFormulaTriv = LO.System.Triv.mk

@[reducible, inline]

abbrev LO.Modal.Ver {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐕𝐞𝐫 = 𝝂𝗩𝗲𝗿

def LO.Modal.«term𝐕𝐞𝐫» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐕𝐞𝐫» = Lean.ParserDescr.node `LO.Modal.term𝐕𝐞𝐫 1024 (Lean.ParserDescr.symbol "𝐕𝐞𝐫")

instance LO.Modal.instVerHilbertFormulaVer {α : Type u_1} : LO.System.Ver 𝐕𝐞𝐫

Equations

• LO.Modal.instVerHilbertFormulaVer = LO.System.Ver.mk

@[reducible, inline]

abbrev LO.Modal.GL {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐆𝐋 = 𝝂𝗟

def LO.Modal.«term𝐆𝐋» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐆𝐋» = Lean.ParserDescr.node `LO.Modal.term𝐆𝐋 1024 (Lean.ParserDescr.symbol "𝐆𝐋")

instance LO.Modal.instGLHilbertFormulaGL {α : Type u_1} : LO.System.GL 𝐆𝐋

Equations

• LO.Modal.instGLHilbertFormulaGL = LO.System.GL.mk

@[reducible, inline]

abbrev LO.Modal.Grz {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐆𝐫𝐳 = 𝝂𝗚𝗿𝘇

def LO.Modal.«term𝐆𝐫𝐳» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐆𝐫𝐳» = Lean.ParserDescr.node `LO.Modal.term𝐆𝐫𝐳 1024 (Lean.ParserDescr.symbol "𝐆𝐫𝐳")

instance LO.Modal.instGrzHilbertFormulaGrz {α : Type u_1} : LO.System.Grz 𝐆𝐫𝐳

Equations

• LO.Modal.instGrzHilbertFormulaGrz = LO.System.Grz.mk

@[reducible, inline]

abbrev LO.Modal.K4H {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝟒𝐇 = 𝝂(𝟰 ∪ 𝗛)

def LO.Modal.«term𝐊𝟒𝐇» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝟒𝐇» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟒𝐇 1024 (Lean.ParserDescr.symbol "𝐊𝟒𝐇")

instance LO.Modal.instK4HHilbertFormulaK4H {α : Type u_1} : LO.System.K4H 𝐊𝟒𝐇

Equations

• LO.Modal.instK4HHilbertFormulaK4H = LO.System.K4H.mk

@[reducible, inline]

abbrev LO.Modal.K4Loeb {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝟒(𝐋) = { axioms := 𝗞 ∪ 𝟰, rules := ⟮Nec⟯ ∪ ⟮Loeb⟯ }

def LO.Modal.«term𝐊𝟒(𝐋)» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝟒(𝐋)» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟒(𝐋) 1024 (Lean.ParserDescr.symbol "𝐊𝟒(𝐋)")

instance LO.Modal.instHasAxiomKK4Loeb {α : Type u_1} : 𝐊𝟒(𝐋).HasAxiomK

Equations

• LO.Modal.instHasAxiomKK4Loeb = { has_axiomK := ⋯ }

instance LO.Modal.instHasNecessitationK4Loeb {α : Type u_1} : 𝐊𝟒(𝐋).HasNecessitation

Equations

• LO.Modal.instHasNecessitationK4Loeb = { has_necessitation := ⋯ }

instance LO.Modal.instHasLoebRuleK4Loeb {α : Type u_1} : 𝐊𝟒(𝐋).HasLoebRule

Equations

• LO.Modal.instHasLoebRuleK4Loeb = { has_loeb := ⋯ }

instance LO.Modal.instK4LoebHilbertFormulaK4Loeb {α : Type u_1} : LO.System.K4Loeb 𝐊𝟒(𝐋)

Equations

• LO.Modal.instK4LoebHilbertFormulaK4Loeb = LO.System.K4Loeb.mk

@[reducible, inline]

abbrev LO.Modal.K4Henkin {α : Type u_1} : LO.Modal.Hilbert α

Equations

• 𝐊𝟒(𝐇) = { axioms := 𝗞 ∪ 𝟰, rules := ⟮Nec⟯ ∪ ⟮Henkin⟯ }

def LO.Modal.«term𝐊𝟒(𝐇)» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐊𝟒(𝐇)» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟒(𝐇) 1024 (Lean.ParserDescr.symbol "𝐊𝟒(𝐇)")

instance LO.Modal.instHasAxiomKK4Henkin {α : Type u_1} : 𝐊𝟒(𝐇).HasAxiomK

Equations

• LO.Modal.instHasAxiomKK4Henkin = { has_axiomK := ⋯ }

instance LO.Modal.instHasNecessitationK4Henkin {α : Type u_1} : 𝐊𝟒(𝐇).HasNecessitation

Equations

• LO.Modal.instHasNecessitationK4Henkin = { has_necessitation := ⋯ }

instance LO.Modal.instHasHenkinRuleK4Henkin {α : Type u_1} : 𝐊𝟒(𝐇).HasHenkinRule

Equations

• LO.Modal.instHasHenkinRuleK4Henkin = { has_henkin := ⋯ }

instance LO.Modal.instK4HenkinHilbertFormulaK4Henkin {α : Type u_1} : LO.System.K4Henkin 𝐊𝟒(𝐇)

Equations

• LO.Modal.instK4HenkinHilbertFormulaK4Henkin = LO.System.K4Henkin.mk

@[reducible, inline]

abbrev LO.Modal.GLS {α : Type u_1} : LO.Modal.Hilbert α

Solovey's Provability Logic of True Arithmetic. Remark necessitation is not permitted.

Equations

• 𝐆𝐋𝐒 = { axioms := 𝐆𝐋.theorems ∪ 𝗧, rules := ∅ }

def LO.Modal.«term𝐆𝐋𝐒» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐆𝐋𝐒» = Lean.ParserDescr.node `LO.Modal.term𝐆𝐋𝐒 1024 (Lean.ParserDescr.symbol "𝐆𝐋𝐒")

instance LO.Modal.instHasAxiomKHilbertFormulaGLS {α : Type u_1} : LO.System.HasAxiomK 𝐆𝐋𝐒

Equations

• LO.Modal.instHasAxiomKHilbertFormulaGLS = { K := fun (x x_1 : LO.Modal.Formula α) => LO.Modal.Deduction.maxm ⋯ }

instance LO.Modal.instHasAxiomLHilbertFormulaGLS {α : Type u_1} : LO.System.HasAxiomL 𝐆𝐋𝐒

Equations

• LO.Modal.instHasAxiomLHilbertFormulaGLS = { L := fun (x : LO.Modal.Formula α) => LO.Modal.Deduction.maxm ⋯ }

instance LO.Modal.instHasAxiomTHilbertFormulaGLS {α : Type u_1} : LO.System.HasAxiomT 𝐆𝐋𝐒

Equations

• LO.Modal.instHasAxiomTHilbertFormulaGLS = { T := fun (x : LO.Modal.Formula α) => LO.Modal.Deduction.maxm ⋯ }

@[reducible, inline]

abbrev LO.Modal.N {α : Type u_1} : LO.Modal.Hilbert α

Logic of Pure Necessitation

Equations

• 𝐍 = { axioms := ∅, rules := ⟮Nec⟯ }

def LO.Modal.«term𝐍» : Lean.ParserDescr

Equations

• LO.Modal.«term𝐍» = Lean.ParserDescr.node `LO.Modal.term𝐍 1024 (Lean.ParserDescr.symbol "𝐍")

instance LO.Modal.instHasNecOnlyN {α : Type u_1} : 𝐍.HasNecOnly

Equations

• LO.Modal.instHasNecOnlyN = { has_necessitation_only := ⋯ }

theorem LO.Modal.normal_weakerThan_of_maxm {α : Type u_1} [DecidableEq α] {Λ₁ : LO.Modal.Hilbert α} {Λ₂ : LO.Modal.Hilbert α} [Λ₁.IsNormal] [Λ₂.IsNormal] (hMaxm : ∀ {p : LO.Modal.Formula α}, p ∈ Ax(Λ₁) → Λ₂ ⊢! p) : Λ₁ ≤ₛ Λ₂

theorem LO.Modal.normal_weakerThan_of_subset {α : Type u_1} [DecidableEq α] {Λ₁ : LO.Modal.Hilbert α} {Λ₂ : LO.Modal.Hilbert α} [Λ₁.IsNormal] [Λ₂.IsNormal] (hSubset : autoParam (Ax(Λ₁) ⊆ Ax(Λ₂)) _auto✝) : Λ₁ ≤ₛ Λ₂

theorem LO.Modal.K_weakerThan_KD {α : Type u_1} [DecidableEq α] : 𝐊 ≤ₛ 𝐊𝐃

theorem LO.Modal.K_weakerThan_KB {α : Type u_1} [DecidableEq α] : 𝐊 ≤ₛ 𝐊𝐁

theorem LO.Modal.K_weakerThan_KT {α : Type u_1} [DecidableEq α] : 𝐊 ≤ₛ 𝐊𝐓

theorem LO.Modal.K_weakerThan_K4 {α : Type u_1} [DecidableEq α] : 𝐊 ≤ₛ 𝐊𝟒

theorem LO.Modal.K_weakerThan_K5 {α : Type u_1} [DecidableEq α] : 𝐊 ≤ₛ 𝐊𝟓

theorem LO.Modal.KT_weakerThan_S4 {α : Type u_1} [DecidableEq α] : 𝐊𝐓 ≤ₛ 𝐒𝟒

theorem LO.Modal.K4_weakerThan_S4 {α : Type u_1} [DecidableEq α] : 𝐊𝟒 ≤ₛ 𝐒𝟒

theorem LO.Modal.S4_weakerThan_S4Dot2 {α : Type u_1} [DecidableEq α] : 𝐒𝟒 ≤ₛ 𝐒𝟒.𝟐

theorem LO.Modal.S4_weakerThan_S4Dot3 {α : Type u_1} [DecidableEq α] : 𝐒𝟒 ≤ₛ 𝐒𝟒.𝟑

theorem LO.Modal.S4_weakerThan_S4Grz {α : Type u_1} [DecidableEq α] : 𝐒𝟒 ≤ₛ 𝐒𝟒𝐆𝐫𝐳

theorem LO.Modal.K_weakerThan_GL {α : Type u_1} [DecidableEq α] : 𝐊 ≤ₛ 𝐆𝐋

theorem LO.Modal.K4_weakerThan_Triv {α : Type u_1} [DecidableEq α] : 𝐊𝟒 ≤ₛ 𝐓𝐫𝐢𝐯

theorem LO.Modal.K4_weakerThan_GL {α : Type u_1} [DecidableEq α] : 𝐊𝟒 ≤ₛ 𝐆𝐋

theorem LO.Modal.KT_weakerThan_Grz {α : Type u_1} [DecidableEq α] : 𝐊𝐓 ≤ₛ 𝐆𝐫𝐳

theorem LO.Modal.K4_weakerThan_Grz {α : Type u_1} [DecidableEq α] : 𝐊𝟒 ≤ₛ 𝐆𝐫𝐳

theorem LO.Modal.KD_weakerThan_KD₂ {α : Type u_1} [DecidableEq α] : 𝐊𝐃 ≤ₛ 𝐊𝐃(⊥)

theorem LO.Modal.KD₂_weakerThan_KD {α : Type u_1} [DecidableEq α] : 𝐊𝐃(⊥) ≤ₛ 𝐊𝐃

theorem LO.Modal.KD_equiv_KD₂ {α : Type u_1} [DecidableEq α] : 𝐊𝐃 =ₛ 𝐊𝐃(⊥)

theorem LO.Modal.GL_weakerThan_K4Loeb {α : Type u_1} [DecidableEq α] : 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)

theorem LO.Modal.K4Loeb_weakerThan_K4Henkin {α : Type u_1} [DecidableEq α] : 𝐊𝟒(𝐋) ≤ₛ 𝐊𝟒(𝐇)

theorem LO.Modal.K4Henkin_weakerThan_K4H {α : Type u_1} [DecidableEq α] : 𝐊𝟒(𝐇) ≤ₛ 𝐊𝟒𝐇

theorem LO.Modal.K4Henkin_weakerThan_GL {α : Type u_1} [DecidableEq α] : 𝐊𝟒𝐇 ≤ₛ 𝐆𝐋

theorem LO.Modal.GL_equiv_K4Loeb {α : Type u_1} [DecidableEq α] : 𝐆𝐋 =ₛ 𝐊𝟒(𝐋)

theorem LO.Modal.GL_weakerThan_GLS {α : Type u_1} : 𝐆𝐋 ≤ₛ 𝐆𝐋𝐒