Foundation.Propositional.Hilbert.Basic

source

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

Type u_2

schema : Set (Formula α)
schema_closed (φ : Formula α) : φ ∈ self.schema → ∀ (s : Substitution α), φ⟦s⟧ ∈ self.schema

Instances For

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instSetLikeFormula {α : Type u_1} :

SetLike (Hilbert α) (Formula α)

Equations

LO.Propositional.Hilbert.instSetLikeFormula = { coe := LO.Propositional.Hilbert.schema, coe_injective := ⋯ }

source

def LO.Propositional.Hilbert.Min {α : Type u_1} :

Hilbert α

Equations

LO.Propositional.Hilbert.Min = { schema := ∅, schema_closed := ⋯ }

Instances For

source

def LO.Propositional.Hilbert.Int {α : Type u_1} :

Hilbert α

Equations

LO.Propositional.Hilbert.Int = { schema := {x : LO.Propositional.Formula α | ∃ (φ : LO.Propositional.Formula α), LO.Axioms.EFQ φ = x}, schema_closed := ⋯ }

Instances For

source

def LO.Propositional.Hilbert.Cl {α : Type u_1} :

Hilbert α

Equations

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

Instances For

source

@[simp]

theorem LO.Propositional.Hilbert.Int_le_Cl {α : Type u_1} :

Hilbert.Int.schema ⊆ Hilbert.Cl.schema

source

inductive LO.Propositional.HilbertProof {α : Type u_1} (Λ : Hilbert α) :

Formula α → Type u_1

axm {α : Type u_1} {Λ : Hilbert α} {φ : Formula α} : φ ∈ Λ → HilbertProof Λ φ
mdp {α : Type u_1} {Λ : Hilbert α} {φ ψ : Formula α} : HilbertProof Λ (φ 🡒 ψ) → HilbertProof Λ φ → HilbertProof Λ ψ
verum {α : Type u_1} {Λ : Hilbert α} : HilbertProof Λ Axioms.Verum
implyS {α : Type u_1} {Λ : Hilbert α} {φ ψ χ : Formula α} : HilbertProof Λ (Axioms.ImplyS φ ψ χ)
implyK {α : Type u_1} {Λ : Hilbert α} {φ ψ : Formula α} : HilbertProof Λ (Axioms.ImplyK φ ψ)
andElimL {α : Type u_1} {Λ : Hilbert α} {φ ψ : Formula α} : HilbertProof Λ (Axioms.AndElim₁ φ ψ)
andElimR {α : Type u_1} {Λ : Hilbert α} {φ ψ : Formula α} : HilbertProof Λ (Axioms.AndElim₂ φ ψ)
andIntro {α : Type u_1} {Λ : Hilbert α} {φ ψ : Formula α} : HilbertProof Λ (Axioms.AndInst φ ψ)
orIntroL {α : Type u_1} {Λ : Hilbert α} {φ ψ : Formula α} : HilbertProof Λ (Axioms.OrInst₁ φ ψ)
orIntroR {α : Type u_1} {Λ : Hilbert α} {φ ψ : Formula α} : HilbertProof Λ (Axioms.OrInst₂ φ ψ)
orElim {α : Type u_1} {Λ : Hilbert α} {φ ψ χ : Formula α} : HilbertProof Λ (Axioms.OrElim φ ψ χ)

Instances For

source

@[implicit_reducible]

instance LO.Propositional.instEntailmentHilbertFormula {α : Type u_1} :

Entailment (Hilbert α) (Formula α)

Equations

LO.Propositional.instEntailmentHilbertFormula = { Prf := LO.Propositional.HilbertProof }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instModusPonensFormula {α : Type u_1} (H : Hilbert α) :

Entailment.ModusPonens H

Equations

H.instModusPonensFormula = { mdp := fun {φ ψ : LO.Propositional.Formula α} => LO.Propositional.HilbertProof.mdp }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instHasAxiomImplyKFormula {α : Type u_1} (H : Hilbert α) :

Entailment.HasAxiomImplyK H

Equations

H.instHasAxiomImplyKFormula = { implyK := fun {φ ψ : LO.Propositional.Formula α} => LO.Propositional.HilbertProof.implyK }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instHasAxiomImplySFormula {α : Type u_1} (H : Hilbert α) :

Entailment.HasAxiomImplyS H

Equations

H.instHasAxiomImplySFormula = { implyS := fun {φ ψ χ : LO.Propositional.Formula α} => LO.Propositional.HilbertProof.implyS }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instHasAxiomAndInstFormula {α : Type u_1} (H : Hilbert α) :

Entailment.HasAxiomAndInst H

Equations

H.instHasAxiomAndInstFormula = { and₃ := fun {φ ψ : LO.Propositional.Formula α} => LO.Propositional.HilbertProof.andIntro }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instMinimalFormula {α : Type u_1} (H : Hilbert α) :

Entailment.Minimal H

Equations

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

source

def LO.Propositional.Hilbert.ofSchema {α : Type u_1} {Λ : Hilbert α} {φ : Formula α} :

φ ∈ Λ → HilbertProof Λ φ

Alias of LO.Propositional.HilbertProof.axm.

Equations

@LO.Propositional.Hilbert.ofSchema = @LO.Propositional.HilbertProof.axm

Instances For

source

theorem LO.Propositional.Hilbert.of_schema {α : Type u_1} {H : Hilbert α} {φ : Formula α} (h : φ ∈ H) :

H ⊢ φ

source

def LO.Propositional.Hilbert.ofLE {α : Type u_1} {H₁ H₂ : Hilbert α} {φ : Formula α} (h : H₁.schema ⊆ H₂.schema) :

H₁ ⊢! φ → H₂ ⊢! φ

Equations

Instances For

source

theorem LO.Propositional.Hilbert.of_le {α : Type u_1} {H₁ H₂ : Hilbert α} {φ : Formula α} (h : H₁.schema ⊆ H₂.schema) :

H₁ ⊢ φ → H₂ ⊢ φ

source

theorem LO.Propositional.Hilbert.weakerThan_of_le {α : Type u_1} {H₁ H₂ : Hilbert α} (h : H₁.schema ⊆ H₂.schema) :

H₁ ⪯ H₂

source

def LO.Propositional.Hilbert.Subst {α : Type u_1} {φ : Formula α} {H : Hilbert α} (s : Substitution α) :

H ⊢! φ → H ⊢! φ⟦s⟧

Equations

Instances For

source

theorem LO.Propositional.Hilbert.subst {α : Type u_1} {φ : Formula α} {H : Hilbert α} (s : Substitution α) :

H ⊢ φ → H ⊢ φ⟦s⟧

source

def LO.Propositional.Hilbert.ofProofSchema {α : Type u_1} {H₁ H₂ : Hilbert α} {φ : Formula α} (h : H₂ ⊢!* H₁.schema) :

H₁ ⊢! φ → H₂ ⊢! φ

Equations

Instances For

source

theorem LO.Propositional.Hilbert.of_proof_schema {α : Type u_1} {H₁ H₂ : Hilbert α} {φ : Formula α} (h : H₂ ⊢* H₁.schema) :

H₁ ⊢ φ → H₂ ⊢ φ

source

theorem LO.Propositional.Hilbert.weakerThan_of_provable_schema {α : Type u_1} {H₁ H₂ : Hilbert α} (h : H₂ ⊢* H₁.schema) :

H₁ ⪯ H₂

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instIntFormulaInt {α : Type u_1} :

Entailment.Int Hilbert.Int

Equations

LO.Propositional.Hilbert.instIntFormulaInt = { toMinimal := LO.Propositional.Hilbert.Int.instMinimalFormula, efq := fun {φ : LO.Propositional.Formula α} => LO.Propositional.HilbertProof.axm ⋯ }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instHasAxiomEFQFormulaCl {α : Type u_1} :

Entailment.HasAxiomEFQ Hilbert.Cl

Equations

LO.Propositional.Hilbert.instHasAxiomEFQFormulaCl = { efq := fun {φ : LO.Propositional.Formula α} => LO.Propositional.HilbertProof.axm ⋯ }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instHasAxiomLEMFormulaCl {α : Type u_1} :

Entailment.HasAxiomLEM Hilbert.Cl

Equations

LO.Propositional.Hilbert.instHasAxiomLEMFormulaCl = { lem := fun {φ : LO.Propositional.Formula α} => LO.Propositional.HilbertProof.axm ⋯ }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instIntFormulaCl {α : Type u_1} :

Entailment.Int Hilbert.Cl

Equations

LO.Propositional.Hilbert.instIntFormulaCl = { toMinimal := LO.Propositional.Hilbert.Cl.instMinimalFormula, toHasAxiomEFQ := LO.Propositional.Hilbert.instHasAxiomEFQFormulaCl }

source

@[implicit_reducible]

instance LO.Propositional.Hilbert.instClFormulaClOfDecidableEq {α : Type u_1} [DecidableEq α] :

Entailment.Cl Hilbert.Cl

Equations

LO.Propositional.Hilbert.instClFormulaClOfDecidableEq = { toMinimal := LO.Propositional.Hilbert.Cl.instMinimalFormula, toHasAxiomDNE := LO.Entailment.instHasAxiomDNEOfHasAxiomLEM }

source

@[reducible, inline]

abbrev LO.Propositional.Hilbert.logic {α : Type u_1} (H : Hilbert α) :

Logic α

Equations

H.logic = { logic := LO.Entailment.theory H, subst := ⋯, mdp := ⋯ }

Instances For

source

theorem LO.Propositional.Hilbert.mem_logic_of_proof {α : Type u_1} {H : Hilbert α} {φ : Formula α} (h : H ⊢! φ) :

φ ∈ H.logic

source

theorem LO.Propositional.Hilbert.mem_logic_of_provable {α : Type u_1} {H : Hilbert α} {φ : Formula α} (h : H ⊢ φ) :

φ ∈ H.logic

source

theorem LO.Propositional.Hilbert.provable_of_mem_logic {α : Type u_1} {H : Hilbert α} {φ : Formula α} (h : φ ∈ H.logic) :

H ⊢ φ

source

theorem LO.Propositional.Hilbert.iff_mem_logic_provable {α : Type u_1} {H : Hilbert α} {φ : Formula α} :

H ⊢ φ ↔ φ ∈ H.logic

source

@[reducible, inline]

abbrev LO.Propositional.Int {α : Type u_1} :

Logic α

Equations

LO.Propositional.Int = LO.Propositional.Hilbert.Int.logic

Instances For

source

@[reducible, inline]

abbrev LO.Propositional.Cl {α : Type u_1} :

Logic α

Equations

LO.Propositional.Cl = LO.Propositional.Hilbert.Cl.logic

Instances For