Cтраница 3
Тарский ( и, по-видимому, несколько других математиков, в том числе К. Ге дель, не опубликовавший этого результата) нашел универсальный разрешающий метод для элементарной геометрии. Для проверки суждения достаточно было бы порождать все теоремы и ждать, которое из суждений Л, А появится первым. Обоснованность предположений Вейля была подтверждена теоремой Черча об алгоритмической неразрешимости исчисления предикатов и последующими результатами о неразрешимости систем, содержащих арифметику. Сравнение упомянутых выше результатов Тарского и Черча показывает, что в элементарной геометрии натуральные числа невыразимы. [31]