I am studying decidability of theories and fragments in first-order logic (see, for instance, Some decidable theories in https://en.wikipedia.org/wiki/Decidability_(logic) or the thesis: https://hal.inria.fr/tel-02406821/document). Particularly, I am interested in seeing whether first-order theories are decidable on its $\exists^*\forall^*$ fragment.
While researching, I discovered the Guarded Fragment, $\textit{GF}$, so I am trying to see whether any formula within $\textit{GF}$ can be reduced to a formula in the $\exists^*\forall^*$ class: i.e., from a formula $\phi$ in $\textit{GF}$ to a formula $\exists^*\forall^* \textit{. } \varphi$, whatever $\varphi$ is.
First, I am trying to understand what the $\textit{GF}$ means. I understand from (http://ceur-ws.org/Vol-106/06-kazakov.pdf) that it must be a formula in $\forall \overline{x} \textit{. } [G \implies F]$ form or in $\exists \overline{x} \textit{. } [G \wedge F]$ form, but I do not properly get what $G$ and $F$ are. Can someone clarify? I mean, it is said that they are atoms, but where are then variables $\overline{x}$ and $\overline{y}$ instantiated/used?
In (it is a download page https://ir.cwi.nl/pub/2120/2120D.pdf), for instance, they exemplify some cases (search Example 1). Can someone explain why $\forall x \textit{. }(a(x,y) \implies b(x,y))$ and $\exists x \textit{. } (a(x,y) \wedge b(x,y))$ are guarded, whereas $\forall x \textit{. } (a(x) \implies b(x, y))$ and $\exists x \textit{. } (a(x) \wedge b(x, y))$ are not? Consider, also, this more complicated exmaple: $\forall x \textit{. } (a(x, y) \implies \forall z \textit{. } (b(y, z) \implies c(y, z) \wedge d(y, z))) $
Also, for any of the examples, I would like to know whether it is inside the $\exists^*\forall^*$ class. Thus, I thought that a good way to do this is to transform the formula to prenex normal form, where all the quantifiers are located at the beginning. Is this a correct way of checking this? In case it is, can someone explain how to do it? I read (Transform a formula into prenex normal form) but I do not understand it completely.
I guess this can be done, since I read in (https://en.wikipedia.org/wiki/Prenex_normal_form) that every formula in classical logic is equivalent to a formula in prenex normal form.
I know they are several questions, but I would be happy with clarifying any of them. The aim of this post is none other than to respond to the following: if a formula is in the guarded fragment, does it mean it has an equivalent in the $\exists^*\forall^*$ class?
PS: I have seen guarded fragment is NEXPTIME decidable, while Ramsey-Schofinkel-Bradley (i.e., $\exists^*\forall^*$ with no function symbols) is 2EXPTIME. So they seem similar...
A mere part of an answer but here's a start. I looked at the 2120D.pdf paper briefly to try to understand your questions about what is guarded and what is not. He defines it pretty rigorously in Section 2, Definition 1. Your questions are addressed in clause 5 of the definition.
So $\forall x \textit{. }(a(x,y) \implies b(x,y))$ and $\exists x \textit{. } (a(x,y) \wedge b(x,y))$ are both guarded, because the guard clause $a(x,y)$ contains all the arguments $x,y$ of the consequent. Whereas $\forall x \textit{. } (a(x) \implies b(x, y))$ and $\exists x \textit{. } (a(x) \wedge b(x, y))$ are not because the guard clause only contains $x$ while the consequent clauses contain $x$ and $y$.