Documentation

Foundation.Modal.Hilbert.Basic

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

instance of inference rule

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

@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
structure LO.Modal.Hilbert (α : Type u_2) :
Type u_2
Instances For
inductive LO.Modal.Hilbert.Deduction {α : Type u_1} (H : Hilbert α) :
Formula αType u_1
theorem LO.Modal.Hilbert.Deduction.maxm! {α : Type u_1} {H : Hilbert α} {φ : Formula α} (h : φ H.axioms) :
H ⊢! φ
Equations
  • One or more equations did not get rendered due to their size.
instance LO.Modal.Hilbert.instLoebRuleFormulaOfHasLoebRule {α : Type u_1} {H : Hilbert α} [H.HasLoebRule] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
class LO.Modal.Hilbert.HasNecOnly {α : Type u_1} (H : Hilbert α) :
Instances
instance LO.Modal.Hilbert.instHasNecessitationOfHasNecOnly {α : Type u_1} {H : Hilbert α} [h : H.HasNecOnly] :
H.HasNecessitation
noncomputable def LO.Modal.Hilbert.Deduction.inducition! {α : Type u_1} {H : Hilbert α} {motive : (φ : Formula α) → H ⊢! φSort u_2} (hRules : (r : InferenceRule α) → (hr : r H.rules) → (hant : ∀ {φ : Formula α}, φ r.antecedentsH ⊢! φ) → ({φ : Formula α} → (hp : φ r.antecedents) → motive φ )motive r.consequence ) (hMaxm : {φ : Formula α} → (h : φ H.axioms) → motive φ ) (hMdp : {φ ψ : Formula α} → {hpq : H ⊢! φ ψ} → {hp : H ⊢! φ} → motive (φ ψ) hpqmotive φ hpmotive ψ ) (hImply₁ : {φ ψ : Formula α} → motive (φ ψ φ) ) (hImply₂ : {φ ψ χ : Formula α} → motive ((φ ψ χ) (φ ψ) φ χ) ) (hElimContra : {φ ψ : Formula α} → motive (Axioms.ElimContra φ ψ) ) {φ : Formula α} (d : H ⊢! φ) :
motive φ d
Equations
  • One or more equations did not get rendered due to their size.
noncomputable def LO.Modal.Hilbert.Deduction.inducition_with_necOnly! {α : Type u_1} {H : Hilbert α} [H.HasNecOnly] {motive : (φ : Formula α) → H ⊢! φProp} (hMaxm : ∀ {φ : Formula α} (h : φ H.axioms), motive φ ) (hMdp : ∀ {φ ψ : Formula α} {hpq : H ⊢! φ ψ} {hp : H ⊢! φ}, motive (φ ψ) hpqmotive φ hpmotive ψ ) (hNec : ∀ {φ : Formula α} {hp : H ⊢! φ}, motive φ hpmotive (φ) ) (hImply₁ : ∀ {φ ψ : Formula α}, motive (φ ψ φ) ) (hImply₂ : ∀ {φ ψ χ : Formula α}, motive ((φ ψ χ) (φ ψ) φ χ) ) (hElimContra : ∀ {φ ψ : Formula α}, motive (Axioms.ElimContra φ ψ) ) {φ : Formula α} (d : H ⊢! φ) :
motive φ d

Useful induction for normal modal logic.

Equations
  • =
@[reducible, inline]
abbrev LO.Modal.Hilbert.theorems {α : Type u_1} (H : Hilbert α) :
Equations
@[reducible, inline]
abbrev LO.Modal.Hilbert.Consistent {α : Type u_1} (H : Hilbert α) :
Equations
theorem LO.Modal.Hilbert.normal_weakerThan_of_maxm {α : Type u_1} {H₁ H₂ : Hilbert α} [H₁.IsNormal] [H₂.IsNormal] (hMaxm : ∀ {φ : Formula α}, φ H₁.axiomsH₂ ⊢! φ) :
H₁ ≤ₛ H₂
theorem LO.Modal.Hilbert.normal_weakerThan_of_subset {α : Type u_1} {H₁ H₂ : Hilbert α} [H₁.IsNormal] [H₂.IsNormal] (hSubset : H₁.axioms H₂.axioms) :
H₁ ≤ₛ H₂