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
∀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.