Принцесса или тигр   ::   Смаллиан Рэймонд

Данная ситуация очень похожа на положение дел с построением при помощи циркуля и линейки в евклидовой геометрии: там, для того чтобы показать, что некое построение (например, трисекция угла, квадратура круга или удвоение куба[! То есть построение куба с объемом, вдвое большим, чем объем данного куба. — Прим. перев.!]) невозможно, требуется обычно более критическое определение понятия «построение», чем для того, чтобы показать, например, что то или иное геометрическое построение с помощью циркуля и линейки действительно возможно. То же самое происходит и с доказуемостью: чтобы продемонстрировать, что данное утверждение недоказуемо в некоторой исходной системе аксиом, требуется гораздо более строгое и критическое определение самого понятия «доказательство», чем для получения соответствующего положительного результата, а именно что данное утверждение в самом деле является доказуемым при принятии той или иной аксиомы.

Загадка Гёделя



— Итак, — продолжал Фергюссон, — если задана некоторая система аксиом, то доказательство в данной системе представляет собой конечную последовательность высказываний, построенную по очень строгим правилам. При этом оказывается совсем несложно чисто механическим путем решить, является ли данная последовательность высказываний доказательством в этой системе или нет. Собственно говоря, совсем несложно даже придумать машину, которая может это делать. Гораздо труднее оказывается создать такую машину, которая могла бы решать, какие высказывания в данной системе аксиом доказуемы, а какие нет.