# game-theoretical quantifier

A Henkin or branching quantifier is a multi-variable quantifier in which the selection of variables depends only on some, but not all, of the other quantified variables. For instance the simplest Henkin quantifier can be written:

 $\begin{array}[]{c}\forall x\exists y\\ \forall a\exists b\end{array}\phi(x,y,a,b)$

This quantifier, inexpressible in ordinary first order logic, can best be understood by its skolemization. The formula above is equivalent to $\forall x\forall a\phi(x,f(y),a,g(a))$. Critically, the selection of $y$ depends only on $x$ while the selection of $b$ depends only on $a$. For instance, given a value for $a$, a value of $b$ must be chosen which is compatible with every possible value of $x$, while given any $x$, the value of $y$ chosen must be compatible with every value of $a$.

Logics with this quantifier are stronger than first order logic, lying between first and second order logic in strength. For instance the Henkin quantifier can be used to define the Rescher quantifier, and by extension Härtig’s quantifer:

 $\begin{array}[]{c}\forall x\exists y\\ \forall a\exists b\end{array}[(x=a\leftrightarrow y=b)\wedge\phi(x)\rightarrow% \psi(y)]\leftrightarrow Rxy\phi(x)\psi(y)$

To see that this is true, observe that this essentially requires that the Skolem functions $f(x)=y$ and $g(a)=b$ the same, and moreover that they are injective. Then for each $x$ satisfying $\phi(x)$, there is a different $f(x)$ satisfying $\psi((f(x))$.

This concept can be generalized to the game-theoretical quantifiers. This concept comes from interpreting a formula as a game between a “Prover” and “Refuter.” A theorem is provable whenever the Prover has a winning strategy; at each $\wedge$ the Refuter chooses which side they will play (so the Prover must be prepared to win on either) while each $\vee$ is a choice for the Prover. At a $\neg$, the players switch roles. Then $\forall$ represents a choice for the Refuter and $\exists$ for the Prover.

Classical first order logic, then, adds the requirement that the games have perfect information. The game-theoretical quantifers remove this requirement, so for instance the Henkin quantifier, which would be written $\forall x\exists y\forall a\exists_{/\forall x}b\phi(x,y,a,b)$ states that when the Prover makes a choice for $b$, it is made without knowledge of what was chosen at $x$.

 Title game-theoretical quantifier Canonical name GametheoreticalQuantifier Date of creation 2013-03-22 12:59:19 Last modified on 2013-03-22 12:59:19 Owner Henry (455) Last modified by Henry (455) Numerical id 7 Author Henry (455) Entry type Definition Classification msc 03B15 Related topic Quantifier Defines Henkin quantifier Defines Henkin Defines branching quantifier Defines branching Defines game-theoretic quantifier