Carlos Casado - Вначале была аксиома. Гильберт. Основания математики

В 1939 году этому польскому ученому удалось переехать в США и на несколько десятилетий превратить университет Беркли в мировую столицу математической логики. Он любил работать ночью и увлекался психотропными средствами, которые помогали ему бодрствовать и трудиться без устали, а также имел репутацию Казановы.

Тарский знаменит тем, что в 1933 году опубликовал огромную статью, в которой дал формальное определение истине и таким образом обозначил начало теории моделей. Если Гильберт в своей теории доказательства прояснил синтаксическое понятие формального доказательства, Тарский сделал то же самое с семантическим понятием истины.

Альфред Тарский, 1968 год.

В 1933 году, через два года, после того как Гёдель объявил о двух результатах о неполноте, Тарский извлек на свет другую ограничительную теорему, хотя она уже была провозглашена и доказана Гёделем в письме Цермело, датированном 1931 годом. В этой ограничительной теореме установлено, что любая формальная теория первого порядка, содержащая базовую арифметику, неспособна (если она непротиворечива) выразить свое собственное понятие истины. Интересные непротиворечивые теории не могут содержать выражения «быть истинным» в своем языке, поскольку в этом случае они породили бы парадокс лжеца. С помощью гёделизации можно воспроизвести формулу Г, которая утверждает о самой себе, что она ложная. Воспользовавшись выражением «быть истинным», которое, предположительно, существует в языке, мы придем к следующему противоречию: Т истинное тогда и только тогда, если оно ложное, поскольку именно это утверждает Т. Как в случае с лжецом: я говорю правду, если я лгу. Без сомнения, математические логики сумели применить цикличность, лежащую в основе парадоксов, с большой пользой.

На IX Международном конгрессе математиков, проходившем в 1928 году в Болонье, Гильберт воспользовался случаем, чтобы предложить свой план по спасению математики и обозначить следующий вопрос: существует ли механическая процедура, которая решала бы все и каждую проблему математики, алгоритм, способный принципиально разрешить все математические вопросы, который при заданной математической пропозиции дал бы нам знать, является она теоремой или нет? Другими словами, является ли она разрешимой в математике? Как и на вопросы непротиворечивости и полноты, ответ на нее был отрицательным. После теорем Гёделя стало ясно, что ответ на эту проблему — категорическое «нет», поскольку математика является неполной: предполагаемый алгоритм в течение бесконечного времени «думал» бы над неразрешимым высказыванием, поскольку ни оно, ни его отрицание не являются теоремой. Следовательно, ответ на проблему разрешения оставалось дать только для логики первого порядка, которая, напомним, является полной. Однако в 1936 году Алан Тьюринг (1912-1954) и независимо от него Алонзо Чёрч (1903-1995) доказали, что логика первого порядка также неразрешима.

Для начала Тьюринг сформулировал, что означает думать как машина, механически. Его первая победа заключалась в определении понятия вычислимой функции: это функция, которую способна вычислить машина Тьюринга — вид компьютера без ограничений в пространстве или времени. Одновременно, по другую сторону Атлантического океана, Чёрч пришел к аналогичным выводам, разработав формальную систему, которую назвал лямбда-исчислением. С тех пор под названием тезиса Чёрча — Тьюринга известен постулат, утверждающий, что любое альтернативное определение вычислимости равносильно определению, данному Тьюрингом в терминах его машин. Прибегнув к изобретательному варианту диагонального аргумента Кантора, Тьюринг доказал, что существует намного больше функций, чем машин Тьюринга. Другими словами, существуют невычислимые функции.

Исчислимые функции, как и машины Тьюринга, имеются в счетном количестве, то есть они как иголки в стоге сена всех функций.

Наконец, рассмотрев проблему остановки, он предложил отрицательный ответ на вопрос Гильберта — Entscheidungsproblem: если бы существовала эта процедура, она также была бы способна определить за конечное время, останавливается любая машина Тьюринга через конечное число шагов или входит в бесконечную петлю, когда на входе вводятся некоторые данные. Но последнее, как он доказал, невозможно. Не существует алгоритма, способного получить на входе логическое или математическое высказывание и выдать на выходе: «теорема» или «не теорема» (хотя свойство выводимости действительно разрешимо в ограниченной логике пропозиций).