Logic.Propositional

First-order Logic

Logical symbols

data TRUE

The constant "true".

data FALSE

The constant "false".

data And p q infixl 3

The conjunction of p and q.

Instances

Symmetric (And :: k -> k -> Type)

Defined in Logic.Propositional

Methods

symmetric :: Proof (And p q) -> Proof (And q p)

DistributiveR (And :: Type -> k -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveR :: Proof (And (And p q) r == And (And p r) (And q r))

DistributiveR (Or :: Type -> k -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveR :: Proof (Or (And p q) r == And (Or p r) (Or q r))

DistributiveR (And :: Type -> k -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveR :: Proof (And (Or p q) r == Or (And p r) (And q r))

DistributiveL (And :: k -> Type -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveL :: Proof (And p (And q r) == And (And p q) (And p r))

DistributiveL (Or :: k -> Type -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveL :: Proof (Or p (And q r) == And (Or p q) (Or p r))

DistributiveL (And :: k -> Type -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveL :: Proof (And p (Or q r) == Or (And p q) (And p r))

Associative (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

associative :: Proof (And p (And q r) == And (And p q) r)

type (&&) p q = p `And` q infixl 3

An infix alias for And.

type (∧) p q = p `And` q infixl 3

An infix alias for And.

type (/\) p q = p `And` q infixl 3

An infix alias for And.

data Or p q infixl 2

The disjunction of p and q.

Instances

Symmetric (Or :: k -> k -> Type)

Defined in Logic.Propositional

Methods

symmetric :: Proof (Or p q) -> Proof (Or q p)

DistributiveR (Or :: Type -> k -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveR :: Proof (Or (Or p q) r == Or (Or p r) (Or q r))

DistributiveR (Or :: Type -> k -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveR :: Proof (Or (And p q) r == And (Or p r) (Or q r))

DistributiveR (And :: Type -> k -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveR :: Proof (And (Or p q) r == Or (And p r) (And q r))

DistributiveL (Or :: k -> Type -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveL :: Proof (Or p (Or q r) == Or (Or p q) (Or p r))

DistributiveL (Or :: k -> Type -> Type) (And :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveL :: Proof (Or p (And q r) == And (Or p q) (Or p r))

DistributiveL (And :: k -> Type -> Type) (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

distributiveL :: Proof (And p (Or q r) == Or (And p q) (And p r))

Associative (Or :: Type -> Type -> Type)

Defined in Logic.Propositional

Methods

associative :: Proof (Or p (Or q r) == Or (Or p q) r)

type (||) p q = p `Or` q infixl 2

An infix alias for Or.

type (∨) p q = p `Or` q infixl 2

An infix alias for Or.

type (\/) p q = p `Or` q infixl 2

An infix alias for Or.

data Implies p q infixr 1

The implication "p implies q".

type (-->) p q = p `Implies` q infixr 1

An infix alias for Implies.

data Not p

The negation of p.

data ForAll x p

Universal quantification.

data Exists x p

Existential quantifiation.

Natural deduction

Tautologies

true :: Proof TRUE

TRUE is always true, and can be introduced into a proof at any time.

noncontra :: Proof (Not (p && Not p))

The Law of Noncontradiction: for any proposition P, "P and not-P" is false.

Introduction rules

Introduction rules give the elementary building blocks for creating a formula from simpler ones.

introAnd :: Proof p -> Proof q -> Proof (p && q)

Prove "P and Q" from P and Q.

introAnd' :: Proof q -> Proof p -> Proof (p && q)

Prove "P and Q" from Q and P.

introOrL :: Proof p -> Proof (p || q)

Prove "P or Q" from P.

introOrR :: Proof q -> Proof (p || q)

Prove "P or Q" from Q.

introImpl :: (Proof p -> Proof q) -> Proof (p --> q)

Prove "P implies Q" by demonstrating that, from the assumption P, you can prove Q.

introNot :: (Proof p -> Proof FALSE) -> Proof (Not p)

Prove "not P" by demonstrating that, from the assumption P, you can derive a false conclusion.

contrapositive :: (Proof p -> Proof FALSE) -> Proof (Not p)

contrapositive is an alias for introNot, with a somewhat more suggestive name. Not-introduction corresponds to the proof technique "proof by contrapositive".

contradicts :: Proof p -> Proof (Not p) -> Proof FALSE

Prove a contradiction from P and "not P".

contradicts' :: Proof (Not p) -> Proof p -> Proof FALSE

contradicts' is contradicts with the arguments flipped. It is useful when you want to partially apply contradicts to a negation.

introUniv :: (forall c. Proof (p c)) -> Proof (ForAll x (p x))

Prove "For all x, P(x)" from a proof of P(*c*) with *c* indeterminate.

introEx :: Proof (p c) -> Proof (Exists x (p x))

Prove "There exists an x such that P(x)" from a specific instance of P(c).

Elimination rules

Elimination rules give the elementary building blocks for decomposing a complex formula into simpler ones.

elimAndL :: Proof (p && q) -> Proof p

From the assumption "P and Q", produce a proof of P.

elimAndR :: Proof (p && q) -> Proof q

From the assumption "P and Q", produce a proof of Q.

elimOr :: (Proof p -> Proof r) -> (Proof q -> Proof r) -> Proof (p || q) -> Proof r

If you have a proof of R from P, and a proof of R from Q, then convert "P or Q" into a proof of R.

elimOrL :: (Proof p -> Proof r) -> Proof (p || q) -> (Proof q -> Proof r) -> Proof r

Eliminate the first alternative in a conjunction.

elimOrR :: (Proof q -> Proof r) -> Proof (p || q) -> (Proof p -> Proof r) -> Proof r

Eliminate the second alternative in a conjunction.

elimImpl :: Proof p -> Proof (p --> q) -> Proof q

Given "P imples Q" and P, produce a proof of Q. (modus ponens)

modusPonens :: Proof (p --> q) -> Proof p -> Proof q

modusPonens is just elimImpl with the arguments flipped. In this form, it is useful for partially applying an implication.

modusTollens :: Proof (p --> q) -> Proof (Not q) -> Proof (Not p)

Modus tollens lets you prove "Not P" from "P implies Q" and "Not Q".

Modus tollens is not fundamental, and can be derived from other rules:

                                  -----         (assumption)
                        p --> q,    p
                       ---------------------    (modus ponens)
               Not q,            q
              --------------------------        (contradicts')
                      FALSE
          ------------------------------------- (not-intro)
                             Not p

We can encode this proof tree as a Proof to implement modus_tollens:

modusTollens :: Proof (p --> q) -> Proof (Not q) -> Proof (Not p)
modusTollens impl q' = introNot $ p -> contradicts' q' (modusPonens impl p)

absurd :: Proof FALSE -> Proof p

From a falsity, prove anything.

elimUniv :: Proof (ForAll x (p x)) -> Proof (p c)

Given "For all x, P(x)" and any c, prove the proposition "P(c)".

elimEx :: (forall c. Proof (p c) -> Proof q) -> Proof (Exists x (p x)) -> Proof q

Given a proof of Q from P(c) with c generic, and the statement "There exists an x such that P(x)", produce a proof of Q.

Classical logic and the Law of the Excluded Middle

class Classical

The inference rules so far have all been valid in constructive logic. Proofs in classical logic are also allowed, but will be constrained by the Classical typeclass.

classically :: (Classical => Proof p) -> Proof p

Discharge a Classical constraint, by saying "I am going to allow a classical argument here."

NOTE: The existence of this function means that a proof should only be considered constructive if it does not have a Classical constraint, *and* it does not invoke classically.

lem :: Classical => Proof (p || Not p)

The Law of the Excluded Middle: for any proposition P, assert that either P is true, or Not P is true.

contradiction :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p

Proof by contradiction: this proof technique allows you to prove P by showing that, from "Not P", you can prove a falsehood.

Proof by contradiction is not a theorem of constructive logic, so it requires the Classical constraint. But note that the similar technique of proof by contrapositive (not-introduction) is valid in constructive logic! For comparison, the two types are:

contradiction  :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p
introNot       ::              (Proof      p  -> Proof FALSE) -> Proof (Not p)

The derivation of proof by contradiction from the law of the excluded middle goes like this: first, use the law of the excluded middle to prove p || Not p. Then use or-elimination to prove p for each alternative. The first alternative is immediate; for the second alternative, use the provided implication to get a proof of falsehood, from which the desired conclusion is derived.

contradiction impl = elimOr id (absurd . impl) lem

elimNot :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p

Alias for contradiction, to complete the patterns.

elimNotNot :: Classical => Proof (Not (Not p)) -> Proof p

Double-negation elimination. This is another non-constructive proof technique, so it requires the Classical constraint.

The derivation of double-negation elimination follows from proof by contradiction, since "Not (Not p)" contradicts "Not p". elimNotNot p'' = contradiction (contradicts' p'')

Mapping over conjunctions and disjunctions.

These function names mimic the ones for (FunctorBifunctorProfunctor).

firstAnd :: (Proof p -> Proof p') -> Proof (p && q) -> Proof (p' && q)

Apply a derivation to the left side of a conjunction.

secondAnd :: (Proof q -> Proof q') -> Proof (p && q) -> Proof (p && q')

Apply a derivation to the right side of a conjunction.

bimapAnd :: (Proof p -> Proof p') -> (Proof q -> Proof q') -> Proof (p && q) -> Proof (p' && q')

Apply derivations to the left and right sides of a conjunction.

firstOr :: (Proof p -> Proof p') -> Proof (p || q) -> Proof (p' || q)

Apply a derivation to the left side of a disjunction.

secondOr :: (Proof q -> Proof q') -> Proof (p || q) -> Proof (p || q')

Apply a derivation to the right side of a disjunction.

bimapOr :: (Proof p -> Proof p') -> (Proof q -> Proof q') -> Proof (p || q) -> Proof (p' || q')

Apply derivations to the left and right sides of a disjunction.

lmapImpl :: (Proof p' -> Proof p) -> Proof (p --> q) -> Proof (p' --> q)

Apply a derivation to the left side of an implication.

rmapImpl :: (Proof q -> Proof q') -> Proof (p --> q) -> Proof (p --> q')

Apply a derivation to the right side of an implication.

dimapImpl :: (Proof p' -> Proof p) -> (Proof q -> Proof q') -> Proof (p --> q) -> Proof (p' --> q')

Apply derivations to the left and right sides of an implication.

mapNot :: (Proof p' -> Proof p) -> Proof (Not p) -> Proof (Not p')

Apply a derivation inside of a negation.