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, Truthand 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 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: - Implies P P
- Implies P (Implies Q P)
- Implies (And P Q) P
- Implies P (Or P Q)
- Implies P (Not (Not P))
- Implies (Implies P (Not P)) (Not P)
- Equivalence (And P Q) (And Q P)
- Equivalence (And (And P Q) R) (And P (And Q R))
` 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!
Last modified: Fri Dec 5 16:17:27 KST 2003 |