1
$\begingroup$

My text provides (a pretty standard, I think) recursive definition of well-formed formula:

The set of wff, denoted $\textbf{WFF}$, is the smallest set that satisfies:

  1. All propositional variables, $\textbf{p}$, and the propositional constants $\top,\bot$ are in $\textbf{WFF}$. These are called atomic formulas.
  2. If $A,B\in\textbf{WFF}$, then $(\neg A), (A\circ B)\in\textbf{WFF}$, where $\circ\in\{\land,\lor,\rightarrow,\equiv\}$

Presumably from the definition, the text relies on the fact that all formulas are strictly one of (1) atomic, (2) of the form $(\neg A)$, or of the form $(A \circ B)$ in all its proofs about formulas, and, intuitively, I can appreciate that the definition implies this.

Here's a very simple proof, presented in the text, that $\color{red}{p\lor}$ is not a formula:

$p\lor$ is clearly not atomic.

$p\lor$ does not begin with an open parenthesis, and therefore is not of the form $(\neg A)$ or $(A\circ B)$

Therefore $p\lor\notin\textbf{WFF}$

$\square$

But doesn't it still need to be proved that all formulas are either atomic, $(\neg A)$, or $(A\circ B)$? After all, in part 2. of the definition, how do we know (beyond intuition) that $A$ cannot equal $p\lor$, and therefore $\notin\textbf{WFF}$?

Edit: I realize that "smallest set" means that we "throw away" any strings that don't satisfy the definition's criteria, but how can we be sure that in condition 2., $A$ and $B$ are not of a form different from $(\neg A)$ or $(A\circ B)$? (Even though intuitively that's rather obvious, doesn't it require an explicit proof of its own?)

$\endgroup$
  • $\begingroup$ I find the start of the definition contestable. The recursive nature of the definition of WFF allows for one to argue that the set is countably infinite. But, adding a single string which is not a wff to WFF, yields a set which is still countably infinite. So, I don't see how WFF is the smallest set. $\endgroup$ – Doug Spoonwood Dec 18 '17 at 3:43
  • 1
    $\begingroup$ @DougSpoonwood Smallest in the sense of set inclusion, not in the sense of cardinality. $\endgroup$ – Alex Kruckman Dec 18 '17 at 21:24
5
$\begingroup$

In this particular example, the following direct argument would work:

Assume $W$ is a set of words that satisfies your two conditions. Then $$ W' = \{w\in W\mid w\text{ does not end with }{\lor}\} $$ will also satisfy the two conditions (which can easily be checked). Therefore, if $W$ contains any word that ends with $\lor$, it will not be the smallest set that satisfies the condition, and therefore it is not $\mathbf{WFF}$. In particular, $\mathbf{WFF}$ does not contain the word $p\lor$.

In general, we can show from the smallest-set definition that $\mathbf{WFF}$ consists of exactly those words that have a finite parse tree that matches the rules, and when you have a wff, you can therefore assume that has a parse tree.

Usually, though, when reasoning about wffs you don't need to appeal to parse trees explicitly -- almost everything you'd want to prove by picking wffs apart can be phrased as structural induction:

Suppose $\phi(w)$ is some property of strings such that

  • $\phi(w)$ holds whenever $w$ is an atomic formula.
  • Whenever $\phi(u)$ and $\phi(w)$ hold, then also $\phi((\neg w))$ and $\phi((u\circ w))$.

Then $\phi(w)$ holds for every $w\in\mathbf{WFF}$.

This is true because $\{w\in\mathbf{WFF}\mid \phi(w)\}$ is a set that satisfies the two condition, and since $\mathbf{WFF}$ is the smallest such set, it must equal $\{w\in\mathbf{WFF}\mid \phi(w)\}$.

In particular, when you have a wff, you can assume that it has one of the forms in the definition -- because "has one of those forms" is a property that works as $\phi$ in the structural induction theorem.

$\endgroup$
  • $\begingroup$ Can we have the smallest set for a countably infinite set, when there exist multiple countably infinite sets? $\endgroup$ – Doug Spoonwood Dec 18 '17 at 3:51
  • $\begingroup$ @Doug: Yes, because (as one easily sees) the intersection of any nonempty family of sets that all satisfy the condition will itself satisfy the condition. $\endgroup$ – Henning Makholm Dec 18 '17 at 11:55
4
$\begingroup$

It is because, as explicitly stated in the definition, the set WFF is the smallest set satisfying 1 and 2 (where 'smaller' is understood in terms of subsets: in this context, set $A$ is 'smaller' than set $B$ if $A$ is a strict subset of $B$)

So, if there was something $X$ in WFF that was not either atomic or of the form $A \circ B$, then WFF would not be the smallest set satisfying 1 and 2, because if there are such elements, then out of all those, pick a smallest one (i.e with the least length/number of symbols), and that element can't possibly have been forced in the set by either 1 or 2

For example, if $p\lor$ was in the set, then $(\neg p \lor)$ would by 2 be forced in the set as well, and therefore also $(\neg p\lor \land \neg p \lor)$, etc. Now, all these later 'larger' ones are thus all forced by the initial $p \lor$, and therefore removing any of those from the set would go against the set satisfying 1 and 2. However, the 'smallest' such 'nonsense' formula (or at least: a 'nonsense' formula such that no smaller one exists in the set) is certainly not forced by either 1 or 2, and can therefore be removed from the set without effecting the set's satisfying 1 and 2. Hence, since WFF is the smallest set satisfying 1 and 2, it cannot contain such a smallest formula that is not atomic or of the form $(A \circ B)$.

$\endgroup$
  • $\begingroup$ Yes, I noticed the term "smallest" and I interpreted it as you say. However, and maybe I'm just misinterpreting, but how can we be assured that in condition 2., the $A$ and $B$ cannot be strings that are not of the form $(\neg A)$ or $(A \circ B)$? $\endgroup$ – yroc Dec 17 '17 at 1:51
  • $\begingroup$ @yroc Oh! Now I see what you mean! OK, let me think ... $\endgroup$ – Bram28 Dec 17 '17 at 2:00
  • $\begingroup$ @yroc Hmm, one thing I immediate note is that the proof as stated does go through: $p\lor$ is not atomic, and can't possibly be formed through recursive step 2, since it does not star with a $($. Thus, at least that particular proof need not rely on the claim that * all* statements are of a certain form ... but of course we still all believe that that is true ... and presumably there is a proof for that! So what is that proof? ... more thinking ... $\endgroup$ – Bram28 Dec 17 '17 at 2:04
  • $\begingroup$ @yroc OK, I got it ... out of all the 'nonsense' formulas, there must be one or more 'smallest' ones, and those can certainly be removed without any repercussions as to whether the set satisfies 1 or 2. $\endgroup$ – Bram28 Dec 17 '17 at 2:15
  • 3
    $\begingroup$ @DougSpoonwood Good point! Yes, it needs to be spelled out that in this context, 'smaller' needs to be defined in terms of subsets, rather than cardinality, or else someone could indeed easily get confused. Thanks! $\endgroup$ – Bram28 Dec 18 '17 at 11:31
3
$\begingroup$

The definition of $\textbf{WFF}$ given is just one example of many that are stated in terms of "the smallest set" that satisfies some property, but they are better understood as giving a recursive construction for the desired set. More precisely, the construction is given by stages. In stage $1$ we are given a set of atomic formulas. In stage $n$ we construct those formulas produced using all previous stages using the given operations. The final set $\textbf{WFF}$ is the disjoint union of the sets of all the stages.

For example, $\;p\;$ is given in stage $1$, $\;(\neg p)\;$ is produced in stage $2$, $\;(q\to(\neg p))\;$ is produced in stage $3$, and so on. This constructive building up approach is in contrast to a cutting down approach where we have to assume that there exists a smallest set with a certain property.

$\endgroup$
  • $\begingroup$ I find the idea of stages nice, because it partitions WFF into classes of different syntactic complexity. One might use the stage of a formula to evaluate that formula's syntactic complexity. Such an evaluation might get contrasted with evaluating the complexity of a formula purely by it's length (number of symbols). $\endgroup$ – Doug Spoonwood Dec 18 '17 at 17:43
  • $\begingroup$ @DougSpoonwood: Yes, I think it is a great idea. Also, even though I did not explicitly mention it, the formulas can be considered as abstract objects with no need for syntactic form as a string of symbols. Its abstract form is primary, and any syntactic expression is secondary only for practical purposes. $\endgroup$ – Somos Dec 18 '17 at 20:25
0
$\begingroup$

Using the constructive approach as suggested by Somos, we can take a step back and make an algorithm for any member of WFF.

We can start with a counter C equal to 0.

If the current symbol is a propositional variable, then we decrease C by 1.

If the current symbol is $\lnot$, then we rewrite the counter.

If the current symbol is '(', then we increase the counter by 1.

If the current symbol is ')', then we decrease the counter by 1.

Finally, if the current symbol is a member of ∘, then we increase the counter by 1.

For ($\lnot$A), the sequence of the values of the counter is

[0, 1, 1, 0, -1].
    (  ¬  A   )

For any propositional variable, the sequence of the values of the counter is

[0, -1].
     A

For (A∘B), the sequence of the values of the counter is

[0, 1, 0, 1, 0, -1].
    (  A  ∘  B   )

Any member of WFF which satisfies that algorithm will have one propositional variable, the value of C will start as 0, end with -1, and only have -1 as it's final value.

Now the above algorithm is adequate to determine what is and what is not a member of **WFF*. The following lemma builds towards a proof of adequacy.

Lemma: Each formula F produced from the constructive process will have C start as 0, end with -1, and F will have at least one propositional variable.

Proof: That any formula at stage 1 has C start as 0 and end with -1 is indicated above. That any such F has at least one propositional variable follows from the nature of the constructive process.

Induction step: Now, we'll assume that all stage n formulas satisfy this lemma. For a stage (n + 1) formula, we either have a formula A of stage n which is inside of ($\lnot$A) or two formulas A and B of stage n inside of (A∘B). If the former, then the sequence of the values of the counter is [1, 1, {...}, one less than the final value {...}], where {...} is the sequence of the values of the counter for A. But, the sequence of values of C in {...} took in a number and produced one less than that number by the inductive assumption. Thus, it follows that the sequence of the values of the counter once the algorithm has gone through all value changes that happen in {...} is (1, 1, 0, -1). For a formula of the type (A∘B) the sequence of the values of the counter is [1, {...}, one more than the value of C at the end of {...}, !...!, one less than the value of C at the end of !...!]. But again, the values of {...} start with some number and produce a number one less than that number, and !...! effects the same decrease in value. Thus, the sequence of values when each of {...} and !...! terminate is [1, 0, 1, 0, -1]. So, assuming that this theorem holds for stage n, it will hold at the stage (n+1). Therefore, each formula produced from the constructive process will have C start as 0 and end with -1 and have at least one propositional variable.

That -1 only appears at the end of the algorithm also gets guaranteed by the base case, and an inductive step where sequences of values for {...} and !...! refer back to the base case.

So, let's say that we suppose that some $\alpha$ has a form different from ($\lnot$A) or (A∘B). We then apply the above algorithm to that $\alpha$. But, if we built up the formula in stages from this definition as we have supposed, then the sequence of values of C for $\alpha$ will either have -1 as some value of C before it's last value, or C will be something other than -1 as it's last value. But, by the algorithm, that shows that $\alpha$ is not a member of WFF.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.