Propositions and theories

Main definitions

• Proposition : the type of propositions over a given type of atom. This type has a Bot instance whenever Atom does, and a Top whenever Atom is inhabited.
• Theory : set of Proposition.
• IsIntuitionistic : a theory is intuitionistic if it contains the principle of explosion.
• IsClassical : an intuitionistic theory is classical if it further contains double negation elimination.
• Proposition.subst : replace atom x in a A : Proposition Atom with f x, for a function f : Atom → Proposition Atom'. This induces a monad structure on Proposition, with pure := Proposition.atom. Theory is a functor, by mapping each proposition A ∈ T to f <$> A.
• Theory.intuitionisticCompletion : the freely generated intuitionistic theory extending a given theory.

Notation

We instantiate the notation classes HasAnd, HasOr, HasImpl and HasNot for Proposition Atom to give access to, respectively, the notations ∧, ∨, → and ¬ for propositional connectives. In the case that Atom has a bottom element (respectively, is inhabited) we give instances HasBot (Proposition Atom) and (respectively, HasTop (Proposition Atom)).

inductive Cslib.Logic.PL.Proposition (Atom : Type u) : Type u

Propositions.

• atom {Atom : Type u} (x : Atom) : Proposition Atom

  Propositional atoms

• and {Atom : Type u} (a b : Proposition Atom) : Proposition Atom

  Conjunction

• or {Atom : Type u} (a b : Proposition Atom) : Proposition Atom

  Disjunction

• imp {Atom : Type u} (a b : Proposition Atom) : Proposition Atom

  Implication

def Cslib.Logic.PL.instDecidableEqProposition.decEq {Atom✝ : Type u_1} [DecidableEq Atom✝] (x✝ x✝¹ : Proposition Atom✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Logic.PL.instDecidableEqProposition {Atom✝ : Type u_1} [DecidableEq Atom✝] : DecidableEq (Proposition Atom✝)

@[instance_reducible]

instance Cslib.Logic.PL.instBEqProposition {Atom✝ : Type u_1} [BEq Atom✝] : BEq (Proposition Atom✝)

def Cslib.Logic.PL.instBEqProposition.beq {Atom✝ : Type u_1} [BEq Atom✝] : Proposition Atom✝ → Proposition Atom✝ → Bool

@[instance_reducible]

instance Cslib.Logic.PL.instBotProposition {Atom : Type u} [Bot Atom] : Bot (Proposition Atom)

@[instance_reducible]

instance Cslib.Logic.PL.instInhabitedOfBot {Atom : Type u} [Bot Atom] : Inhabited Atom

@[reducible, inline]

abbrev Cslib.Logic.PL.Proposition.neg {Atom : Type u} [Bot Atom] : Proposition Atom → Proposition Atom

We view negation as a defined connective ~A := A → ⊥

@[reducible, inline]

abbrev Cslib.Logic.PL.Proposition.top {Atom : Type u} [Inhabited Atom] : Proposition Atom

A fixed choice of a derivable proposition (of course any two are equivalent).

@[instance_reducible]

instance Cslib.Logic.PL.instTopProposition {Atom : Type u} [Inhabited Atom] : Top (Proposition Atom)

@[instance_reducible]

instance Cslib.Logic.PL.instHasAndProposition {Atom : Type u} : HasAnd (Proposition Atom)

@[instance_reducible]

instance Cslib.Logic.PL.instHasOrProposition {Atom : Type u} : HasOr (Proposition Atom)

@[instance_reducible]

instance Cslib.Logic.PL.instHasImpProposition {Atom : Type u} : HasImp (Proposition Atom)

@[instance_reducible]

instance Cslib.Logic.PL.instHasNotPropositionOfBot {Atom : Type u} [Bot Atom] : HasNot (Proposition Atom)

theorem Cslib.Logic.PL.not_eq {Atom : Type u} [Bot Atom] (A : Proposition Atom) : HasImp.imp A ⊥ = HasNot.not A

def Cslib.Logic.PL.Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') : Proposition Atom → Proposition Atom'

Substitute each atom in a proposition for a proposition, possibly changing the atomic language.

@[instance_reducible]

instance Cslib.Logic.PL.instMonadProposition : Monad Proposition

@[reducible, inline]

abbrev Cslib.Logic.PL.Theory (Atom : Type u_1) : Type u_1

Theories are arbitrary sets of propositions.

def Cslib.Logic.PL.Theory.subst {Atom Atom' : Type u} (T : Theory Atom) (f : Atom → Proposition Atom') : Theory Atom'

Extend a substitution from Proposition to Theory.

@[instance_reducible]

instance Cslib.Logic.PL.Theory.instFunctor : Functor Theory

@[reducible, inline]

abbrev Cslib.Logic.PL.Theory.MPL (Atom : Type u) : Theory Atom

The empty theory corresponds to minimal propositional logic.

@[reducible, inline]

abbrev Cslib.Logic.PL.Theory.IPL (Atom : Type u) [Bot Atom] : Theory Atom

Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet).

theorem Cslib.Logic.PL.Theory.efq_mem_ipl {Atom : Type u} [Bot Atom] (A : Proposition Atom) : HasImp.imp ⊥ A ∈ IPL Atom

@[reducible]

def Cslib.Logic.PL.Theory.intuitionisticCompletion {Atom : Type u} (T : Theory Atom) : Theory (WithBot Atom)

Attach a bottom element to a theory T, and the principle of explosion for that bottom.

@[reducible, inline]

abbrev Cslib.Logic.PL.Theory.CPL (Atom : Type u) [Bot Atom] : Theory Atom

Classical logic further adds double negation elimination.

theorem Cslib.Logic.PL.Theory.dne_mem_cpl {Atom : Type u} [Bot Atom] (A : Proposition Atom) : HasImp.imp (HasNot.not (HasNot.not A)) A ∈ CPL Atom

class Cslib.Logic.PL.Theory.IsIntuitionistic (Atom : Type u) [Bot Atom] (S : Type u_1) [InferenceSystem S (Proposition Atom)] : Sort (max (u + 1) u_2)

An inference system is intuitionistic if it derives ex falso quodlibet. TODO: this should be generalised outside the PL scope, once we have typeclasses to express that a type possesses an implication connective.

• efq (A : Proposition Atom) : InferenceSystem.derivation S (HasImp.imp ⊥ A)

  The principle of explosion (ex falso quolibet).

class Cslib.Logic.PL.Theory.IsClassical (Atom : Type u) [Bot Atom] (S : Type u_1) [InferenceSystem S (Proposition Atom)] : Sort (max (u + 1) u_2)

An inference system is classical if it validates double-negation elimination. TODO: this should be generalised outside the PL scope, once we have typeclasses to express that a type possesses an implication connective.

• dne (A : Proposition Atom) : InferenceSystem.derivation S (HasImp.imp (HasNot.not (HasNot.not A)) A)

  Double-negation elimination.