# Proving that an effective procedure is correct

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?

-
"duh" is induction. – André Nicolas Aug 31 '12 at 1:38
If you want to show something is effective, you could develop a coding for the variables and logical symbols and then write a Turing Machine that carries out your algorithm. Again to prove that the algorithm works, you would still need induction. – William Aug 31 '12 at 1:48
@William I'm more of a programmer than a mathematician. I could probably code a wff parser in one of several languages in a few minutes. I'm a little OCD as well, so I agonize (perhaps a little too much) over the details in my math studies (and in my programming). – Code-Guru Aug 31 '12 at 1:51
@Code-Guru That is fine. Most programming languages can simulate arbitrary Turing Machines and Turing Machine can simulate most programming languages. But most of the time, no one ever writes a Turing machine to prove something is effective. They usually use the Church-Turing Thesis and essentially conclude that if you think you can carry this out by hand, then it is probably effective. – William Aug 31 '12 at 1:56
@Code-Guru: Although your algorithm is correct, if you put on your programmer hat for a moment you'll see that it's likely to be very inefficient (exponential time) because it tries every occurrence of $\lor$ as a break point. The right break point can be found more efficiently by counting brackets. – Andreas Blass Nov 10 '12 at 17:18