Due in class on Monday October 3rd.
0. [0 Points] Subscribe to the course mailing list. All students in COS 441 are required to sign up for the class mailing list. If you have questions about assignments or other information you can send email to cos441 "atsign" lists.cs.princeton.edu.
To subscribe to the list go to https://lists.cs.princeton.edu/mailman/listinfo/cos441.
One of the important elements of this class is learning how to write down proofs of properties in a clear, precise and exacting fashion. You will be graded both on correctness and clarity of your proofs. Hand-waving is not acceptable! Normally, you will lay out your proofs in a similar way as in this document. In particular, always remember to state the proof methodology you are using in your proof ("Induction on ..."). Points will be automatically deducted from answers in which the proof methodology is not stated clearly.
There are 25 points to gain on this assignment.
1. Recall the following inductive definitions of natural numbers and addition from class:
|- N nat
----------- -------------
|- Z nat |- S N nat
|- add N1 N2 N3
------------------- ------------------------------
|- add Z N N |- add (S N1) N2 (S N3)
(a) [3 Points] Prove that for all N1, N2, N3:
If |- add N1 N2 N3 then |- add N2 N1 N3.
(b) [3 Points] Inductively define multiplication as the repeated addition of natural numbers. Here is the judgment form:
|- mult N1 N2 N3
The following are valid judgments (among many others of course):
|- mult Z (S Z) Z
|- mult (S Z) (S Z) (S Z)
|- mult (S S Z) (S S Z) (S S S S Z)
(c) [6 Points] Show that the (|- mult N1 N2 N3) relation you define is also a total function. In other words, prove two things:
i) It is a function: If (|- mult N1 N2 N3) then N3 is unique. (ie: there is no N4 such that N4 is not N3 and (|- mult N1 N2 N4) ).
ii) It is total: For all N1, N2, there exists an N3 such that (|- mult N1 N2 N3).
You may assume any true property of addition that you want. State any property you use as a lemma before using it. Ie: at the beginning of your proof, say something like:
Lemma 1: If ... then ....
and then in your proof, refer to the lemma. eg:
|- ....
(by Lemma 1 and facts 17,18)
(d) [2
Points] Convert
the following recursive equations into an inductively defined relation
fact(zero) = succ(zero)
fact(succ(X)) = mult(succ(X), fact(X))
2. Here is the definition of intuitionistic propositional logic with implication, conjunction and truth:
------------------ hyp
G1, F, G2 |- F
G,F1 |- F2 G |- F1 => F2 G |- F1
----------------- =>I ---------------------------------- =>E
G |- F1 => F2 G |- F2
G |- F1 G |- F2 G |- F1 /\ F2 G |- F1 /\ F2
----------------------- /\I ------------------ /\E1 ------------------ /\E2
G |- F1 /\ F2 G |- F1 G |- F2
------------- True I (no elimination rule for true)
G |- True
(a)
[2 Points] Prove the following judgements are valid:
i) . |- (A /\ (B /\ C)) => ((A /\ B) /\ C)
ii) C |- (C => B) => B
(b) [4 Points] Prove that this logic obeys the standard Weakening Lemma:
Weakening Lemma: If G |- F then G,F' |- F.
Intuitively, Weakening says that adding extra unnecessary "junk" to the context (such as F') does not prevent us from proving formulas true. Your proof may use the Exchange Lemma:
Exchange Lemma: If G1,F1,F2,G2 |- F then G1,F2,F1,G2 |- F.
You only need to show the cases of your proof for the rules (True I), (hyp), (=>I), (=>E).
(c) [2 Points] Lets extend the logic with falsehood:
i) Give a single (natural deduction style) inference rule for the connective "False." As usual, your rule for false should only involve the connective "False" and no other connectives. Is it an introduction rule or an elimination rule?
ii) Using your rule for False, prove that for all formulas A, |- False => A
(d) [3 Points] Let's extend the logic with disjunction. Here are the introduction rules for disjunction:
G |- F1 G |- F2
---------------- \/I1 ---------------- \/I2
G |- F1 \/ F2 G |- F1 \/ F2
i) What is(are) the elimination rule(s) for disjunction? Hint: To formulate elimination rule(s), think about how one uses the information F1 \/ F2 is true to prove some other formula F3 is true. Once again, the rules for disjunction are only allowed to involve the disjunction connective and judgmental notions. Your rules should not contain any other connectives (false, =>, etc.)The following judgments should be true (you do not have to prove them, but you might want to check that your rules make these judgments true):
. |- F1 => F1 \/ F2
. |- F2 => F1 \/ F2
. |- (false \/ F) => F
. |- F => (false \/ F)
. |- (F1 \/ F2) => (F2 \/ F1)
. |- ((F1 \/ F2) \/ F3) => (F1 \/ (F2 \/ F3))
. |- true \/ F
. |- ((F1 => F3) /\ (F2 => F3)) => ((F1 \/ F2) => F3)
ii) Use your rules to prove that disjunction is associative:
. |- ((F1 \/ F2) \/ F3) => (F1 \/ (F2 \/ F3))