Results on propositional theories

In this file we prove the expected results that IPL Atom is an intuitionistic theory, and CPL Atom is a classical theory. We provide derived rules for common intuitionistic and classical proof patterns.

@[instance_reducible]

instance Cslib.Logic.PL.Theory.instIsIntuitionisticIPL {Atom : Type u} [DecidableEq Atom] [Bot Atom] : IsIntuitionistic Atom ↑(IPL Atom)

Equations

• Cslib.Logic.PL.Theory.instIsIntuitionisticIPL = { efq := fun (A : Cslib.Logic.PL.Proposition Atom) => Cslib.Logic.PL.Theory.Derivation.ax ⋯ }

def Cslib.Logic.PL.Theory.IsIntuitionistic.efqCtx {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom} [IsIntuitionistic Atom ↑T] (Γ : Ctx Atom) (A : Proposition Atom) : InferenceSystem.derivation ↑T (Γ, HasImp.imp ⊥ A)

Derivation of efq in an arbitrary context.

Equations

• Cslib.Logic.PL.Theory.IsIntuitionistic.efqCtx Γ A = Cslib.Logic.PL.Theory.Derivation.weakCtx ⋯ (Cslib.Logic.PL.Theory.IsIntuitionistic.efq A)

def Cslib.Logic.PL.Theory.IsIntuitionistic.efqRule {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom} [IsIntuitionistic Atom ↑T] (Γ : Ctx Atom) (A : Proposition Atom) (D : InferenceSystem.derivation ↑T (Γ, ⊥)) : InferenceSystem.derivation ↑T (Γ, A)

Efq as a derived rule.

Equations

• Cslib.Logic.PL.Theory.IsIntuitionistic.efqRule Γ A D = Cslib.Logic.PL.Theory.Derivation.implE (Cslib.Logic.PL.Theory.IsIntuitionistic.efqCtx Γ A) D

def Cslib.Logic.PL.Theory.IsIntuitionistic.contra {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom} [IsIntuitionistic Atom ↑T] {Γ : Ctx Atom} (A B : Proposition Atom) (hΓ : A ∈ Γ) (hΓ' : HasNot.not A ∈ Γ) : InferenceSystem.derivation ↑T (Γ, B)

Prove any proposition from contradictory hypotheses.

Equations

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

@[instance_reducible]

instance Cslib.Logic.PL.Theory.instIsClassicalCPL {Atom : Type u} [DecidableEq Atom] [Bot Atom] : IsClassical Atom ↑(CPL Atom)

Equations

• Cslib.Logic.PL.Theory.instIsClassicalCPL = { dne := fun (A : Cslib.Logic.PL.Proposition Atom) => Cslib.Logic.PL.Theory.Derivation.ax ⋯ }

def Cslib.Logic.PL.Theory.IsClassical.byContra {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom} [IsClassical Atom ↑T] {Γ : Ctx Atom} {A : Proposition Atom} (D : InferenceSystem.derivation ↑T (insert (HasNot.not A) Γ, ⊥)) : InferenceSystem.derivation ↑T (Γ, A)

Proof by contradiction as a derived rule.

Equations

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

@[instance_reducible]

instance Cslib.Logic.PL.Theory.instIsIntuitionisticOfIsClassical {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom} [IsClassical Atom ↑T] : IsIntuitionistic Atom ↑T

Equations

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

def Cslib.Logic.PL.Theory.IsClassical.lem {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom} [IsClassical Atom ↑T] (A : Proposition Atom) : InferenceSystem.derivation (↑T) (HasOr.or A (HasNot.not A))

Law of excluded middle in a classical theory.

Equations

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

def Cslib.Logic.PL.Theory.IsClassical.pierce {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom} [IsClassical Atom ↑T] (A B : Proposition Atom) : InferenceSystem.derivation (↑T) (HasImp.imp (HasImp.imp (HasImp.imp A B) A) A)

Pierce's law in a classical theory.

Equations

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

def Cslib.Logic.PL.Theory.LEM (Atom : Type u) [Bot Atom] : Theory Atom

The axiom system consisting of instances of LEM.

Equations

• Cslib.Logic.PL.Theory.LEM Atom = {x : Cslib.Logic.PL.Proposition Atom | ∃ (A : Cslib.Logic.PL.Proposition Atom), Cslib.Logic.HasOr.or A (Cslib.Logic.HasNot.not A) = x}

theorem Cslib.Logic.PL.Theory.lem_mem_lem {Atom : Type u} [Bot Atom] (A : Proposition Atom) : HasOr.or A (HasNot.not A) ∈ LEM Atom

def Cslib.Logic.PL.Theory.Pierce (Atom : Type u) : Theory Atom

The axiom system consisting of instances of Pierce's law.

Equations

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

theorem Cslib.Logic.PL.Theory.pierce_mem_pierce {Atom : Type u} (A B : Proposition Atom) : HasImp.imp (HasImp.imp (HasImp.imp A B) A) A ∈ Pierce Atom

@[instance_reducible]

instance Cslib.Logic.PL.Theory.instIsClassicalLEM {Atom : Type u} [DecidableEq Atom] [Bot Atom] : IsClassical Atom ↑(LEM Atom ∪ IPL Atom)

Equations

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

@[instance_reducible]

instance Cslib.Logic.PL.Theory.instIsClassicalPierce {Atom : Type u} [DecidableEq Atom] [Bot Atom] : IsClassical Atom ↑(Pierce Atom ∪ IPL Atom)

Equations

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