Documentation

Foundation.Propositional.Hilbert.Basic

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

Type u_2

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

Instances For

@[instance_reducible]

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

SetLike (Hilbert α) (Formula α)

Equations

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

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

@[simp]

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

Hilbert.Int.schema ⊆ Hilbert.Cl.schema

inductive FFL.Propositional.Hilbert.Proof {α : Type u_1} (Λ : Hilbert α) :

Formula α → Type u_1

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

Instances For

@[instance_reducible]

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

Entailment (Hilbert α) (Formula α)

Equations

FFL.Propositional.instEntailmentHilbertFormula = { Entails := fun (H : FFL.Propositional.Hilbert α) (φ : FFL.Propositional.Formula α) => Nonempty (H.Proof φ) }

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

Entailment.ModusPonens H

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

Entailment.HasAxiomImplyK H

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

Entailment.HasAxiomImplyS H

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

Entailment.HasAxiomAndInst H

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

Entailment.Minimal H

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

φ ∈ Λ → Λ.Proof φ

Alias of FFL.Propositional.Hilbert.Proof.axm.

Equations

@FFL.Propositional.Hilbert.ofSchema = @FFL.Propositional.Hilbert.Proof.axm

Instances For

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

H ⊢ φ

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

H₁.Proof φ → H₂.Proof φ

Equations

Instances For

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

H₁ ⊢ φ → H₂ ⊢ φ

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

H₁ ⪯ H₂

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

H.Proof φ → H.Proof (φ⟦s⟧)

Equations

Instances For

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

H ⊢ φ → H ⊢ φ⟦s⟧

def FFL.Propositional.Hilbert.ofProofSchema {α : Type u_1} {H₁ H₂ : Hilbert α} {φ : Formula α} (h : {φ : Formula α} → φ ∈ H₁.schema → H₂.Proof φ) :

H₁.Proof φ → H₂.Proof φ

Equations

Instances For

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

H₁ ⊢ φ → H₂ ⊢ φ

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

H₁ ⪯ H₂

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

Entailment.Int Hilbert.Int

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

Entailment.HasAxiomEFQ Hilbert.Cl

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

Entailment.HasAxiomLEM Hilbert.Cl

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

Entailment.Int Hilbert.Cl

instance FFL.Propositional.Hilbert.instClFormulaCl {α : Type u_1} :

Entailment.Cl Hilbert.Cl

@[reducible, inline]

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

Equations

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

Instances For

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

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

H ⊢ φ

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

H ⊢ φ ↔ φ ∈ H.logic

@[reducible, inline]

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

Equations

FFL.Propositional.Int = FFL.Propositional.Hilbert.Int.logic

Instances For

@[reducible, inline]

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

Equations

FFL.Propositional.Cl = FFL.Propositional.Hilbert.Cl.logic

Instances For