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

Associative And

Methods

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

Symmetric And

Methods

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

DistributiveR Or And

Methods

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

DistributiveR And Or

Methods

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

DistributiveR And And

Methods

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

DistributiveL Or And

Methods

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

DistributiveL And Or

Methods

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

DistributiveL And And

Methods

distributiveL :: Proof (And p (And q r) == And (And p q) (And p 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

Associative Or

Methods

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

Symmetric Or

Methods

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

DistributiveR Or Or

Methods

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

DistributiveR Or And

Methods

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

DistributiveR And Or

Methods

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

DistributiveL Or Or

Methods

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

DistributiveL Or And

Methods

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

DistributiveL And Or

Methods

distributiveL :: Proof (And p (Or q r) == Or (And p q) (And p 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.

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

Prove "P and Q" from P and Q.

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

Prove "P or Q" from P.

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

Prove "P or Q" from Q.

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

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

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

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

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

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

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

Prove a contradiction from P and "not P".

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

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

univ_intro :: (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.

ex_intro :: 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.

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

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

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

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

and_elim :: (p && q) -> Proof (p, q)

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

or_elim :: (p -> Proof r) -> (q -> Proof r) -> (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.

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

Eliminate the first alternative in a conjunction.

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

Eliminate the second alternative in a conjunction.

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

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

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

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

modus_tollens :: (p --> q) -> 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)
                 q,           Not q    
              --------------------------        (contradicts')
                      FALSE
          ------------------------------------- (not-intro)
                             Not p

We can encode this proof tree more-or-less directly as a Proof to implement modus_tollens:

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

modus_tollens impl q' =
  do  modus_ponens impl
   |. contradicts' q'
   |\ not_intro

absurd :: FALSE -> Proof p

From a falsity, prove anything.

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

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

ex_elim :: (forall c. p c -> Proof q) -> 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 :: forall p. Classical => (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 => (Not p -> Proof FALSE) -> p
not_intro      ::              (p     -> Proof FALSE) -> 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 =
  do  lem             -- introduce p || Not p
   |$ or_elimL given  -- dispatch the first, straightforward case
   |/ impl            -- Now we're on the second case. Apply the implication..
   |. absurd          -- .. and, from falsity, conclude p.

not_not_elim :: Classical => 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". not_not_elim p'' = contradiction (contradicts' p'')

Mapping over conjunctions and disjunctions

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

Apply a derivation to the left side of a conjunction.

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

Apply a derivation to the right side of a conjunction.

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

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

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

Apply a derivation to the left side of a disjunction.

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

Apply a derivation to the right side of a disjunction.

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

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

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

Apply a derivation to the left side of an implication.

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

Apply a derivation to the right side of an implication.

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

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

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

Apply a derivation inside of a negation.