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?