[Prev][Next][Index][Thread]
games and classical logic
Date: Mon, 9 Dec 91 23:04:03 +0100
A GAME-THEORETIC SEMANTICS OF CLASSICAL LOGIC
---------------------------------------------
This is a simplification of a previous message about cut-elimination.
As could be expected, the treatment of cut-elimination
can be clarified and unified if we extend formulae to contain OR and AND nodes.
The result is a quite simple game-theoretic semantics of classical logic.
Comments are very wellcome.
FORMULAE:
a formula is a AND, OR tree of bounded depth, where the leaves are booleans
True or False.
We don't restrict trees to be finitely branching, hence we can represent
universal and existential quantifications (as infinite conjunction
and disjunction respectively).
We define the complement A* of a formula by
True* = False, False* = True
if A is /\ Ai, then A* is \/ Ai*
if A is \/ Ai, then A* is /\ Ai*.
We will write also A,B for A \/ B.
For instance, the sequent (x)P(x),(E x)P*(x) is thought of as
the infinite disjunction \/ P*(n) \/ [/\ P(n)].
PROVABLE FORMULAE:
This is an inductive definition:
.if A is /\ Ai, A is provable iff for all i, Ai is provable
.if A is \/ Ai, A is provable iff there exists i0 such that Ai0 is
True or Ai0 = /\ Ai0j, and for all j, Ai0j \/ A is provable.
REMARK: a standard inductive argument shows that if A* and A,B
are provable, then B is provable. We are going to refine this result
(which fails to produce satisfactory computations in general, cf. the 0/1
example of the previous message).
GAMES, PLAYERS and INTERACTION SEQUENCES:
The definition of provable suggests the following game between player I
and player II for a configuration A:
.if A is /\ Ai, player II chooses an i, and the configuration becomes Ai
and the game goes on,
.if A is \/ Ai, player I choses i0 such that Ai0 is True (and wins
the game), or such that Ai0 is /\ Ai0j, and player II chooses a j
and the configuration becomes A \/ Ai0j, and the game goes on.
A sequence of such actions, infinite or terminating with a win of
a given player I P, is called a PLAY of P.
Given a player I P for A, and a player I Q for A*, one can form the
INTERACTION SEQUENCE of P and Q by letting P play against Q. A given
interaction sequence between P and Q can be seen as a tree of
plays for P (and dually, as a tree of plays for Q).
STRATEGIES, PROOFS and EVIDENCE:
A SIMPLE STRATEGY for A tells a player I how to play against any
player II for A.
A STRATEGY for A tells a player I how to interact against any player
I for A*. A PARTIAL STRATEGY is a strategy that may fail to indicate
moves.
It is clear that any strategy can be restricted to a simple strategy, and
any simple strategy extends canonically to a strategy. In general,
a strategy differs from the extension of its associated simple
strategy (see below for an example). Also, a strategy can be considered
as a player.
A simple strategy is a PROOF of A if it wins against any player II.
This definition agrees with the inductive definition of provable.
A strategy S is an EVIDENCE of A iff for any player Q of A*, the interaction
sequence of S and Q, seen as a tree of plays for S, is well-founded,
where terminal leaves are either success for S, or S waiting
for an answer of Q.
REMARK: if S is an evidence for A, the simple strategy S that S defines
by restriction is a proof of A.
A PARTIAL EVIDENCE for A is a partial strategy S for A such that, for any
player Q for A*, the interaction sequence of S and Q either stops
because S fails to indicate a move, or
seen as a tree of plays for S, is well-founded,
where terminal leaves are either success for S, or S waiting
for an answer of Q.
REMARK: if S is a strategy for A \/ B, S can be seen as a partial strategy
for A (and for B). If S is an evidence for A \/ B, then S is a partial
evidence for A (and for B).
PROPOSITION: let A be a formula, if S is a partial evidence for A and T
-----------
is a partial evidence for A*, the interaction sequence of S and T is finite.
PROOF: by induction on the depth of A. If the proposition holds for
-----
depth(A) = n, then it holds for depth(A) = n+1, because each moves of
depth n+1 can be seen as a backtrack point. Hence the interaction sequence
can be decomposed as an interaction sequence of depth n, plus a finite
number of backtracking in a formula.
CUT-ELIMINATION:
The advantage of evidences against proofs is that they have a good behaviour
w.r.t. cut-elimination. Given a strategy S for A*, and a strategy T for
A \/ B, we can define the strategy CUT(S,T) for B by describing its behaviour
against any player R for B*. The combination of S and R forms a player
for A* /\ B*, and we let this combination play against T, hidding all
the moves that are in A or A*.
In general, we will get only a partial strategy. It may be that there
is an "infinite internal chatter" between S and T,
without eventual moves in B.
HOWEVER, if S is an evidence for A*, and T an evidence for A \/ B, then
CUT(S,T) is an evidence for B.
For this, we have only to show that each internal communication in A
is finite. This follows from the proposition, because T can be
seen as a partial evidence for A, and S is an evidence for A*.
EXAMPLE:
we take the 0/1 example of the previous message. We have three
cut-free proofs
Q0 proves (E a,b)[a<b & f(a)=f(b)] , (E x)(y) ~[x <= y & f(y) = 0]
Q1 proves (E a,b)[a<b & f(a)=f(b)] , (E x)(y) ~[x <= y & f(y) = 1]
P proves (x0)(E y0)[ x0 <= y0 & f(y0) = 0],(x1)(E y1)[ x1 <= y1 & f(y1) = 1]
that we can write
Qi proves C,Ai*
P proves A0,A1
where C is Sigma01, and A0, A1 are Pi02. These cut-free proofs can be
considered as simple strategies that are proofs, and extend
canonically to evidences.
If we consider
CUT(Q0,P) which is a strategy for C,A1
this is an evidence for C,A1 and it can be checked that this is not a
canonical extension of a simple strategy.
If we form
CUT(CUT(Q0,P),Q1)
we get the expected proof of C. If we replace CUT(Q0,P) by the simple
strategy it defines, we get a proof of C that may look at 4 values for f.