Foundation.Modal.Hilbert.Basic

source

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

Type u_2

instance of inference rule

antecedents : List (LO.Modal.Formula α)
consequence : 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.

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.InferenceRule.Necessitation {α : Type u_1} (φ : LO.Modal.Formula α) :

LO.Modal.Hilbert.InferenceRule α

Equations

LO.Modal.Hilbert.InferenceRule.Necessitation φ = { antecedents := [φ], consequence := □φ, antecedents_nonempty := ⋯ }

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.InferenceRule.Necessitation.set {α : Type u_1} :

Set (LO.Modal.Hilbert.InferenceRule α)

Equations

⟮Nec⟯ = {x : LO.Modal.Hilbert.InferenceRule α | ∃ (φ : LO.Modal.Formula α), LO.Modal.Hilbert.InferenceRule.Necessitation φ = x}

Instances For

source

def LO.Modal.Hilbert.InferenceRule.«term⟮Nec⟯» :

Lean.ParserDescr

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.InferenceRule.LoebRule {α : Type u_1} (φ : LO.Modal.Formula α) :

LO.Modal.Hilbert.InferenceRule α

Equations

LO.Modal.Hilbert.InferenceRule.LoebRule φ = { antecedents := [□φ ➝ φ], consequence := φ, antecedents_nonempty := ⋯ }

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.InferenceRule.LoebRule.set {α : Type u_1} :

Set (LO.Modal.Hilbert.InferenceRule α)

Equations

⟮Loeb⟯ = {x : LO.Modal.Hilbert.InferenceRule α | ∃ (φ : LO.Modal.Formula α), LO.Modal.Hilbert.InferenceRule.LoebRule φ = x}

Instances For

source

def LO.Modal.Hilbert.InferenceRule.«term⟮Loeb⟯» :

Lean.ParserDescr

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.InferenceRule.HenkinRule {α : Type u_1} (φ : LO.Modal.Formula α) :

LO.Modal.Hilbert.InferenceRule α

Equations

LO.Modal.Hilbert.InferenceRule.HenkinRule φ = { antecedents := [□φ ⭤ φ], consequence := φ, antecedents_nonempty := ⋯ }

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.InferenceRule.HenkinRule.set {α : Type u_1} :

Set (LO.Modal.Hilbert.InferenceRule α)

Equations

⟮Henkin⟯ = {x : LO.Modal.Hilbert.InferenceRule α | ∃ (φ : LO.Modal.Formula α), LO.Modal.Hilbert.InferenceRule.HenkinRule φ = x}

Instances For

source

def LO.Modal.Hilbert.InferenceRule.«term⟮Henkin⟯» :

Lean.ParserDescr

Equations

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

Instances For

source

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

Type u_2

axioms : LO.Modal.Theory α
rules : Set (LO.Modal.Hilbert.InferenceRule α)

Instances For

source

inductive LO.Modal.Hilbert.Deduction {α : Type u_1} (H : LO.Modal.Hilbert α) :

LO.Modal.Formula α → Type u_1

maxm: {α : Type u_1} → {H : LO.Modal.Hilbert α} → {φ : LO.Modal.Formula α} → φ ∈ H.axioms → H.Deduction φ
rule: {α : Type u_1} → {H : LO.Modal.Hilbert α} → {rl : LO.Modal.Hilbert.InferenceRule α} → rl ∈ H.rules → ({φ : LO.Modal.Formula α} → φ ∈ rl.antecedents → H.Deduction φ) → H.Deduction rl.consequence
mdp: {α : Type u_1} → {H : LO.Modal.Hilbert α} → {φ ψ : LO.Modal.Formula α} → H.Deduction (φ ➝ ψ) → H.Deduction φ → H.Deduction ψ
imply₁: {α : Type u_1} → {H : LO.Modal.Hilbert α} → (φ ψ : LO.Modal.Formula α) → H.Deduction (LO.Axioms.Imply₁ φ ψ)
imply₂: {α : Type u_1} → {H : LO.Modal.Hilbert α} → (φ ψ χ : LO.Modal.Formula α) → H.Deduction (LO.Axioms.Imply₂ φ ψ χ)
ec: {α : Type u_1} → {H : LO.Modal.Hilbert α} → (φ ψ : LO.Modal.Formula α) → H.Deduction (LO.Axioms.ElimContra φ ψ)

Instances For

source

instance LO.Modal.Hilbert.Deduction.instSystemFormula {α : Type u_1} :

LO.System (LO.Modal.Formula α) (LO.Modal.Hilbert α)

Equations

LO.Modal.Hilbert.Deduction.instSystemFormula = { Prf := LO.Modal.Hilbert.Deduction }

source

instance LO.Modal.Hilbert.Deduction.instLukasiewiczFormula {α : Type u_1} {H : LO.Modal.Hilbert α} :

LO.System.Lukasiewicz H

Equations

LO.Modal.Hilbert.Deduction.instLukasiewiczFormula = LO.System.Lukasiewicz.mk

source

instance LO.Modal.Hilbert.Deduction.instClassicalFormula {α : Type u_1} {H : LO.Modal.Hilbert α} :

LO.System.Classical H

Equations

LO.Modal.Hilbert.Deduction.instClassicalFormula = LO.System.Classical.mk

source

instance LO.Modal.Hilbert.Deduction.instHasDiaDualityFormula {α : Type u_1} {H : LO.Modal.Hilbert α} :

LO.System.HasDiaDuality H

Equations

LO.Modal.Hilbert.Deduction.instHasDiaDualityFormula = inferInstance

source

theorem LO.Modal.Hilbert.Deduction.maxm! {α : Type u_1} {H : LO.Modal.Hilbert α} {φ : LO.Modal.Formula α} (h : φ ∈ H.axioms) :

H ⊢! φ

source

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

Prop

has_necessitation : ⟮Nec⟯ ⊆ H.rules

Instances

source

instance LO.Modal.Hilbert.instNecessitationFormulaOfHasNecessitation {α : Type u_1} {H : LO.Modal.Hilbert α} [H.HasNecessitation] :

LO.System.Necessitation H

Equations

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

source

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

Prop

has_loeb : ⟮Loeb⟯ ⊆ H.rules

Instances

source

instance LO.Modal.Hilbert.instLoebRuleFormulaOfHasLoebRule {α : Type u_1} {H : LO.Modal.Hilbert α} [H.HasLoebRule] :

LO.System.LoebRule H

Equations

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

source

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

Prop

has_henkin : ⟮Henkin⟯ ⊆ H.rules

Instances

source

instance LO.Modal.Hilbert.instHenkinRuleFormulaOfHasHenkinRule {α : Type u_1} {H : LO.Modal.Hilbert α} [H.HasHenkinRule] :

LO.System.HenkinRule H

Equations

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

source

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

Prop

has_necessitation_only : H.rules = ⟮Nec⟯

Instances

source

instance LO.Modal.Hilbert.instHasNecessitationOfHasNecOnly {α : Type u_1} {H : LO.Modal.Hilbert α} [h : H.HasNecOnly] :

H.HasNecessitation

Equations

⋯ = ⋯

source

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

Prop

has_axiomK : 𝗞 ⊆ H.axioms

Instances

source

instance LO.Modal.Hilbert.instHasAxiomKFormulaOfHasAxiomK {α : Type u_1} {H : LO.Modal.Hilbert α} [H.HasAxiomK] :

LO.System.HasAxiomK H

Equations

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

source

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

Prop

has_necessitation_only : H.rules = ⟮Nec⟯
has_axiomK : 𝗞 ⊆ H.axioms

Instances

source

instance LO.Modal.Hilbert.instKFormulaOfIsNormal {α : Type u_1} {H : LO.Modal.Hilbert α} [H.IsNormal] :

LO.System.K H

Equations

LO.Modal.Hilbert.instKFormulaOfIsNormal = LO.System.K.mk

source

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

motive φ d

Equations

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

Instances For

source

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

motive φ d

Useful induction for normal modal logic.

Equations

⋯ = ⋯

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.theorems {α : Type u_1} (H : LO.Modal.Hilbert α) :

Set (LO.Modal.Formula α)

Equations

H.theorems = LO.System.theory H

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.Consistent {α : Type u_1} (H : LO.Modal.Hilbert α) :

Prop

Equations

H.Consistent = LO.System.Consistent H

Instances For

source

theorem LO.Modal.Hilbert.normal_weakerThan_of_maxm {α : Type u_1} {H₁ H₂ : LO.Modal.Hilbert α} [H₁.IsNormal] [H₂.IsNormal] (hMaxm : ∀ {φ : LO.Modal.Formula α}, φ ∈ H₁.axioms → H₂ ⊢! φ) :

H₁ ≤ₛ H₂

source

theorem LO.Modal.Hilbert.normal_weakerThan_of_subset {α : Type u_1} {H₁ H₂ : LO.Modal.Hilbert α} [H₁.IsNormal] [H₂.IsNormal] (hSubset : H₁.axioms ⊆ H₂.axioms) :

H₁ ≤ₛ H₂