Quantifiers in a first-order-logic syntax tree

Question

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.

Thank you in advance.

Answer 1

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.