[FOM] Gentzen's consistency proof

[tchow]

At the risk of continuing a monologue that nobody else is
interested in, let me try to be even more specific, and
perhaps partially answer some of my earlier questions.

I'd like to understand exactly how much of Gentzen's proof
goes through in PRA.  Working in PRA, I think we can make
the following definitions.

For a natural number n, define "n is a game player" to mean
"n encodes an ordered pair (M,x) where M is a Turing machine
that plays Gentzen's reduction game on x."  This should be
easy because it's easy to check that M satisfies some simple
syntactic properties that ensure that it will follow the
rules for playing the game, and it's also easy to check that
x has the correct syntactic properties for encoding a sequent
(or whatever representation we are using to play the game).

Similarly define "n is a Gentzen game player" to mean that
n is a game player and that n arises from a PA-proof of x
Gentzen's inductive rules for constructing a winning
strategy step by step from a PA-proof of x.  Again, I don't
see any issues here because no fancy induction is needed
to step through a PA-proof and modify the Turing machine
appropriately at each step.

Now comes a part that I'm not sure about.  I'd like to define
"n is a winning game player" to mean that n is a game player
and that n has a winning strategy against an adversary.
What I'm worried about is that the naive way to state this
seems to require a potentially unbounded number of
alternations of quantifiers, or quantifying over game trees
(of which there could be uncountably many).  I suspect that
I'm just missing some standard encoding trick, and that it
should be possible to express "n is a winning game player"
while working in PRA, but I'm not seeing it right now.

If we assume that this is possible, then it seems to me that
the crucial step, which can't be done in PRA or even PA, is
to prove that "n is a Gentzen game player" implies "n is a
winning game player," because this would imply that PA is
consistent.  On the other hand, I think that the following
should be a theorem of PRA:

Theorem. If every Gentzen game player is a winning game
player, then PA is consistent.

If I haven't gone off the rails so far, then I think this
means that in any model of PRA + "PA is inconsistent" there
will be some Gentzen game player that is not winning, and
therefore an infinite descending sequence in some "ordinal"
below "epsilon_0" (where the scare quotes remind us that
we are talking about what these things mean in the
nonstandard model).

Still, even if all this is correct, it does not imply a
positive answer to my original question about whether
we can effectively construct an infinite descending
sequence in an ordinal below epsilon_0 from a PA proof.
If we imagine for a moment that PA is really inconsistent
and we have a finite sequence of (standard) Gentzen game
players in front of us, each associated with a step in
a PA-proof of "1=0", then one of those Gentzen game
players does not have a winning strategy.  But we don't
necessarily have an effective algorithm for constructing
the adversary's winning strategy.  We can write a program
to try every possible adversarial strategy but it is not
going to know whether it's currently traversing an
infinite descending sequence in an ordinal or whether
it's just taking a long time, and the real winning
strategy is still to come.

So I guess my main question now is whether "n is a winning
game player" is expressible in PRA, and if so, whether the
above "Theorem" is really a theorem of PRA.

Tim