Understanding quantifiers through gaming metaphors

Question

In the appendix about mathematical logic of his book "Analysis 1", Terence Tao explains quantifiers via gaming metaphors. For example he writes

In the first game, the opponent gets to pick what x is, and then you have to prove P(x); if you can always win this game, then you have proven that P(x) is true for all x.

Isn't he confusing "truth" with "provability" here? Because being able to always win this game means that for each x, there is an individual proof of the fact that P(x). But proving “for all x, we have P(x)” is something different than proving “for each x, there is a proof of P(x)”. (To speak about provability of statements, one normally gives an exact definition of what “(first-order) terms”, “well-formed (first-order) formulas” are and then specifies a formal calculus consisting of inference rules and logical axioms, in order to then define what it means for a formula to “be deducible from a set of axioms”. But even if one has done this, one shouldn’t confuse “deducible formulas” with “true formulas”.)

The other gaming metaphors are:

In the second game, you get to choose what x is, and then you prove P(x); if you can win this game, you have proven that P(x) is true for some x.

and

To continue the gaming metaphor, suppose you play a game where your opponent first picks a positive number x, and then you pick a positive number y. You win the game if y 2 = x. If you can always win the game regardless of what your opponent does, then you have proven that for every positive x, there exists a positive y such that y 2 = x.

He gives us the exercise to think of such gaming metaphors for other statements, for example:

There exists a positive number x such that for every positive number y, we have y^2 = x.

What would be the corresponding gaming metaphor? I would say it’s something like this: I choose a positive number x. Then, my opponent gives me a positive y. I win iff y^2 = x. The statement is true iff there is a fixed positive number x with which I can always win. Is that correct? I somehow don’t really understand the purpose of these gaming metaphors. What is it? In this example, thinking about what the corresponding gaming metaphor could be, doesn’t help me understand the statement more.

Answer 1

As already mentioned, Terence was being informal. But the distinction you are trying to make is important. $ \def\nn{\mathbb{N}} \def\pa{\text{PA}} \def\prf{\text{Proof}} \def\box{\square} $

I shall talk from the perspective of the meta-system. Take any formal system $S$ that has decidable proof validity. For each $n \in \nn$ and formula $φ$ over PA, let $\prf_S(n,φ)$ be a $Σ_0$-sentence over PA, such that $PA \vdash \prf_S(n,φ)$ iff $n$ codes a proof of $φ$ over $S$, and $PA \vdash \neg \prf_S(n,φ)$ otherwise. Then (since PA is consistent) for each natural number $n$ we have $\pa \vdash \neg \prf_\pa(n,\bot)$, however $\pa \nvdash \forall x\ ( \neg \prf_\pa(x,\bot) )$.

This is hence a counter-example to Terence's claim as stated. To make his claim more correct, we must change the wording to something like:

If you can prove that given any $x$ you can prove $P(x)$, then you have proven that $\forall x\ ( P(x) )$.

Or we can change his phrasing to "if you can show that you can always win this game, ...".

Even with this change, in practice you cannot fulfill the condition in the sense required by modern mathematics. What does it even mean to be given say an infinite subset of $\nn$? And how on earth can we prove that such a set satisfies $P$? One way of interpreting the condition so that this works is

You can give a systematic procedure for constructing the proof of $P(x)$ over $S$ (plus whatever other sentences hold in the current context).

This usually amounts to writing down the proof itself... This of course can be considered just a way of expressing the inference rule that if $S \vdash P(x)$ then $S \vdash \forall x\ ( P(x) )$, where the game semantics explain the meaning of free-ness of $x$ in "$S \vdash P(x)$".

Anyway, you probably do not need to know game semantics, since you seem to know logic already, but see my comments at this post for how game semantics can better clarify the role of LEM (law of excluded middle) in classical logic. The BHK interpretation ties in nicely with game semantics, where the program corresponding to a proof can be seen as implementing a winning strategy for the game.

Answer 2

You are technically right, and the author is being somewhat informal with his choice of words. More precise would be, "Your opponent gets to choose $x$, and if $P(x)$ holds you win." This, of course, is much less evocative of two people playing a game, which is why I think he chose to use the more active phrasing. In fact, indeed, if we are being very formal, the game described is perhaps closer to a game for provability than for truth.

The gaming metaphor you picked for the statement is correct.

In this context (of an introductory analysis book), I assume the game-theoretic description of the interpretation of quantifiers is mostly to make them easily understandable for people who have never seen them before. These games are actually a very natural way to think about quantifiers. For instance, I bet you have heard an $\epsilon$-$\delta$ proof explained by something like

For every $\epsilon > 0$ you choose, no matter how small, I can always find a $\delta > 0$ such that ....