Due by midnight on Monday October 1st.

For proofs: Either hand in in class, email to Kenny (kzhu@cs.princeton.edu) or deliver to Kenny's office. Please put "COS 441 A2" in the subject line of any email.

For code: email to Kenny (kzhu@cs.princeton.edu) a file named firstlastnameA2.sml where "firstlastname" is your firstname followed by your last name. eg:

davidwalkerA2.sml

Again, please put "COS 441 A2" in the subject line of any email.

There are 10 points to gain on this assignment.

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

G |- False

(no introduction rule for false) ------------- False E

G |- F

1.
[2 Points] Prove the following judgements are valid:

i) . |- (A /\ (B /\ C)) => ((A /\ B) /\ C)

ii) C |- (C => B) => B

2. [3 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).

3. Implement propositional intuitionistic logic formulas:

eg:

datatype form =

PropF of string

| TrueF

| ...

| AndF of form * form

Optional, ungraded exercise. if you would like more practice programming in ML, try the following exercise. They will not be graded but if you want feedback, you can show them to either Kenny or myself. A little extra work with ML now might help you on future assignments.

Implement an improved printer that minimizes the number of parentheses.

A perfect solution will

(("N is even") /\ ("N is multiple of 5")) /\ (("N is a multiple of 3") /\ ("N is multiple of 7"))

print:

"N is even" /\ "N is multiple of 5" /\ "N is a multiple of 3" /\ "N is multiple of 7"

- treat => as left associative. Instead of:
("N is multiple of 5" => ("N is a multiple of 3" => "N is multiple of 7"))

print:

"N is multiple of 5" => "N is a multiple of 3" => "N is multiple of 7"

but still print this formula with parens:

("N is multiple of 5" => "N is a multiple of 3") => "N is multiple of 7"

- give /\ higher precedence than => and only insert parentheses where necessary. Instead of:
(("N is multiple of 5" /\ "N is a multiple of 3") => "N is multiple of 7")

print:

"N is multiple of 5" /\ "N is a multiple of 3" => "N is multiple of 7"

- Suggestion:

- Associate each formula type with an integer precedence (2 for /\ and 1 for =>)
- Implement printform2 by introducing a helper function (printaux (prec,f)) to print formula f. When the top-most connective in f has lower precedence level than prec, print parentheses.