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 α
Instances For
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]
Equations
Instances For
@[reducible, inline]
Equations
- ⟮Nec⟯ = {x : LO.Modal.InferenceRule α | ∃ (p : LO.Modal.Formula α), { antecedents := [p], antecedents_nonempty := ⋯, consequence := □p } = x}
Instances For
Equations
- LO.Modal.«term⟮Nec⟯» = Lean.ParserDescr.node `LO.Modal.term⟮Nec⟯ 1024 (Lean.ParserDescr.symbol "⟮Nec⟯")
Instances For
@[reducible, inline]
Equations
- ⟮Loeb⟯ = {x : LO.Modal.InferenceRule α | ∃ (p : LO.Modal.Formula α), { antecedents := [□p ➝ p], antecedents_nonempty := ⋯, consequence := p } = x}
Instances For
Equations
- LO.Modal.«term⟮Loeb⟯» = Lean.ParserDescr.node `LO.Modal.term⟮Loeb⟯ 1024 (Lean.ParserDescr.symbol "⟮Loeb⟯")
Instances For
@[reducible, inline]
Equations
- ⟮Henkin⟯ = {x : LO.Modal.InferenceRule α | ∃ (p : LO.Modal.Formula α), { antecedents := [□p ⭤ p], antecedents_nonempty := ⋯, consequence := p } = x}
Instances For
Equations
- LO.Modal.«term⟮Henkin⟯» = Lean.ParserDescr.node `LO.Modal.term⟮Henkin⟯ 1024 (Lean.ParserDescr.symbol "⟮Henkin⟯")
Instances For
- axioms : LO.Modal.Theory α
- rules : LO.Modal.InferenceRules α
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- 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)
Instances For
Equations
- LO.Modal.Deduction.instSystemFormulaHilbert = { Prf := LO.Modal.Deduction }
Equations
- LO.Modal.Deduction.instLukasiewiczHilbertFormula = LO.System.Lukasiewicz.mk
Equations
- LO.Modal.Deduction.instClassicalHilbertFormula = LO.System.Classical.mk
instance
LO.Modal.Deduction.instHasDiaDualityHilbertFormula
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
:
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
Instances
theorem
LO.Modal.Hilbert.HasNecessitation.has_necessitation
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
[self : Λ.HasNecessitation]
:
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.
Instances
theorem
LO.Modal.Hilbert.HasLoebRule.has_loeb
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
[self : Λ.HasLoebRule]
:
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.
Instances
theorem
LO.Modal.Hilbert.HasHenkinRule.has_henkin
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
[self : Λ.HasHenkinRule]
:
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.
Instances
theorem
LO.Modal.Hilbert.HasNecOnly.has_necessitation_only
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
[self : Λ.HasNecOnly]
:
instance
LO.Modal.Hilbert.instHasNecessitationOfHasNecOnly :
{α : Type u_2} → {Λ : LO.Modal.Hilbert α} → [h : Λ.HasNecOnly] → Λ.HasNecessitation
Equations
- LO.Modal.Hilbert.instHasNecessitationOfHasNecOnly = { has_necessitation := ⋯ }
Instances
theorem
LO.Modal.Hilbert.HasAxiomK.has_axiomK
{α : Type u_1}
{Λ : LO.Modal.Hilbert α}
[self : Λ.HasAxiomK]
:
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
:
Instances
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.
Instances For
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 Foundation.
Equations
- ⋯ = ⋯
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊» = Lean.ParserDescr.node `LO.Modal.term𝐊 1024 (Lean.ParserDescr.symbol "𝐊")
Instances For
Equations
- LO.Modal.instIsNormalK = LO.Modal.Hilbert.IsNormal.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.instIsNormalExtK = LO.Modal.Hilbert.IsNormal.mk
Equations
- LO.Modal.«term𝜿_» = Lean.ParserDescr.node `LO.Modal.term𝜿_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝜿") (Lean.ParserDescr.cat `term 1024))
Instances For
theorem
LO.Modal.Normal.maxm!
{α : Type u_1}
{Ax : LO.Modal.Theory α}
{p : LO.Modal.Formula α}
(h : p ∈ Ax)
:
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝝈_» = Lean.ParserDescr.node `LO.Modal.term𝝈_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝝈") (Lean.ParserDescr.cat `term 1024))
Instances For
instance
LO.Modal.instS4HilbertFormulaExtS4 :
{α : Type u_2} → {Ax : LO.Modal.Theory α} → LO.System.S4 𝝈Ax
Equations
- LO.Modal.instS4HilbertFormulaExtS4 = LO.System.S4.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝐓» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐓 1024 (Lean.ParserDescr.symbol "𝐊𝐓")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝐁» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐁 1024 (Lean.ParserDescr.symbol "𝐊𝐁")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝐃» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐃 1024 (Lean.ParserDescr.symbol "𝐊𝐃")
Instances For
Equations
- LO.Modal.instKDHilbertFormulaKD = LO.System.KD.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝐏» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐏 1024 (Lean.ParserDescr.symbol "𝐊𝐏")
Instances For
Equations
- LO.Modal.instHasAxiomPHilbertFormulaKP = { P := LO.Modal.Deduction.maxm ⋯ }
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝐓𝐁» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐓𝐁 1024 (Lean.ParserDescr.symbol "𝐊𝐓𝐁")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝟒» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟒 1024 (Lean.ParserDescr.symbol "𝐊𝟒")
Instances For
Equations
- LO.Modal.instK4HilbertFormulaK4 = LO.System.K4.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝟓» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟓 1024 (Lean.ParserDescr.symbol "𝐊𝟓")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐒𝟒» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟒 1024 (Lean.ParserDescr.symbol "𝐒𝟒")
Instances For
Equations
- LO.Modal.instS4HilbertFormulaS4 = LO.System.S4.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐒𝟒.𝟐» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟒.𝟐 1024 (Lean.ParserDescr.symbol "𝐒𝟒.𝟐")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐒𝟒.𝟑» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟒.𝟑 1024 (Lean.ParserDescr.symbol "𝐒𝟒.𝟑")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐒𝟒𝐆𝐫𝐳» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟒𝐆𝐫𝐳 1024 (Lean.ParserDescr.symbol "𝐒𝟒𝐆𝐫𝐳")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝐓𝟒𝐁» = Lean.ParserDescr.node `LO.Modal.term𝐊𝐓𝟒𝐁 1024 (Lean.ParserDescr.symbol "𝐊𝐓𝟒𝐁")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐒𝟓» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟓 1024 (Lean.ParserDescr.symbol "𝐒𝟓")
Instances For
Equations
- LO.Modal.instS5HilbertFormulaS5 = LO.System.S5.mk
Equations
- LO.Modal.«term𝐒𝟓𝐆𝐫𝐳» = Lean.ParserDescr.node `LO.Modal.term𝐒𝟓𝐆𝐫𝐳 1024 (Lean.ParserDescr.symbol "𝐒𝟓𝐆𝐫𝐳")
Instances For
Equations
- LO.Modal.instS5HilbertFormulaS5Grz = LO.System.S5.mk
Equations
- LO.Modal.instGrzHilbertFormulaS5Grz = LO.System.Grz.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐓𝐫𝐢𝐯» = Lean.ParserDescr.node `LO.Modal.term𝐓𝐫𝐢𝐯 1024 (Lean.ParserDescr.symbol "𝐓𝐫𝐢𝐯")
Instances For
Equations
- LO.Modal.instTrivHilbertFormulaTriv = LO.System.Triv.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐕𝐞𝐫» = Lean.ParserDescr.node `LO.Modal.term𝐕𝐞𝐫 1024 (Lean.ParserDescr.symbol "𝐕𝐞𝐫")
Instances For
Equations
- LO.Modal.instVerHilbertFormulaVer = LO.System.Ver.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐆𝐋» = Lean.ParserDescr.node `LO.Modal.term𝐆𝐋 1024 (Lean.ParserDescr.symbol "𝐆𝐋")
Instances For
Equations
- LO.Modal.instGLHilbertFormulaGL = LO.System.GL.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐆𝐫𝐳» = Lean.ParserDescr.node `LO.Modal.term𝐆𝐫𝐳 1024 (Lean.ParserDescr.symbol "𝐆𝐫𝐳")
Instances For
Equations
- LO.Modal.instGrzHilbertFormulaGrz = LO.System.Grz.mk
@[reducible, inline]
Instances For
Equations
- LO.Modal.«term𝐊𝟒𝐇» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟒𝐇 1024 (Lean.ParserDescr.symbol "𝐊𝟒𝐇")
Instances For
Equations
- LO.Modal.instK4HHilbertFormulaK4H = LO.System.K4H.mk
Equations
- LO.Modal.«term𝐊𝟒(𝐋)» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟒(𝐋) 1024 (Lean.ParserDescr.symbol "𝐊𝟒(𝐋)")
Instances For
Equations
- LO.Modal.instHasAxiomKK4Loeb = { has_axiomK := ⋯ }
Equations
- LO.Modal.instHasNecessitationK4Loeb = { has_necessitation := ⋯ }
Equations
- LO.Modal.instHasLoebRuleK4Loeb = { has_loeb := ⋯ }
Equations
- LO.Modal.instK4LoebHilbertFormulaK4Loeb = LO.System.K4Loeb.mk
Equations
- LO.Modal.«term𝐊𝟒(𝐇)» = Lean.ParserDescr.node `LO.Modal.term𝐊𝟒(𝐇) 1024 (Lean.ParserDescr.symbol "𝐊𝟒(𝐇)")
Instances For
Equations
- LO.Modal.instHasAxiomKK4Henkin = { has_axiomK := ⋯ }
Equations
- LO.Modal.instHasNecessitationK4Henkin = { has_necessitation := ⋯ }
Equations
- LO.Modal.instHasHenkinRuleK4Henkin = { has_henkin := ⋯ }
Equations
- LO.Modal.instK4HenkinHilbertFormulaK4Henkin = LO.System.K4Henkin.mk
@[reducible, inline]
Solovey's Provability Logic of True Arithmetic. Remark necessitation is not permitted.
Instances For
Equations
- LO.Modal.«term𝐆𝐋𝐒» = Lean.ParserDescr.node `LO.Modal.term𝐆𝐋𝐒 1024 (Lean.ParserDescr.symbol "𝐆𝐋𝐒")
Instances For
Equations
- LO.Modal.instHasAxiomKHilbertFormulaGLS = { K := fun (x x_1 : LO.Modal.Formula α) => LO.Modal.Deduction.maxm ⋯ }
Equations
- LO.Modal.instHasAxiomLHilbertFormulaGLS = { L := fun (x : LO.Modal.Formula α) => LO.Modal.Deduction.maxm ⋯ }
Equations
- LO.Modal.instHasAxiomTHilbertFormulaGLS = { T := fun (x : LO.Modal.Formula α) => LO.Modal.Deduction.maxm ⋯ }
@[reducible, inline]
Logic of Pure Necessitation
Instances For
Equations
- LO.Modal.«term𝐍» = Lean.ParserDescr.node `LO.Modal.term𝐍 1024 (Lean.ParserDescr.symbol "𝐍")
Instances For
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✝)
:
Λ₁ ≤ₛ Λ₂