# Quantifiers in a first-order-logic syntax tree

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:

### ∀x(S(x)→(¬T(x)))

(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

        ∀x
|
→
/   \
S    ¬
|    |
x    T
|
x


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.

• 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. – Mauro ALLEGRANZA Sep 1 '16 at 14:04

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