Functional Programming and Type Theory ChungAng University, Fall 2003
Homework in natural deduction for propositional logic

Deadline: Wednesday Dec 3, at 3 pm

Implement the natural deduction rules for constructive propositional logic in Haskell using the technique which was presented last week on the blackboard!

The main idea is that a proposition is implemented as a type and a proof as a program, proof rules are functions. So, you should implement the following type constructors: 

And, Or, Implies, Neg, Falsity, Truth
and functions for the introduction and elimination rules like: 
Andintro, Orintro1, Orintro2, Implyintro, Negintro, Truthintro, andel,
orel,
etc.

Sorry! I think that Falsity is not possible to define in Haskell, neither is negation, but if you have an idea how to do it I would appreciate to see it. Otherwise you can skip that part of the exercise.

If you have forgotten the rules, you can find them on the net, e.g. this one from Sweden and this one from USA.

As an example, the implementation of And consists of the following definitions: 

And A B = data Andintro A B end
andelim :: (and A B) -> (A -> B -> C) -> C
andelim = ...
Maybe it is possible to use infix syntax for the logical connectives, then your formulae look nicer. Now you can prove (i.e. find a program for) the following propositions:
  1. Implies P P
  2. Implies P (Implies Q P)
  3. Implies (And P Q) P
  4. Implies P (Or P Q)
  5. Implies P (Not (Not P))
  6. Implies (Implies P (Not P)) (Not P)
  7. Equivalence (And P Q) (And Q P)
  8. Equivalence (And (And P Q) R) (And P (And Q R))
Two propositions are equivalent if they imply each other. So the type Equivalence A B can be seen as an abbreviation for another type involving Implies and And.

More examples can be found in the link to Sweden on top of this page. Good luck!
Bengt Nordstrom


Last modified: Fri Dec 5 16:17:27 KST 2003