системы H, а частным ее примером, применимым к конкретной системе F (т.е., собственно, H), будет теорема системы H. Таким образом, можно сформулировать один из выводов формальной системы H:
«система H обоснованна», а следовательно, «высказывание G(H) истинно»;
или, точнее, скажем так:
«система H непротиворечива», а следовательно, «высказывание G(H) истинно».
Если говорить о реальном смысле этих утверждений, то из них, в сущности, следует, что высказывание G(H) также утверждается системой. А так как (что касается первого из двух вышеприведенных утверждений) истинность любого производимого системой H утверждения, во всяком случае, обусловлена допущением, что система H обоснованна, то получается, что если система H утверждает нечто, явно обусловленное ее собственной обоснованностью, то она вполне может утверждать это напрямую. (Из утверждения «если мне можно верить, то X истинно» следует более простое утверждение, исходящее из того же источника: «X истинно».) Однако в действительности обоснованная формальная система H не может утверждать истинность высказывания G(H), что является следствием ее неспособности утверждать собственную обоснованность. Более того, как мы видим, она не может включать в себя и смысл символов, которыми оперирует. Те же факты годятся и для иллюстрации второго утверждения, причем в этом случае ко всему прочему добавляется и некоторая ирония: система H не способна утверждать собственную непротиворечивость лишь в том случае, если она действительно непротиворечива, если же формальная система непротиворечивой не является, то подобные ограничения ей неведомы. Противоречивая формальная система H может утверждать (в качестве «теоремы») вообще все, что она в состоянии сформулировать! Она вполне может, как выясняется, сформулировать и утверждение: «система М. непротиворечива». Формальная система (достаточно обширная) утверждает собственную непротиворечивость тогда и только тогда, когда она противоречива!
Q19. Почему бы нам просто не учредить процедуру многократного добавления высказывания G(F) к любой системе F, какой мы в данным момент пользуемся, и не позволить этой процедуре выполняться бесконечно?
Когда нам дана какая-либо конкретная формальная система F, достаточно обширная и полагаемая обоснованной, мы в состоянии понять, как добавить к ней высказывание G(F) в качестве новой аксиомы и получить тем самым новую систему F1, которая также будет считаться обоснованной. (Для согласования обозначений в последующем изложении систему F можно также обозначить через F0.) Теперь мы можем добавить к системе F1 высказывание G (F1), получив в результате новую систему F2, также, предположительно, обоснованную. Повторив данную процедуру, т.е. добавив к системе F2 высказывание G (F2), получим систему F3 и т.д. Приложив еще совсем немного усилий, мы непременно сообразим, как построить еще одну формальную систему Fω, аксиомы которой позволят нам включить в систему в качестве дополнительных аксиом для F все бесконечное множество высказываний {G(F0), G (F1), G(F2), G(F3), …}. Очевидно, что система Fω также будет обоснованной. Этот процесс можно продолжить и дальше: к системе Fω добавляется высказывание G (Fω), в результате чего получается система Fω+1, к которой затем добавляется высказывание G(Fω +1), что дает систему Fω+2, и т.д. Далее, как и в предыдущий раз, мы можем построить формальную систему Fω2 (=Fω+ω), включив в нее весь бесконечный набор соответствующих аксиом, каковая система опять-таки окажется очевидно обоснованной. Добавлением к ней высказывания G (Fω2), получим систему Fω2+1 и т.д., а потом построим новую систему Fω3 (=Fω2+ω), включив в нее опять-таки бесконечное множество аксиом. Повторив всю вышеописанную процедуру, мы сможем получить формальную систему Fω4, после следующего повтора — систему Fω5 и т.д. Еще чуть-чуть потрудиться, и мы обязательно увидим, как можно включить уже это множество новых аксиом {G (Fω), G (Fω2), G (Fω3), G (Fω4), …} в новую формальную систему Fω2 (=Fωω). Повторив всю процедуру, мы получим новую систему Fω2 +ω2, затем — систему Fω2 +ω2+ω2 и т.д.; в конце концов, когда мы сообразим, как связать все это вместе (разумеется, и на этот раз не без некоторого напряжения умственных способностей), наши старания приведут нас к еще более всеобъемлющей системе Fω3, которая также должна быть обоснованной.
Читатели, которые знакомы с понятием канторовых трансфинитных ординалов, несомненно, узнают индексы, обычно используемые для обозначения таких чисел. Тем же, кто от подобных вещей далек, не стоит беспокоиться из-за незнания точного значения этих символов. Достаточно сказать, что описанную процедуру «гёделизации» можно продолжить и далее: мы получим формальные системы Fω4, Fω5, …, после чего придем к еще
