Consider the well-formed formula in set theory (∀x) ((∀y) ((x ∈ y) ∨ (y ∈ x ))). I believe there are 5 subformulas:

  1. (x ∈ y)
  2. (y ∈ x)
  3. ((x ∈ y)∨(y ∈ x))
  4. (∀y) ((x ∈ y)∨(y ∈ x))
  5. (∀x) ((∀y) ((x ∈ y)∨(y ∈ x)))

However I am not sure if there are more, e.g. potentially things like

  • (∀y) ((∀x) ((x ∈ y)∨(y ∈ x)))
  • (∀x) ((x ∈ y)∨(y ∈ x))
  • etc.

I noticed Wikipedia does not have a 'subformula' article, so my only reference is William Weiss's excellent online book on Set Theory (see in particular page 12 for his discussion of "subformulas").

Edit: The 2 additional possibilities looked plausible to me because

  • (∀y) ((∀x) ((x ∈ y)∨(y ∈ x)))

is logically equivalent to our formula (∀x) ((∀y) ((x ∈ y)∨(y ∈ x))). Does this imply that it, as well as its subformula

  • (∀x) ((x ∈ y)∨(y ∈ x))

Should be included in our list?

  • Could you edit the question to make it clear what you're actually trying to ask? Do you just want a list of all the WFFs in (∀x) ((∀y) ((x ∈ y) ∨ (y ∈ x )))? – DTR Sep 26 '15 at 2:56

You can use a parse tree for this. First you draw the parse tree, then you draw boxes around subtrees.

Parse tree           Parse tree with boxes

And you see that you were correct.

Note for example that ∀y ∀x (x ∈ y ∨ y ∈ x) is equivalent to a subformula (namely the whole formula), but not a subformula itself, because it doesn't exist in the parse tree. You need to modify the structure to get to that form.

On request, here's a complete LaTeX example to generate the picture on the right:




\begin{tikzpicture}[every node/.style={draw,circle}]
    \node (ax) {$\forall x$}
        child{ node (ay) {$\forall y$} 
            child { node (or) {$\lor$} 
                child { node (xy) {$x\in y$} }
                child { node (yx) {$y\in x$} }
    \draw[red] ($(xy.south west)-(0.3,0.3)$) rectangle ($(xy.north east) + (0.3,0.3)$);
    \draw[red] ($(yx.south west)-(0.3,0.3)$) rectangle ($(yx.north east) + (0.3,0.3)$);
    \draw[red] ($(xy.south west)-(0.4,0.4)$) rectangle ($(yx.north east |- or.north east) + (0.4,0.3)$);
    \draw[red] ($(xy.south west)-(0.5,0.5)$) rectangle ($(yx.north east |- ay.north east) + (0.5,0.3)$);
    \draw[red] ($(xy.south west)-(0.6,0.6)$) rectangle ($(yx.north east |- ax.north east) + (0.6,0.3)$);

  • Hi Keelan, thanks very much for illustrating these subformulas in a tree diagram. I agree - it is very helpful to understanding and identifying the subformulas. Quick follow up (see edit in question): does it matter that (∀y) ((∀x) ((x ∈ y)∨(y ∈ x))) is logically equivalent to (∀x) ((∀y) ((x ∈ y)∨(y ∈ x)))? – Mathemanic Sep 26 '15 at 20:55
  • @EthanAlvaree see the final paragraph of my answer. Equivalence is something different than subformulas. For example, (P or not P) is equivalent to True, but neither is a subformula of the other. Or a more non-trivial example: (P implies Q) vs. (not P or Q). – user2953 Sep 26 '15 at 21:01
  • Slightly off-topic but I love your figures. Do you have a Tikz code for generating your parse tree with boxes? – Mathemanic Sep 28 '15 at 6:43
  • @EthanAlvaree you were lucky, I hadn't turned off my laptop so it was still in /tmp. See the edit ;-) – user2953 Sep 28 '15 at 7:31

In general, the subformulas of Φ are those formulas used in the construction of Φ. You can see the construction of Φ as a tree, and every formula in that tree is a subformula of the resulting tree trunk (maybe this is more intuitive than the recursive formal definition you see in the book).

An informal way to construct your formula and to show is well formed, using the collection of formulas of set theory defined in Weiss's Book:

  1. (x ∈ y) is a wff by Rule 1
  2. (y ∈ x ) is a wff by Rule 1
  3. (x ∈ y) ∨ (y ∈ x ) is a wff by Rule 4
  4. (∀y) ((x ∈ y) ∨ (y ∈ x )) is a wff by Rule 7
  5. (∀x) ((∀y) ((x ∈ y) ∨ (y ∈ x ))) is a wff by Rule 7

And there you have the subformulas.

Is true that (∀x) ((x ∈ y) ∨ (y ∈ x )) is a wff, you can see this with the rule 7:

  1. If Φ is a formula and vi is a variable, then (∀vi)Φ is also a formula.

So, if ((x ∈ y) ∨ (y ∈ x )) is a formula, and x is a variable then (∀x) ((x ∈ y) ∨ (y ∈ x )) is also a formula.

However, (∀x) ((x ∈ y) ∨ (y ∈ x )) is not a subformula of your original formula, because is not used in the construction of it. The same goes for the other case you mentioned.

  • Thank you JosEduSol! So it doesn't matter that (∀y) ((∀x) ((x ∈ y)∨(y ∈ x))) is logically equivalent to (∀x) ((∀y) ((x ∈ y)∨(y ∈ x)))? – Mathemanic Sep 26 '15 at 20:54
  • @EthanAlvaree As Keelan explained in his answer, it doesn't matter in this case. You are just working with formulas and subformulas. Think in syntactic construction terms. – JosEduSol Sep 26 '15 at 20:59

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.