I'm struggling to understand a remark in Daniel Leivant's Higher Order Logic (link), namely that in section 3.3 on page 16:

It is mentioned that any second-order formula can be brought into prenex normal form, which is indeed easy to see. However, then he says:

A second order prenex formula $\psi$ can be further transformed (without increasing the number of quantifiers in any kind) into an equivalent formula $\psi^*$ in which no second order quantifier falls in the scope of a first order quantifier.

He then describes a procedure on how to recursively move out second-order quantifiers, where the key part is:

replace $\forall x\exists f\; \phi[x,f]$ by $\exists g\forall x\; \phi[x,g_x]$ where $g_x(z) := g(x,z)$, ...

and similarly for quantifiers over relation variables. The formulas in above sentence are equivalent by a weak form of the Axiom of Choice

Now, I'm working in monadic second-order logic, so I only need to (and can) quantify over sets. I'm guessing the replacement would then look like: $$\forall x\exists A\; \phi[x,A]\text{ by }\exists B\forall x\;\phi[x,B_x],$$ but I do not see how I could formally make this $B_x$, since it looks like we need to define $B_x := B(x)$ (which would mean $B$ is no longer a set, but rather a function), or at least we need to define a pairing function $\langle\cdot,\cdot\rangle$ such that $y\in B_x\rightleftarrows \langle x,y\rangle\in B$, and in the domain I'm working in (finite words over $\{0,1\}$, with immediate successor functions and lexicographic ordering defined) this doesn't seem to be possible.

So now I'm wondering: does this method work in monadic second-order logic, i.e. how could we define $B$ or $B_x$, or is there another way to see we can indeed swap first-order quantifiers and monadic second-order quantifiers using some form of the axiom of choice?

  • $\begingroup$ A "set" in logic is a (monadic) predicate: $x \in A$ iff $A(x)$. Thus, the transformation of the monadic predicate $A$ needs a binary predicate $B$ such that: $B_x(z) \equiv B(x,z)$. $\endgroup$ – Mauro ALLEGRANZA Jun 1 '17 at 10:07
  • $\begingroup$ So, this procedure cannot be applied to monadic second-order logic if I understand correctly? $\endgroup$ – konewka Jun 1 '17 at 10:08
  • $\begingroup$ @konewka: just as you said, it will depend on your signature and background theory you're working in. If you are working with monadic theories of arithmetic, or other theories with pairing functions for first-order objects, you are fine. The key point is that if you know $\forall x \exists A P(x,A)$ then you choose a sequence $(A_x)$ of witnesses, and you change the formula to $\exists B \forall x P'(x,B)$ where $P'$ changes $P$ by replacing instances of $t \in A$ with $\pi(x,t) \in B$ where $\pi$ is the pairing function. Then the new formula is satisfied with $B = \{ \pi(x,y) : y \in A_x\}$. $\endgroup$ – Carl Mummert Jun 1 '17 at 12:03

Your Answer

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

Browse other questions tagged or ask your own question.