2
$\begingroup$

I will start with definitions, theorems, and a few solved exercises which I am taking as theorems now. My actual question will be last, if you want to scroll ahead to see it.

Definitions:

(1) The set of wffs is the intersection of all sets $\mathscr{S}$ of formulas such that:

(i) $\mathbf{p} \in \mathscr{S}$ for each propositional variable $\mathbf{p}$.

(ii) For each formula $\mathbf{A}$ if $\mathbf{A} \in \mathscr{S}$, then $\mathord{\sim} \mathbf{A} \in \mathscr{S}$.

(iii) For all formulas $\mathbf{A}$ and $\mathscr{B}$, if $\mathbf{A} \in \mathscr{S}$ and $\mathbf{B} \in \mathscr{S}$, then $\left[\mathbf{A} \lor \mathbf{B} \right] \in \mathscr{S}$.

(2) A wff is a member of the set of wffs.

Theorems:

1000 Principle of Induction on the Construction of a Wff. Let $\mathscr{R}$ be a property of formulas, and let $\mathscr{R}(\mathbf{A})$ mean that $\mathbf{A}$ has property $\mathscr{R}$. Suppose

(1) $\mathscr{R}(\mathbf{q})$ for each propositional variable $\mathbf{q}$.

(2) Whenever $\mathscr{R}(\mathbf{A})$, then $\mathscr{R}(\mathord{\sim} \mathbf{A})$.

(3) Whenever $\mathscr{R}(\mathbf{A})$ and $\mathscr{R}(\mathbf{B})$, then $\mathscr{R}([\mathbf{A} \lor \mathbf{B}])$.

Then every wff has property $\mathscr{R}$.

Completed Exercises which can be used as Theorems:

X1000. Using the definition of the set of wffs, show that if $\mathbf{A}$ and $\mathbf{B}$ are wffs, then $\mathord{\sim} \mathbf{A}$ and $\left[\mathbf{A} \lor \mathbf{B}\right]$ are also wffs.

X1001. A formation sequence for a formula $\mathbf{Y}$ is a finite sequence $\mathbf{Y}_1, ..., \mathbf{Y}_m$ of formulas such that $\mathbf{Y}_m$ is $\mathbf{Y}$ and for each $i$ ($1 \le i \le m$), one of the following conditions holds:

(a) $\mathbf{Y}_i$ is a propositional variable;

(b) there is $j < i$ such that $\mathbf{Y}_i$ is $\mathord{\sim} \mathbf{Y}_j$;

(c) there are indices $j < i$ and $k < i$ such that $\mathbf{Y}_i$ is $\left[ \mathbf{Y}_j \lor \mathbf{Y}_k \right]$.

Prove that a formula $\mathbf{Y}$ is well-formed iff it has a formation sequence. (Hint: Metatheorem 1000 may be useful.)

X1002. Prove that every wff is of the form $\mathbf{p}$ for some propositional variable $\mathbf{p}$, or of the form $\mathord{\sim} \mathbf{A}$ or $\left[\mathbf{A} \lor \mathbf{B}\right]$ for some wffs $\mathbf{A}$ and $\mathbf{B}$.

Current Exercise:

Using the results above, describe an effective procedure which can be used to determine of an arbitrary formula $\mathbf{Y}$ whether or not it is a wf, and prove that this procedure is correct.

My Effective Procedure:

Suppose $\mathbf{X}$ is a formula. If $\mathbf{X}$ is a propositional variable, then $\mathbf{X}$ is wf. If $\mathbf{X}$ is $\mathord{\sim} \mathbf{Y}$ for some formula $\mathbf{Y}$, then $\mathbf{X}$ is wf iff $\mathbf{Y}$ is wf. If $\mathbf{X}$ is $\left[ \mathbf{Y} \right]$ for some formula $\mathbf{Y}$, then proceed as follows:

  • If $\mathbf{Y}$ contains no occurence of $\lor$, then $\mathbf{Y}$ is not wf.
  • Otherwise, for the $i$th occurrence of $\lor$ in $\mathbf{Y}$, let $\mathbf{Y}$ be $\mathbf{A}_i \lor \mathbf{B}_i$. $\mathbf{X}$ is wf iff $\mathbf{A}_i$ and $\mathbf{B}_i$ are both wf for some integer $i$ with $1 \le i \le n$ where $\mathbf{Y}$ contains $n$ occurrences of $\lor$.

If none of the previous conditions applies, then $\mathbf{X}$ is not wf.

Proof that Effective Procedure is Correct:

We proceed by proof by duh!

Serious attempt at a proof:

Suppose $\mathbf{X}$is a wff. By X1002, $\mathbf{X}$ is of the form $\mathbf{p}$ for some propositional variable $\mathbf{p}$, or of the form $\mathord{\sim} \mathbf{A}$ or $\left[\mathbf{A} \lor \mathbf{B}\right]$ for some wffs $\mathbf{A}$ and $\mathbf{B}$. If $\mathbf{X}$ is of the form $\mathbf{p}$ for some propositional variable $\mathbf{p}$ then the algorithm correctly reports that $\mathbf{X}$ is wf. If $\mathbf{X}$ is of the form $\mathord{\sim} \mathbf{A}$ for some wff $\mathbf{A}$, the the algorithm also clearly gives the correct result.

Edited Question:

Now I'm stuck on the third case. I need to show that if $\mathbf{X}$ is of the form $\left[\mathbf{A} \lor \mathbf{B}\right]$ for some wffs $\mathbf{A}$ and $\mathbf{B}$ then the algorithm correctly reports that $\mathbf{X}$ is wf. I'm uncertain that simply stating that this is obvious is sufficient.

Does anyone have any suggestions?

  • 0
    @AndreasBlass Thanks for the comment. Efficiency isn't my primary concern here. I could (relatively) easily write a LALR parser, but that might be overkill. If/when I want to actually implement such an algorithm, I will certainly revisit the trade-off between run-time efficiency and amount of time to write and debug the code.2012-11-13

0 Answers 0