I was told that syntax trees of F-O-L formulas are built the same way as propositional ones. Everything seems pretty intuitive to me, but I'm not too sure about quantifiers.

Let's say we want to build a syntax tree based on the following formula:


(where S,T are predicates, x is a variable)

In this case, ∀x bounds to the whole "inner" formula S(x)→(¬T(x)), so it should be

       /   \
      S    ¬ 
      |    |
      x    T

Is that correct? I understand that from a graph perspective, quantifiers-with-a-variable are unary, meaning that they can only have one child. Am I correct in thinking that this child can either be a

(i) logical connective

(ii) predicate symbol

(iii) another quantifier-with-a-variable

But it cannot be a term (constant, single variable, functional symbol)?

Here are some visualizations for cases (ii) and (iii) to clarify what I mean:

(iii) formula: ∃x∀y(S(x)∧T(y))                     (ii) formula: ∃x(S(x))

        ∃x                                               ∃x
         |                                                |
        ∀y                                                S
         |                                                |  
         ∧                                                x
       /   \
      S     T 
      |     |
      x     y

These trees should be valid based on my assumption.

Thank you in advance.

  • 2
    $\begingroup$ Your assumption is correct; you do not "unpack" $\forall x$ into symbol+variable. Thus, a quantifier must be followed by another quantifier (and so on) or a quant-free formula. In this case we may have either an atomic formula : i.e. a predicate or an equality (if FOL+equality), or a "complex" one, that means a connective. $\endgroup$ – Mauro ALLEGRANZA Sep 1 '16 at 14:04

Correct. Quantifiers are placed in front of formulas, where a formula is one of the following:

  1. An atomic formula $P(t_1, ... t_n)$ with $P$ a predicate and $t_1, ... t_n$ terms.

  2. Some truth-functional operator applied to other formulas

  3. A quantifier applied to some other formula.

So: you indeed never quantify a term and in the syntactical tree a quantifier has indeed exactly one child.


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.