0
$\begingroup$

I have some basic confusions about the definition of the guarded fragment of first-order logic. Hopefully someone can tell me where I'm wrong.

GF in FO is defined by:

  1. Atomic formulas, $x=y$ and $R(x_1,...,x_n)$, are guarded formulas.
  2. If $\phi,\psi$ are guarded formulas, so are $\neg \phi$ and $\phi \wedge \psi$.
  3. For variables $\{x_j,...,x_m\} \subseteq \{x_i,...,x_n\}$ and guarded fomula $\phi$ and atomic formula $A$, $\exists x_j\ A(x_i,...,x_n) \wedge \phi(x_j,...,x_m)$ is a guarded formula.

My reasoning is: for arbitrary FO formula of form $\exists x\ \phi$, I can just pick some relation $T$ that's always true and over all variables, and it's then equivalent to $\exists x \ T \wedge \phi$, a guarded formula. Other forms follow from this. So FO reduces to GF.

But that's obviously not true. I can't figure out where my mistake is. Could someone let me know where I got it wrong?

For example, isn't $$ \forall x\ \exists y\ \forall z\ \phi $$ equivalent to $$ \forall x\ (T \to \exists y\ (T \wedge \forall z\ (T \to \phi))) $$

$\endgroup$
2
$\begingroup$

You're correct that, if the structure you're working with has a universal relation, then using that relation as a guard is equivalent to having no guard at all. However, you don't get to pick the interpretation of the relation symbols. For example, if you're trying to write a formula that is satisfied by exactly the class of 3-colourable graphs, then you should think in terms of an adversary supplying you with an arbitrary graph and your formula has to give the right answer, without being able to rely on any particular properties of the structure you're given.

$\endgroup$
  • $\begingroup$ Ah! Thank you so much! I can’t believe I missed that! Thanks for the example. It really cleared things up for me $\endgroup$ – RexYuan Aug 21 at 15:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.