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✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Logic.PL.instDecidableEqProposition.decEq (Cslib.Logic.PL.Proposition.atom a) (Cslib.Logic.PL.Proposition.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (Cslib.Logic.PL.Proposition.atom x_2) (a.and b) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (Cslib.Logic.PL.Proposition.atom x_2) (a.or b) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (Cslib.Logic.PL.Proposition.atom x_2) (a.imp b) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.and b) (Cslib.Logic.PL.Proposition.atom x_2) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.and b) (a_1.or b_1) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.and b) (a_1.imp b_1) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.or b) (Cslib.Logic.PL.Proposition.atom x_2) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.or b) (a_1.and b_1) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.or b) (a_1.imp b_1) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.imp b) (Cslib.Logic.PL.Proposition.atom x_2) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.imp b) (a_1.and b_1) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.imp b) (a_1.or b_1) = isFalse ⋯

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instDecidableEqProposition = Cslib.Logic.PL.instDecidableEqProposition.decEq

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

Equations

• Cslib.Logic.PL.instBEqProposition.beq (Cslib.Logic.PL.Proposition.atom a) (Cslib.Logic.PL.Proposition.atom b) = (a == b)
• Cslib.Logic.PL.instBEqProposition.beq (a.and a_1) (b.and b_1) = (Cslib.Logic.PL.instBEqProposition.beq a b && Cslib.Logic.PL.instBEqProposition.beq a_1 b_1)
• Cslib.Logic.PL.instBEqProposition.beq (a.or a_1) (b.or b_1) = (Cslib.Logic.PL.instBEqProposition.beq a b && Cslib.Logic.PL.instBEqProposition.beq a_1 b_1)
• Cslib.Logic.PL.instBEqProposition.beq (a.imp a_1) (b.imp b_1) = (Cslib.Logic.PL.instBEqProposition.beq a b && Cslib.Logic.PL.instBEqProposition.beq a_1 b_1)
• Cslib.Logic.PL.instBEqProposition.beq x✝¹ x✝ = false

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instBEqProposition = { beq := Cslib.Logic.PL.instBEqProposition.beq }

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instBotProposition = { bot := Cslib.Logic.PL.Proposition.atom ⊥ }

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instInhabitedOfBot = { default := ⊥ }

@[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 → ⊥

Equations

• x✝.neg = x✝.imp ⊥

@[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).

Equations

• Cslib.Logic.PL.Proposition.top = (Cslib.Logic.PL.Proposition.atom default).imp (Cslib.Logic.PL.Proposition.atom default)

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instTopProposition = { top := Cslib.Logic.PL.Proposition.top }

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instHasAndProposition = { and := Cslib.Logic.PL.Proposition.and }

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instHasOrProposition = { or := Cslib.Logic.PL.Proposition.or }

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instHasImpProposition = { imp := Cslib.Logic.PL.Proposition.imp }

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.instHasNotPropositionOfBot = { not := Cslib.Logic.PL.Proposition.neg }

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.

Equations

• Cslib.Logic.PL.Proposition.subst f (Cslib.Logic.PL.Proposition.atom x_1) = f x_1
• Cslib.Logic.PL.Proposition.subst f (A.and B) = Cslib.Logic.HasAnd.and (Cslib.Logic.PL.Proposition.subst f A) (Cslib.Logic.PL.Proposition.subst f B)
• Cslib.Logic.PL.Proposition.subst f (A.or B) = Cslib.Logic.HasOr.or (Cslib.Logic.PL.Proposition.subst f A) (Cslib.Logic.PL.Proposition.subst f B)
• Cslib.Logic.PL.Proposition.subst f (A.imp B) = Cslib.Logic.HasImp.imp (Cslib.Logic.PL.Proposition.subst f A) (Cslib.Logic.PL.Proposition.subst f B)

@[instance_reducible]

instance Cslib.Logic.PL.instMonadProposition : Monad Proposition

Equations

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

@[reducible, inline]

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

Theories are arbitrary sets of propositions.

Equations

• Cslib.Logic.PL.Theory Atom = Set (Cslib.Logic.PL.Proposition Atom)

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.

Equations

• T.subst f = (fun (x : Cslib.Logic.PL.Proposition Atom) => x >>= f) '' T

@[instance_reducible]

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

Equations

• Cslib.Logic.PL.Theory.instFunctor = { map := fun {α β : Type ?u.1} (f : α → β) => Set.image fun (x : Cslib.Logic.PL.Proposition α) => f <$> x }

@[reducible, inline]

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

The empty theory corresponds to minimal propositional logic.

Equations

• Cslib.Logic.PL.Theory.MPL Atom = ∅

@[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).

Equations

• Cslib.Logic.PL.Theory.IPL Atom = {x : Cslib.Logic.PL.Proposition Atom | ∃ (A : Cslib.Logic.PL.Proposition Atom), Cslib.Logic.HasImp.imp ⊥ A = x}

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.

Equations

• T.intuitionisticCompletion = WithBot.some <$> T ∪ Cslib.Logic.PL.Theory.IPL (WithBot Atom)

@[reducible, inline]

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

Classical logic further adds double negation elimination.

Equations

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

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.