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 introduce notation for the logical connectives: ⊥ ⊤ ∧ ∨ → ¬ for, respectively, falsum, verum, conjunction, disjunction, implication and negation.

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

• impl {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.impl 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.impl 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.impl b_1) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.impl b) (Cslib.Logic.PL.Proposition.atom x_2) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.impl b) (a_1.and b_1) = isFalse ⋯
• Cslib.Logic.PL.instDecidableEqProposition.decEq (a.impl b) (a_1.or b_1) = isFalse ⋯

@[implicit_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

@[implicit_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 }

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.impl a_1) (b.impl 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

@[implicit_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 ⊥ }

@[implicit_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✝.impl ⊥

@[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).impl (Cslib.Logic.PL.Proposition.atom default)

@[implicit_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 }

def Cslib.Logic.PL.«term_∧_» : Lean.TrailingParserDescr

Conjunction

Equations

• Cslib.Logic.PL.«term_∧_» = Lean.ParserDescr.trailingNode `Cslib.Logic.PL.«term_∧_» 36 37 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ ") (Lean.ParserDescr.cat `term 37))

def Cslib.Logic.PL.«term_∨_» : Lean.TrailingParserDescr

Disjunction

Equations

• Cslib.Logic.PL.«term_∨_» = Lean.ParserDescr.trailingNode `Cslib.Logic.PL.«term_∨_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ ") (Lean.ParserDescr.cat `term 36))

def Cslib.Logic.PL.«term_→_» : Lean.TrailingParserDescr

Implication

Equations

• Cslib.Logic.PL.«term_→_» = Lean.ParserDescr.trailingNode `Cslib.Logic.PL.«term_→_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " → ") (Lean.ParserDescr.cat `term 31))

def Cslib.Logic.PL.«term¬_» : Lean.ParserDescr

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

Equations

• Cslib.Logic.PL.«term¬_» = Lean.ParserDescr.node `Cslib.Logic.PL.«term¬_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ¬ ") (Lean.ParserDescr.cat `term 40))

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.PL.Proposition.subst f A).and (Cslib.Logic.PL.Proposition.subst f B)
• Cslib.Logic.PL.Proposition.subst f (A.or B) = (Cslib.Logic.PL.Proposition.subst f A).or (Cslib.Logic.PL.Proposition.subst f B)
• Cslib.Logic.PL.Proposition.subst f (A.impl B) = (Cslib.Logic.PL.Proposition.subst f A).impl (Cslib.Logic.PL.Proposition.subst f B)

@[implicit_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

@[implicit_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), ⊥.impl A = x}

theorem Cslib.Logic.PL.Theory.efq_mem_ipl {Atom : Type u} [Bot Atom] (A : Proposition Atom) : ⊥.impl 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

• Cslib.Logic.PL.Theory.CPL Atom = {x : Cslib.Logic.PL.Proposition Atom | ∃ (A : Cslib.Logic.PL.Proposition Atom), A.neg.neg.impl A = x}

theorem Cslib.Logic.PL.Theory.dne_mem_cpl {Atom : Type u} [Bot Atom] (A : Proposition Atom) : A.neg.neg.impl 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 (⊥.impl 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 (A.neg.neg.impl A)

  Double-negation elimination.