Which of the following expressions are formulas of predicate logic?
(i) $\forall X \, \forall Y \ (X \subseteq Y \leftrightarrow (\forall x \ x \in X \to x \in Y))$
(ii) $\forall P \ P(0) \land \forall n \ (P(n) \to P(n+1) ) \to (\forall n \, P(n))$
(iii) $\forall t\, G(P(t) \, U \, P(t))$, where $P$ is a predicate symbol.
Currently doing some past papers and I wanted to confirm this...
For a formula to be of a predicate logic it must follow the well-formed rules.
Only (iii) is a formula of predicate logic because it follows the well-formed rules. (i) and (ii) use predicates instead of variables after the quantifiers therefore not well-formed and not a formula of predicate logic. Is there any other reasons why they may not be of predicate logic?
I don't know what your underlying language is, but if your set of variables includes $X,Y,x$ and your signature is just consisting of $\in$, taking $\subseteq$ as exactly the abbreviation as the right hand side, then (i) is a well-formed formula in the language of set theory. You may even add $\subseteq$ as a binary relation symbol to make it well-formed in some other signature of your taste.
(ii) seems to suggest that $P$ is a unary predicate which is quantified at the beginning, thus this formula seems not be well-formed in first-order logic.
If you assume for (iii) that $t$ is a variable symbol, and $G,U$ are unary/binary predicate symbols respectively and $P$ is a unary predicate, then this formula does not really make sense, as we have a predicate applied to another predicate.
I think there is needed information missing to really answer the questions for which you should search yourself(in the book where this question is from). The question
is always to be read with some appropriate context.
Now, what is the set of well-formed formulas, $FO(\sigma)$? This set is generated in the following way from the before mentioned sets:
First, we form the set of terms of this signature $\sigma$.
Then $FO(\sigma)$ is formed using this set of terms and $\sigma$ again:
We remark a few things on the process of forming the set of well-formed first-order logic formulas over a signature $\sigma$ and a set of variable $Var$ I just sketched:
So for you to analyse if a formula is well-formed, your first question has to be over what signature and over what set of variables. Then you may assert membership in $FO(\sigma)$.
As I said before, this is just a sketch. First, what I was describing was first-order logic without equality, but the differences are marginal(on the syntactical level).
We all use shorthand notations and deviate from this formal specification. Thus e.g. even when some author formally defined $Var=\{x_1,x_2,\dots\}$, you're likely to see $\forall x\phi$ as a formula. This is meant to be a shorthand but it is not technically fine, but such a minor detail that normally no one gets hurt. A good mantra is that you are allowed to deviate if you can always rephrase it properly.
Another common shorthand also used in your example is that binary predicates are often denoted in infix notation, that is, instead of writing $>(x,y)$ you write $x>y$.
There are however situations where the concrete syntactical structure matters, that is why this is set on such a firm ground.
I want to end with, that working with these objects is a purely syntactical matter. There is no meaning attached to these strings(yet) and that is how they ought to be treated. Two strings differ if they differ in one symbol already. It is not about representing (semantically) the same.
EDIT: I tried to not give you an answer but to explain to you the context of how to find an answer yourself(which some of my perspective on the top). I could not have given a precise answer as you we're asking about a syntactic technicality for which I don't know the complete surrounding to, i.e. the signature, etc. This answer turned out longer than expected and thus if something is unclear, we should clarify this together in the comments.