Problem Set 5

Due Date: Thurs, Feb 27

Reading

Please study Smullyan, Chapter XI, p. 101-108, and skim Chapter IV, p. 43-51 for Thurs, Feb 27.

Problems

1. Give a top-down Gentzen proof of formulas (2), (4), (6), and (8) on page 24.

2. Recall the lecture presentation of Smullyan's definition of a tree. A tree is a 4-tuple $<s,a,p,f>$ where $S$ is a set of nodes, $a \in S$, $p$ maps $\{x:S\vert x \neq a\}$ into $S$; it computes the predecessor of a node, the function $f$ maps $S$ to $\mathbb{N}^+=\{1,2,3, \dots\}.$ The two axioms are:

   Ax 1. For all $x$ in $S$, $f(x)=1$ iff $x=a.$

   Ax 2. For all $x$ in $S$, $f(x)=f(p(x))+1.$

   Define $L(i)=\{x:S\vert f(x)=i\}.$

   Prove carefully that $L(i+1)=\{x:S\vert p(x)\in L(i)\}$ and describe the result graphically.

3. Recall that Refinement Logic is a single conclusion (top down) Gentzen system in which the rule $\frac{H \vdash P \vee Q}{H \vdash P,Q}$ is replaced by $\frac{H \vdash P \vee Q}{H \vdash P}$ or $\frac{H \vdash P \vee Q}{H \vdash Q}$ and the rule $\frac{H \vdash G}{H,X \vee \sim X \vdash G}$ for any formula $x$.

   Prove the following formulas in Refinement Logic:

   1. $((P \supset Q) \supset P)\supset P$
   2. $(P \supset Q) \supset \; \sim Q \supset \sim P$
   3. $(\sim Q \supset \sim P) \supset (P \supset Q)$
   4. $\sim (P \vee Q) \supset \; \sim P \; \vee \sim Q$

4. Write down the rules for a Gentzen system based on the Sheffer stroke and one based on joint denial (see p. 14 of Smullyan and p.30).

5. Produce Tableau rules and Refinement rules for a logic with the constants $t,f$ (Smullyan, p. 13), but without $\sim$. Define $\sim P$ as $P \supset f$ and show how to replace any deduction using the $\sim$ rules by one using $P \supset f$ instead.