Arithmetic games

A sentence of a formal theory of the first order arithmetic is a game.
The language must include the symbols of the first order logic and at
least the basic symbols of arithmetic: relation symbols for equality
and order, function symbols for addition and multiplication, and some
constants like zero and one.
The game is played between two players. Initially one of the players is
Proponent and the other is Opponent but they may change roles as the
rules specify. When the game is played the sentence is reduced until
it is either True or False. In addition to the symbols of the language
of the initial sentence a reduced sentence may contain any natural
number.
At each step the action depends on the main operator (i.e., the one with
lowest precedence) of the current sentence:
If the main operator is universal quantifier the Opponent chooses a
value for the variable. The game continues with the quantified formula.
If the main operator is existential quantifier the Proponent chooses a
value for the variable. The game continues with the quantified formula.
If the main operator is equivalence the Proponent chooses "true" or
"false". If "true" is chosen the game continues with the conjunction
of the same operands, otherwise the game continues with the conjunction
of the neagtions of the operands.
If the main operator is implication the Proponent chooses one of the
operands. If the propnent chooses the left operand the game continues
with the negation of the chosen formula, otherwise the game continues
with the chosen formula.
If the main operator is conjunction the Opponent chooses one of the
operands. The game contiues with the chosen formula.
If the main operator is disjunction the Proponent chooses one of the
operands. The game continues with the chosen formula.
If the main operator is negation the roles of the layers are swapped:
the Proponent becomes the Opponent and the former Opponent becomes the
Proponent.
If the main operand is a relation its both sides are evaluated. If there
are variables in the expressions the values chosen by players are used.
The values are compared, so the corrent formula is reduced either to
"true" or to "false".
If the current formula is "true" the current Proponent has won.
If the current formula is "false" the corrent Opponent has won.
If the sentence is provable there is a strategy for the Proponent
to win the game. If the negation of the sentence is provable there
is a strategy for the Opponent to win the game. If the sentence
is undecidable there is no expressible strategy for either player
to win the game.
Gödel's sentence is an example where there is no expressible
strategy for either player.
--
Mikko