Basic

structure LO.IntProp.Hilbert (α : Type u_1) : Type u_1

Imported declaration from the Incompleteness formalization.

• axioms : Set (Formula α)

  Imported declaration from the Incompleteness formalization.

@[reducible, inline]

abbrev LO.IntProp.Hilbert.axiomInstances {α : Type u} (H : Hilbert α) : Set (Formula α)

Imported declaration from the Incompleteness formalization.

Equations

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

class LO.IntProp.Hilbert.FiniteAxiomatizable {α : Type u} (H : Hilbert α) : Prop

Imported declaration from the Incompleteness formalization.

• axioms_fin : H.axioms.Finite

inductive LO.IntProp.Hilbert.Deduction {α : Type u} (H : Hilbert α) : Formula α → Type u

Imported declaration from the Incompleteness formalization.

• maxm {α : Type u} {H : Hilbert α} {φ : Formula α} : φ ∈ H.axiomInstances → H.Deduction φ
• mdp {α : Type u} {H : Hilbert α} {φ ψ : Formula α} : H.Deduction (φ ==> ψ) → H.Deduction φ → H.Deduction ψ
• verum {α : Type u} {H : Hilbert α} : H.Deduction ⊤
• implyS {α : Type u} {H : Hilbert α} (φ ψ : Formula α) : H.Deduction (φ ==> ψ ==> φ)
• implyK {α : Type u} {H : Hilbert α} (φ ψ χ : Formula α) : H.Deduction ((φ ==> ψ ==> χ) ==> (φ ==> ψ) ==> φ ==> χ)
• andElimL {α : Type u} {H : Hilbert α} (φ ψ : Formula α) : H.Deduction (φ ⋏ ψ ==> φ)
• andElimR {α : Type u} {H : Hilbert α} (φ ψ : Formula α) : H.Deduction (φ ⋏ ψ ==> ψ)
• andIntro {α : Type u} {H : Hilbert α} (φ ψ : Formula α) : H.Deduction (φ ==> ψ ==> φ ⋏ ψ)
• orIntroL {α : Type u} {H : Hilbert α} (φ ψ : Formula α) : H.Deduction (φ ==> φ ⋎ ψ)
• orIntroR {α : Type u} {H : Hilbert α} (φ ψ : Formula α) : H.Deduction (ψ ==> φ ⋎ ψ)
• orElim {α : Type u} {H : Hilbert α} (φ ψ χ : Formula α) : H.Deduction ((φ ==> χ) ==> (ψ ==> χ) ==> φ ⋎ ψ ==> χ)

@[implicit_reducible]

instance LO.IntProp.Hilbert.instEntailmentFormula {α : Type u} : Entailment (Formula α) (Hilbert α)

Equations

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

@[implicit_reducible]

instance LO.IntProp.Hilbert.instModusPonensFormula {α : Type u} {H : Hilbert α} : Entailment.ModusPonens H

Equations

• LO.IntProp.Hilbert.instModusPonensFormula = { mdp := fun {φ ψ : LO.IntProp.Formula α} => LO.IntProp.Hilbert.Deduction.mdp }

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasAxiomImply₁Formula {α : Type u} {H : Hilbert α} : Entailment.HasAxiomImply₁ H

Equations

• LO.IntProp.Hilbert.instHasAxiomImply₁Formula = { imply₁ := LO.IntProp.Hilbert.Deduction.implyS }

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasAxiomImply₂Formula {α : Type u} {H : Hilbert α} : Entailment.HasAxiomImply₂ H

Equations

• LO.IntProp.Hilbert.instHasAxiomImply₂Formula = { imply₂ := LO.IntProp.Hilbert.Deduction.implyK }

@[implicit_reducible]

instance LO.IntProp.Hilbert.instHasAxiomAndInstFormula {α : Type u} {H : Hilbert α} : Entailment.HasAxiomAndInst H

Equations

• LO.IntProp.Hilbert.instHasAxiomAndInstFormula = { and₃ := LO.IntProp.Hilbert.Deduction.andIntro }

@[implicit_reducible]

instance LO.IntProp.Hilbert.instMinimalFormula {α : Type u} {H : Hilbert α} : Entailment.Minimal H

Equations

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

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

noncomputable def LO.IntProp.Hilbert.Deduction.rec! {α : Type u} {H : Hilbert α} {motive : (φ : Formula α) → H ⊢! φ → Sort u_1} (maxm : {φ : Formula α} → (h : φ ∈ H.axiomInstances) → motive φ ⋯) (mdp : {φ ψ : Formula α} → {hpq : H ⊢! φ ==> ψ} → {hp : H ⊢! φ} → motive (φ ==> ψ) hpq → motive φ hp → motive ψ ⋯) (verum : motive ⊤ ⋯) (implyS : {φ ψ : Formula α} → motive (Axioms.Imply₁ φ ψ) ⋯) (implyK : {φ ψ χ : Formula α} → motive (Axioms.Imply₂ φ ψ χ) ⋯) (andElimL : {φ ψ : Formula α} → motive (φ ⋏ ψ ==> φ) ⋯) (andElimR : {φ ψ : Formula α} → motive (φ ⋏ ψ ==> ψ) ⋯) (andIntro : {φ ψ : Formula α} → motive (φ ==> ψ ==> φ ⋏ ψ) ⋯) (orIntroL : {φ ψ : Formula α} → motive (φ ==> φ ⋎ ψ) ⋯) (orIntroR : {φ ψ : Formula α} → motive (ψ ==> φ ⋎ ψ) ⋯) (orElim : {φ ψ χ : Formula α} → motive ((φ ==> χ) ==> (ψ ==> χ) ==> φ ⋎ ψ ==> χ) ⋯) {φ : 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.IntProp.Hilbert.Deduction.subst! {α : Type u} {H : Hilbert α} {φ : Formula α} (s : Substitution α) (h : H ⊢! φ) : H ⊢! φ⟦s⟧

Imported declaration from the Incompleteness formalization.

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

theorem LO.IntProp.Hilbert.weakerThan_of_subset_axioms {α : Type u} {H₁ H₂ : Hilbert α} (hSubset : H₁.axioms ⊆ H₂.axioms) : H₁ wkn H₂