Predicate Logic Well Formed Formula: Is ((∀x P(x)) ∨ (∃y Q(f (y)))) well formed?

Question

Having difficulties understanding well formed formulas. I understand rules, but don't know how they apply to these. If they're not well formed formulas, how do I write it so that it'll be a well formed predicate formula. Please help.

1) ((∀x P(x)) ∨ (∃y Q(f (y)))) Is this a well formed formula? Is the f(y) well formed? From the rules, it looks like predicate constants are always capitalized. Does it make a difference?

2) ∀x ∃y (P(x) ∧ Q(y)) This looks like a well formed formula to me, right?

3) ∀x (P(x) → (¬∃y Q(y))) Does the ¬∃y cause any problems?

Answer 1

YES: 2) and 3) are well-formed.

About 1), we usually use $f$ to denote a function; in this case, YES: $∃y \ Q(f(y))$ is well-formed.

If $f$ instead is a predicate symbol, then NO: we cannot use a predicate as argument of another one.

Example of predicate symbol (binary): $<$; example of function symbol (binary): $+$.

We can write $(x<y)$ and also $(x<(y+z))$, but we cannot write: $(x<(y<z))$.

Answer 2

A formula is well-formed if it can be built up recursively. For example, for 1) we have:

Since $x$ is a variable, $x$ is a term

Since $y$ is a variable, $y$ is a term

Since $y$ is a term, and $f$ a function symbol, $f(y)$ is a term

Since $x$ is a term, and $P$ a predicate symbol, $P(x)$ is a (atomic) formula

Since $f(y)$ is a term, and $Q$ a predicate symbol, $Q(f(y))$ is a (atomic) formula

Since $P(x)$ is a formula, $x$ a variable, and $\forall$ a quantifier, $(\forall x \ P(x))$ is a formula

Since $Q(f(y))$ is a formula, $y$ a variable, and $\exists$ a quantifier, $(\exists y \ Q(f(y)))$ is a formula

Since $(\forall x \ P(x))$ and $(\exists y \ Q(f(y)))$ are formulas, $((\forall x \ P(x)) \lor (\exists y \ Q(f(y))))$ is a formula