# Formation sequence for a logic formula

I will start with some definitions from An Introduction to Mathematical Logic and Type Theory: To Truth through Proof by Peter B. Andrews then give the exercise that I am working along with my attempt at a proof. My actual question will be at the bottom, if you wish to skip ahead.

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}$.

Exercise:

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 $\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.)

Partial Proof:

Suppose $\mathbf{Y}$ is a wff. If $\mathbf{Y} = \mathbf{p}$ for some proprositional variable $\mathbf{p}$ then $\mathbf{Y}_1 = \mathbf{p}$ is a formation sequence for $\mathbf{Y}$. Now assume that formulas $\mathbf{A}$ and $\mathbf{B}$ have formation sequences $\mathbf{A}_1, ..., \mathbf{A}_m$ and $\mathbf{B}_1, ..., \mathbf{B}_n$, respectively. If $\mathbf{Y} = \mathord{\sim}\mathbf{A}$ then $\mathbf{A}_1, ..., \mathbf{A}_m, \mathbf{Y}$ is a formation sequence for $\mathbf{Y}$. If $\mathbf{Y} = \left[ \mathbf{A} \lor \mathbf{B} \right]$ then $\mathbf{A}_1, ..., \mathbf{A}_m, \mathbf{B}_1, ..., \mathbf{B}_n, \mathbf{Y}$ is a formation sequence for $\mathbf{Y}$. By Metatheorem 1000, we can conclude that $\mathbf{Y}$ has a formation sequence.

Question:

Now I am stuck on the proof in the other direction. I know I need to start with "Suppose $\mathbf{Y}$ is a formula with a formation sequence $\mathbf{Y}_1, ..., \mathbf{Y}_m$." I think I need to continue from there with "Let $\mathscr{S}$ be a set of formulas satisfying conditions (i), (ii), and (iii) of the definition of the set of wffs." Now I need to show that $\mathbf{Y} \in \mathscr{S}$. I believe I need to do this by induction. I can see the idea in my head, but I am having trouble formulating it on paper (or on screen, as the case may be). I can start with a base case: "If $\mathbf{Y} = \mathbf{Y}_m = \mathbf{p}$ for some propositional variable $\mathbf{p}$, then $\mathbf{Y} \in \mathscr{S}$." The next case to consider is "If $\mathbf{Y} = \mathbf{Y}_m = \mathord{\sim} \mathbf{Y}_j$ for some $j < m$..." then what? I haven't stated a clear inductive hypothesis, and that's where I'm truly stuck. Should I proceed by induction on $m$, the length of the formation sequence for $\mathbf{Y}$? Or should I use structural induction similar to what I did for the first half of the proof?

Any pointers here would be greatly appreciated. Thanks.

-

Hint: Prove the result by (strong) induction on the length of the formation sequence. So we suppose the result is true for any formula in a formation sequence of length $\lt n$, and show the result holds for any formula in a formation sequence of length $n$.

More precisely, we want to show (by the aforementioned induction) that the collection of end formulas of our sequence of length $n$ is closed under (i),(ii), and (iii), and is therefore an element of any set $\mathscr{S}$ in the definition of the set of wffs. Once one decides what has to be done, the actual details more or less write themselves.

-
Thanks. That's where my thoughts have lead me. I'm just having trouble formulating it to my satisfaction. I guess I just need to give it a bit more thought. –  Code-Guru Aug 6 '12 at 18:09
What's "Hin"? =p –  Code-Guru Aug 6 '12 at 18:20
@Code-Guru: You might have to convince yourself that every initial segment of a formation sequence is also a formation sequence (possibly containing "irrelevant" formulae). –  Arthur Fischer Aug 6 '12 at 18:21
@Arthur I did notice that the definition allows for "unused" formulas in the formation sequence. This also means that a formula $\mathbf{Y}$ does not have a unique formation sequence! –  Code-Guru Aug 6 '12 at 18:23
Certainly a formation sequence (as defined) is not unique. For one thing, one can stutter. One could change definitions to make it unique, while one cannot for proofs. One could nake it unique, but it is a nuisance to do it if one wants sequences. What is obviously unique is the tree structure. –  André Nicolas Aug 6 '12 at 18:36

I don't think your partial proof works. You tacitly assume that because $\mathbf Y$ is a wff must be either a propositional variable, a negation, or a disjunction -- and that is true, but it is also essentially what you're trying to prove in this step, so assuming it just creates a circular argument where you're not actually proving anything.

You have the right intuition about wffs, but at this step the definition you have to work with is the one you quote, and only that. What you're proving in the exercise is essentially that the definition does produce the set that you already have an intuition about. (I imagine that your intuition is actually better captured by the "formation sequence" concept than by the actual definition your text has selected).

What you should be doing in that step is something like: Let $\mathscr F$ be the set of all symbol strings that have a formation sequence. Prove that $\mathscr F$ satisfies the conditions for being one of the $\mathscr S$s being intersected in definition 1. Then, since a wff $\mathbf Y$ is by definition a member of the intersection, it is also a member of $\mathscr F$, and so $\mathbf Y$ must have a formation sequence.

In the other direction, consider an arbitrary $\mathscr S$ from the definition, and an arbitrary formation sequence. Prove that every formula in the sequence is in $\mathscr S$, by long induction on its position in the sequence. Since $\mathscr S$ and the formation sequence were both arbitary, this proves that every $\mathbf Y$ that has a formation sequence is in every $\mathscr S$, and therefore also in the intersection of the $\mathscr S$s -- so it is a wff.

Later in the course you will (probably; I don't have your book) notice a similar situation with the definitions of what the set of theorems in a theory is. The set of logical consequences of a collection of axioms can be defined either as the intersection of all sets $\mathscr R$ of wffs such that $\mathscr R$ contains the axioms and is closed under rules of inference, or as the set of wffs that have formal proofs. And the relation between those two definitions is exactly the same as the relation between the two characterizations of "well-formed formula" you're proving to be equivalent here.

-
Note that Code-Guru also has this Metatheorem 1000, which would itself easily prove that every wff is either a propositional variable, a negation or a disjunction. A proper use of this (meta)theorem should be enough to assuage your thoughts of deficient rigour. –  Arthur Fischer Aug 6 '12 at 19:15
@ArthurFischer: Okay, right. (It surprises me a bit that that metatheorem would come before this exercise; I would have done them in the opposite direction. But perhaps I have a bias for thinking in terms of syntactic witnesses where possible, rather than elegant-but-nonconstructive huge intersections). –  Henning Makholm Aug 6 '12 at 19:20
Perhaps one part of the confusion here is that the section titled "Partial Proof" is the proof that if $\mathbf{Y}$ is a wff then it has a formation sequence. Since I first assume that $\mathbf{Y}$ is in fact a wff, it is perfectly okay to assume that it has one of the three forms. On the other hand, my "Question" is about going the other direction by assuming that $\mathbf{Y}$ has a formation sequence and then proving that it has a wff. Of course, I am reading your first sentence about my partial proof not working as referring to my headings. –  Code-Guru Aug 6 '12 at 19:49
If you are referring to my "partial proof" under the "Question" heading, then I can see how I might be using some circular logic in trying to prove that $\mathbf{Y}$ is a wff. –  Code-Guru Aug 6 '12 at 19:50
@ArthurFischer Thanks for giving that link (which is hidden in my question). I have added the theorem for clarity. I intended to do this originally... –  Code-Guru Aug 6 '12 at 19:53