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}\hfill \forall x\exists y\hfill \\ \hfill \forall a\exists b\hfill \end{array}\varphi (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\varphi (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}\hfill \forall x\exists y\hfill \\ \hfill \forall a\exists b\hfill \end{array}[(x=a\leftrightarrow y=b)\wedge \varphi (x)\to \psi (y)]\leftrightarrow Rxy\varphi (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 $\varphi (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 $\mathrm{\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\varphi (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