Definition nested and unnested first order formulas

Question

What's the definition of nested and unnested formulas in a first order language? I came across the term in a model theory book i'm reading, and I can't seem to find it defined there, or in my brief internet searches. Thanks!

Answer 1

Not a very useful definition, but can be done. For example, in the following two ways.

Def 1. First-order expressions φ are ψ are nested iff either one is in the scope of the other.

Is in the scope of can be defined by induction on the structure of the expressions. Mauro pointed out the interesting case: if φ is of the form $\forall x_1...x_k~\psi$, then ψ is said to be in the scope of φ. When ψ too starts with a quantifier, we speak of the two quantifiers being nested. Alternatively, you can make use of the parse trees associated with the expressions. The definition is straightforward:

Def 2. First-order expressions φ and ψ are nested iff either the parse tree associated with φ is a branch of the parse tree associated with ψ, or the other way around.

Answer 2

Thanks for the answers everyone. I think i've found the answer: Let $L$ be a signature. An unnested atomic formula is an atomic formula of one of the following forms: \begin{align} x=y\\ c=y\\ F(\overline(x))=y\\ R\overline{x} \end{align} where $c,F,R$ are respectively some constant, function, and relation symbols of $L$. (Wilfrid Hodges' "A Shorter Model Theory", section 2.6, page 51)Apparently, using unnested atomic formulas is useful for building up induction on the complexity of formulas - one place I'm finding this is the induction building up to a proof of Los's ultraproduct theorem.(section 8.5)