80-211                                                                                                             Spring 2003

Assignment #13

Due on Wednesday, April 30th

 

Problem 1:  Prove the following claims formally using the axioms of Peano Arithmetic (stated below), the two derived rules and =R1.  You can also use previous results in your current proof, such as you can use the sequent proved in part (c) as a theorem when trying to prove part (d) (hint), since you already proved part (c). 

 

            Axioms of PA:

1. "x(~(Sx = 0))

2. "x"y(Sx = Sy → x = y)

3. [P(0) & "x(P(x) →P(s(x))]  →"xPx,  for any atomic P in the language of arithmetic

4. "x(x + 0 = x)

5. "x"y(x + s(y) = s(x + y))

6. "x(x×0 = 0)

7. "x"y(x×s(y) = x×y + x)

 

D1.  "x(0 + m = m)

D2.  "x(1 +m = s(m))

 

Note: When you were introduced to predicate logic with equality, you only had predicates and relations in the language. So the rules for equality ( = intro and = elim) were in terms of predicates and relations, but now you have functions in your language, so you will need to use the following equality rule in your proofs:

 

=R1:   "x"y"w"z((x = y & w = z) → x @ w = y @ z) where @ is either addition or multiplication.

 

So, for example by the usual = intro you know that x = x  and by axiom 4 you know that y + 0 = y, so then by =R1 you can get that x + (y + 0) = x + y                         

 

Prove:

 

(a)        PA ├ "x(0×x = 0)

 

(b)        PA ├ "x(1×x = x)

 

(c)        PA ├ "x"y"z( (x + y) + z = x + (y + z))

 

            Suggestion: Use the induction schema on z and let x and y be arbitrary terms, so then you can use UI at the end after you’ve applied the induction schema (axiom 3).  So your P(z) will be “(x + y) + z = x + (y + z)”. 

 

 

 

 

(d)        PA ├ "x"y(x + y = y + x)

 

            Suggestion: Use the induction schema on y and let x be an arbitrary term and proceed like part-c. 

 

Problem 2. Prove the following sequents using the natural deduction calculus. Note these are all sequents you have proved in old homework assignments, so you just  need to think about how to transform the old proofs into the natural deduction calculus given in class.

 

(a)        (P→Q) & (P→R) ├ P→ (Q &R)                    from HW2

(b)        P → Q ├ ~Q → ~P                                        from HW1

 

(c)        P→(Q→R) ├ (P→Q)→(P→R)                      from HW1

 

(d)        ~(P Ú Q) ├ ~P & ~Q                                      from HW4

 

(e)        ~(P & Q) ├ ~P Ú ~Q                                      from HW4

 

(f)         P→ Q ├ ~P Ú Q                                             from HW4