CS486 Problem Set 2 DUE: 2/11/03

1.

Solve the exercise on p. 24, items 1, 4, 5, and 8.

(1)

$$\begin{array}[t]{lccr}\mbox{(1)}&\mathsf{F}&{q}{\supset }{({... ...ox{(3)}\\ \multicolumn{4}{c}{\mathsf{X} \mbox{(2)}}\end{array}$$

(4)

$$\begin{array}[t]{lccr}\mbox{(1)}&\mathsf{F}&{[{({({p}{\supse... ...eauxAux} \end{array}} \end{tableauxAux} \end{array}}\end{array}$$

(5)

$$\begin{array}[t]{lccr}\mbox{(1)}&\mathsf{F}&{{\neg }{({p}{\w... ...athsf{X} \mbox{(8)}} \end{tableauxAux} \end{array}}\end{array}$$

(8)

$$\begin{array}[t]{lccr}\mbox{(1)}&\mathsf{F}&{({p}{\vee }{({q... ...lumn{4}{c}{\mbox{*}} \end{tableauxAux} \end{array}}\end{array}$$

$$\begin{array}[t]{lccr}\multicolumn{4}{c}{\mbox{*}}\\ \mbox{... ...thsf{X} \mbox{(11)}} \end{tableauxAux} \end{array}}\end{array}$$

2.

Recall that a tableaux $\mathcal{T}$ is complete if all its branches are either closed or complete, where a branch $\theta$ of a tableaux $\mathcal{T}$ is complete if for every $\alpha$ on $\theta$ both $\alpha_1$ and $\alpha_2$ occur on $\theta$ and if for every $\beta$ on $\theta$ at least one off $\beta_1$, $\beta_2$ occur on $\theta$.

We prove that the tableaux method terminates.

We generate an analytic tableaux for the unsigned formula $X$ in the following manner. At each stage, we have an ordered dyadic tree $\mathcal{T}_i$, In the first stage, we construct the tree $\mathcal{T}_1$, a one-point tree whose origin is $\mathsf{F}~X$. In the $n^{th}$ stage, we select from $\mathcal{T}_{n-1}$ the left-most branch $\theta$ that is unclosed and incomplete. From this branch, we consider all $\alpha$ on $\theta$ such that either $\alpha_1$ or $\alpha_2$ does not occur on $\theta$ and all $\beta$ on $\theta$ such that neither $\beta_1$ nor $\beta_2$ occur on $\theta$. We select the $\alpha$ or $\beta$ node that dominates all others. If we select an $\alpha$ node such that $\alpha_1$ does not occur on $\theta$, then extend $\theta$ by $\alpha_1$ to form $\mathcal{T}_n$. If we select an $\alpha$ node such that $\alpha_2$ does not occur on $\theta$, then extend $\theta$ by $\alpha_2$ to form $\mathcal{T}_n$. If we select $\beta$ node, then extend $\theta$ by $\beta_1$, $\beta_2$ to form $\mathcal{T}_n$.

We show that the above method either closes or completes any branch $\theta$ by induction on the ``size'' of the branch. Define $size(\theta)$ as follows:

$$size(\theta) = \left\{ \begin{array}{ll} 0 & \mbox{if $\t... ...& \mbox{where $x$\ is the node selected} \end{array} \right.$$

Note that an incomplete branch necessarily has an $\alpha$ or $\beta$ node selected by the above procedure; furthermore, the degree of an $\alpha$ or $\beta$ node is greater than zero. Hence $size(\theta) > 0$ for any unclosed, incomplete branch.

Suppose $size(\theta) = 0$. Then $\theta$ is closed or complete.

Suppose $size(\theta) > 0$. Suppose an $\alpha$ node is selected. In either one or two steps, we must close or complete $\theta:\alpha_1:\alpha_2$. Note $size(\theta:\alpha_1:\alpha_2) < size(\theta)$ because $deg(\alpha_1) + deg(\alpha_2) < deg(\alpha)$. Hence, by the induction hypothesis, the method closes or completes the branch. Suppose a $\beta$ node is selected. Then we must close or complete $\theta:\beta_1$ and $\theta:\beta_2$. Note $size(\theta:\beta_1) < size(\theta)$ because $deg(\beta_1) < deg(\beta)$; likewise, $size(\theta:\beta_2) < size(\theta)$ because $deg(\beta_2) < deg(\beta)$. Hence, by the induction hypothesis, the method closes or completes both branches.

Hence, the method closes or completes any branch. In particular, the method closes or completes the one-point tree whose origin is $\mathsf{F}~X$. Thus, the tableaux method terminates.

3.

We prove that any downward closed set $S$ satisfying for all signed formulas $X$, $X \in S$ iff $\overline{X} \not\in S$ is a truth set.

Let $S$ be a downward closed set satisfying for all signed formulas $X$, $X \in S$ iff $\overline{X} \not\in S$. We show that $S$ satisfies the laws of a truth set:

(0)

Show that for any $X$, exactly on of $X$, $\overline{X}$ belongs to $S$.

Let $X$ be a signed formula. If $X \in S$, then $\overline{X} \not\in S$, by the definition of $S$. If $X \not\in S$, then $\overline{X} \in S$, by the definition of $S$. Hence, exactly one of $X$, $\overline{X}$ belongs to $S$.

(a)

Show $\alpha \in S$ iff $\alpha_1 \in S$ and $\alpha_2 \in S$.

Consider $\alpha$. If $\alpha \in S$, then $\alpha_1 \in S$ and $\alpha_2 \in S$, by the definition of downward closed. Suppose $\alpha_1 \in S$ and $\alpha_2 \in S$. By way of contradiction, assume $\alpha \not\in S$. By the definition of $S$, $\overline{\alpha} \in S$. By $(J_1(a))$, $\overline{\alpha}$ is some $\beta$. Hence $\beta_1 \in S$ or $\beta_2 \in S$, by the definition of downward closed. Furthermore, by $(J_2(b))$, $\overline{\alpha_1}$ is $\beta_1$ and $\overline{\alpha_2}$ is $\beta_2$. Thus, $\overline{\alpha_1} \in S$ or $\overline{\alpha_2} \in S$. If $\overline{\alpha_1} \in S$, then $\alpha_1 \not\in S$, by definition of $S$, but contrary to the assumption. If $\overline{\alpha_2} \in S$, then $\alpha_2 \not\in S$, by the definition of $S$, but contrary to the assumption. Hence $\alpha \in S$.

(b)

Show $\beta \in S$ iff $\beta_1 \in S$ or $\beta_2 \in S$.

Consider $\beta$. If $\beta \in S$, then $\beta_1 \in S$ or $\beta_2 \in S$, by the definition of downward closed. Suppose $\beta_1 \in S$ or $\beta_2 \in S$. By way of contradiction, assume $\beta \not\in S$. By the definition of $S$, $\overline{\beta} \in S$. By $(J_1(b))$, $\overline{\beta}$ is some $\alpha$. Hence $\alpha_1 \in S$ and $\alpha_2 \in S$, by the defintion of downward closed. Furthermore, by $(J_2(a))$, $\overline{\beta_1}$ is $\alpha_1$ and $\overline{\beta_2}$ is $\alpha_2$. Thus, $\overline{\beta_1} \in S$ and $\overline{\beta_2} \in S$. Hence $\beta_1 \not\in S$ and $\beta_2 \not\in S$, by the defintion of $S$, but contrary to the assumption. Hence, $\beta \in S$.

4.

We give a recursive datatype definition for an analytic tableau.

    Form = var: Var + 
           neg: Form + 
           and: Form * Form + 
           or: Form * Form +
           imp: Form * Form
    Sign = t: Unit + f: Unit
    Tableaux = index: Nat *
               sign: Sign *
               form: Form *
               next: (closed: Int + 
                      complete: Unit +
                      alpha: Int * Tableaux + 
                      beta: Int * Tableaux * Tableaux)