Ranadom Numbers (was: The Lambda Point)

[Jon Awbrey]

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Antti Karttunen wrote:

<some stuff on the frog remainder theorem>

I've been trying to remember how I got into this
particular briar patch, and then I ran into this
passage in my reading that reminded me:

| At this time, Gödel represented symbols by natural numbers,
| sentences by sequences of numbers, and proofs by sequences of
| sequences of numbers.  All these notions and also the substitution
| function are easily expressible even in small finitary subsytems of
| type theory or set theory.  Hence there are undecidable propositions
| in every system containing such a system.  The undecidable propositions
| are finitary combinatorial in nature.
|
| In September 1930, Gödel attended a meeting at Königsberg (reported in
| the second volume of 'Erkenntnis') and announced his result.  R. Carnap,
| A. Heyting, and J.v. Neumann were at the meeting.  v. Neumann was very
| enthusiastic about the result and had a private discussion with Gödel.
| In this discussion, v. Neumann asked whether number-theoretical
| undecidable propositions could also be constructed in view of
| the fact that the combinatorial objects can be mapped onto
| the integers and expressed the belief that it could be done.
| In reply, Gödel said, "Of course undecidable propositions
| about integers could be so constructed, but they would
| contain concepts quite different from those occurring
| in number theory like addition and multiplication".
| Shortly afterward Gödel, to his own astonishment,
| succeeded in turning the undecidable proposition
| into a polynomial form preceded by quantifiers
| (over natural numbers).  At the same time but
| independently of this result, Gödel also
| discovered his second theorem to the
| effect that no consistency proof of
| a reasonably rich system can be
| formalized in the system itself.
| (Wang, pages 42-43).
|
| Hao Wang, 'Reflections on Kurt Gödel',
| MIT Press, Cambridge, MA, 1987.

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o