FOM: Corrections to my note today on Consistency Proofs
wtait@ix.netcom.com
wtait at ix.netcom.com
Mon Mar 30 11:44:34 EST 1998
Naturally, ``quatifiers'' in
>(Assume that the conclusion of the original deduction contains no
>quatifiers, e.g. by taking its universal closure, and then replace all of
>the remaining free variables in the deduction by 0.)
is my private technical term for ``free variables''.
Also, `G(phi)' in
>The Gentzen consistency proof is in a different direction and is best
>understood as showing how to transform any proof of Delta in PA into a
>winning strategy for player DISJ in his game G(phi) with CONJ.
should be replaced by `G(Delta)'. (I don't know whether the `G' is for
game of for Gentzen.)
Bill Tait
More information about the FOM
mailing list