Reasoning in intuitionistic logic

Please submit your module(s) by Email to <jlu@dcs.ed.ac.uk>

Module logic Import lib_logic;

In order to process this Module declaration when you have Lego started, you must either use the Process Buffer menu item (or ^C^B), or load the file explicitly in Lego with the command "Make logic" (where logic is the filename -- Lego will complain if the filename doesn't match the Module name).

1. Declare P, Q and R to be propositions. Prove the following simple properties about conjunction and disjunction:
   1. Goal and_comm: (and P Q)->(and Q P);

   2. Goal or_comm: (or P Q)->(or Q P);

   3. Goal or_imp:(or (P->Q) (P->R))->(P->(or Q R));

   4. Goal and_imp_or: (and P Q)->(or P Q);

2. Prove that the following three laws are equivalent:

   Excluded Middle

   {P:Prop}or P (not P)

   Double Negation

   {P:Prop}(not (not P))->P

   Peirce

   {P,Q:Prop}((P->Q)->P)->P

   To save some typing, you can define abbreviations in Lego for these things by putting the following commands in your file:

    
   [EM = {P:Prop}or P (not P)]; 
   [DN = {P:Prop}(not (not P))->P];
   [Peirce = {P,Q:Prop}((P->Q)->P)->P];
   

   To show these three things are equivalent, you must show any one of them implies the other two. You do not need to prove all six implications directly. You could do this by proving a cycle of implications, for example EM->DN->Peirce->EM, or by proving two equivalences, for example EM->DN and DN->EM and Peirce->DN and DN->Peirce. Some of the implications are easier than others, so it is a good idea to think about which ones you want to prove.

   NOTE: Be sure you are trying to prove the right goal! In Lego, the scope of a quantifier extends as far to the right as possible if not limited by explicit parentheses. For example, if you write

   Goal {P:Prop}or P (not P) ->{P:Prop}(not (not P))->P;
   

   then Lego will parse this as

   Goal {P:Prop}(or P ((not P) ->{P:Prop}(not (not P))->P));
   

   which is probably not what you wanted. You would need to write

   Goal ({P:Prop}or P (not P)) ->{P:Prop}(not (not P))->P;
   

   to get what you want for this exercise.

   Hint: Remember that these are quantified formulas, so the P and Q may be instantiated to any formula.

   A shortcut when using negation: If you have a goal which you want to prove by absurd_elim, and you wish to do this by using some assumption H: not A and then proving a proof of A, you can do this in one step with Refine H.

   Recall that not A is defined as A->absurd. To prove a negation by proving A->absurd, use the capitalized "Intros", which reduces the goal before introducing assumptions. For example:

     ?0 : not A
   Lego> Intros x;
   Intros x;
   Intros (1) x
     x : A
     ?1 : absurd
   Lego> 
   

3. Prove {P:Prop} not(not ((not(not P)) -> P)). Note the parentheses. Although the law of double negation elimination (shown above) is not provable constructively, this shows that its double negation is provable.