Problem Set 7

Due Date: Thurs, March 13, 2003

Reading

Please read the handout on second order propositional logic (on either the 2001 or 2003 CS486 web site); Smullyan, Chapter IV, p. 43-52; and Suppes' Introduction to Logic, pages 43-54.

Problems

1. Give Refinement logic rules for $P^2.$

2. Prove or disprove these $P^2$ formulas:
   1. $\forall p \forall q((p \supset q)\supset((p \supset \perp) \supset (q \supset \perp)))$

   2. $\forall p \exists q ((p \supset q) \supset ((p \supset \perp) \supset (q \supset \perp )))$

   3. $(\forall p (\sim p)) \supset \neg \;\exists\; p(p)$

   4. $\forall p \exists q ((p \vee q) \supset p)$

   5. $\forall p \exists q((p \vee q) \wedge \sim(p \wedge q))$

3. Reduce these $P^2$ formulas to $P^0$ formulas.
   1. $\forall p(p) \supset \perp$

   2. $\forall p \forall q ((\sim p \vee q) \supset (p \supset q))$

   3. $\forall p \forall q ((p \supset p \vee q)\wedge(p \wedge q \supset p))$

4. Solve exercise 4, page 50 of Smullyan.

5. Solve exercise 3, page 52 of Smullyan.

6. Solve exercise 2, page 55 of Suppes' Introduction to Logic.

7. There is a simple proof for cut elimination in $P^2$. State the theorem and outline a proof. Details are not necessary.

Optional Problem:

Develop the idea that Refinement Logic is a calculus of ``problems.'' Try to define the idea of a problem $P$ and a solution for it, say $s$. Use a semantics based on the idea that $s$ solves $P$.