Basic

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

Imported declaration from the Incompleteness formalization.

• axioms : Set (Formula α)

  Imported declaration from the Incompleteness formalization.

@[reducible, inline]

abbrev LO.Modal.Hilbert.axiomInstances {α : Type u_1} (H : Hilbert α) : Set (Formula α)

Imported declaration from the Incompleteness formalization.

Equations

• H.axiomInstances = {x : LO.Modal.Formula α | ∃ φ ∈ H.axioms, ∃ (s : LO.Modal.Substitution α), φ⟦s⟧ = x}

theorem LO.Modal.Hilbert.mem_axiomInstances_of_mem_axioms {α : Type u_1} {H : Hilbert α} {φ : Formula α} (h : φ ∈ H.axioms) : φ ∈ H.axiomInstances

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

Imported declaration from the Incompleteness formalization.

• axioms_fin : H.axioms.Finite

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

Imported declaration from the Incompleteness formalization.

• maxm {α : Type u_1} {H : Hilbert α} {φ : Formula α} : φ ∈ H.axiomInstances → H.Deduction φ
• mdp {α : Type u_1} {H : Hilbert α} {φ ψ : Formula α} : H.Deduction (φ ==> ψ) → H.Deduction φ → H.Deduction ψ
• nec {α : Type u_1} {H : Hilbert α} {φ : Formula α} : H.Deduction φ → H.Deduction (□φ)
• imply₁ {α : Type u_1} {H : Hilbert α} (φ ψ : Formula α) : H.Deduction (Axioms.Imply₁ φ ψ)
• imply₂ {α : Type u_1} {H : Hilbert α} (φ ψ χ : Formula α) : H.Deduction (Axioms.Imply₂ φ ψ χ)
• ec {α : Type u_1} {H : Hilbert α} (φ ψ : Formula α) : H.Deduction (Axioms.ElimContra φ ψ)

@[implicit_reducible]

instance LO.Modal.Hilbert.Deduction.instEntailmentFormula {α : Type u_1} : Entailment (Formula α) (Hilbert α)

Equations

• LO.Modal.Hilbert.Deduction.instEntailmentFormula = { Prf := LO.Modal.Hilbert.Deduction }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• LO.Modal.Hilbert.Deduction.instClassicalFormula = { toMinimal := LO.Entailment.Lukasiewicz.instClassical.toMinimal, toHasAxiomDNE := LO.Entailment.Lukasiewicz.instHasAxiomDNE }

@[implicit_reducible]

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

Equations

• LO.Modal.Hilbert.Deduction.instHasDiaDualityFormula = inferInstance

@[implicit_reducible]

instance LO.Modal.Hilbert.Deduction.instNecessitationFormula {α : Type u_1} {H : Hilbert α} : Entailment.Necessitation H

Equations

• LO.Modal.Hilbert.Deduction.instNecessitationFormula = { nec := fun {φ : LO.Modal.Formula α} => LO.Modal.Hilbert.Deduction.nec }

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

noncomputable def LO.Modal.Hilbert.Deduction.rec! {α : Type u_1} {H : Hilbert α} {motive : (φ : Formula α) → H ⊢! φ → Sort u_2} (maxm : {φ : Formula α} → (h : φ ∈ H.axiomInstances) → motive φ ⋯) (mdp : {φ ψ : Formula α} → {hpq : H ⊢! φ ==> ψ} → {hp : H ⊢! φ} → motive (φ ==> ψ) hpq → motive φ hp → motive ψ ⋯) (nec : {φ : Formula α} → {hp : H ⊢! φ} → motive φ hp → motive (□φ) ⋯) (imply₁ : {φ ψ : Formula α} → motive (Axioms.Imply₁ φ ψ) ⋯) (imply₂ : {φ ψ χ : Formula α} → motive (Axioms.Imply₂ φ ψ χ) ⋯) (ec : {φ ψ : Formula α} → motive (Axioms.ElimContra φ ψ) ⋯) {φ : Formula α} (d : H ⊢! φ) : motive φ d

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Modal.Hilbert.Deduction.subst! {α : Type u_1} {H : Hilbert α} {φ : Formula α} (s : Substitution α) (h : H ⊢! φ) : H ⊢! φ⟦s⟧

Imported declaration from the Incompleteness formalization.

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• H.theorems = LO.Entailment.theory H

theorem LO.Modal.Hilbert.of_subset {α : Type u_1} {H₁ H₂ : Hilbert α} {φ : Formula α} (hs : H₁.axioms ⊆ H₂.axioms) : H₁ ⊢! φ → H₂ ⊢! φ

theorem LO.Modal.Hilbert.weakerThan_of_dominate_axiomInstances {α : Type u_1} {H₁ H₂ : Hilbert α} (hMaxm : ∀ {φ : Formula α}, φ ∈ H₁.axiomInstances → H₂ ⊢! φ) : H₁ wkn H₂

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