А как быть с правилами действия? Можем ли мы предположить, что настанет время, когда будет однозначно установлена неопровержимая обоснованность этих правил? Во многих формальных системах правилами действия служат достаточно простые утверждения, каждое из которых с очевидностью «неопровержимо», например: «Если установлено, что высказывание  Pявляется теоремой и высказывание  P⇒ Qявляется теоремой, то можно заключить, что высказывание Qтакже является теоремой» (относительно символа ⇒ «следует» см. НРК, с. 393, или [ 223]). Признать неоспоримую справедливость таких правил совсем не трудно. С другой стороны, среди правил действия встречаются и гораздо более тонкие отношения, справедливость которых вовсе не так очевидна; прежде чем прийти к однозначному решению относительно того, считать то или иное такое правило «неопровержимо обоснованным» или нет. нам, возможно, потребуется прибегнуть к весьма подробному и тщательному анализу. Более того, как мы вскоре убедимся, в наборе правил действия формальной системы Fнеизбежно имеются такие правила, неоспоримая обоснованность которых не может быть достоверно установлена ни одним математиком — причем мы все еще полагаем, что число аксиом в системе Fконечно.

В чем же причина? Перенесемся в воображении в то самое время, когда уже однозначно установлена неопровержимая справедливость всех аксиом формальной системы F. Перед нами открывается замечательная возможность без помех рассмотреть всю систему Fцеликом. Попробуем допустить, что все правила действия системы F можно также считать справедливыми безо всяких оговорок. Хотя предполагается, что мы еще не можем знать наверняка, что система Fдействительно включает в себя всю математику, которая в принципе доступна человеческому пониманию и интуиции, мы должны к настоящему моменту уже убедиться в том, что система Fявляется, по меньшей мере, неоспоримо обоснованной, поскольку справедливость как ее аксиом, так и ее правил действия безоговорочно нами принимается. Следовательно, мы также должны уже быть уверены в том, что система F непротиворечива. Не забываем, разумеется, и о том, что, в силу этой непротиворечивости, утверждение G( F) также должно быть истинным — более того, неопровержимо истинным! Однако, поскольку предполагается, что система F фактически (хотя нам об этом неизвестно) включает в себя всю совокупность того, что безоговорочно доступно нашему пониманию, утверждение G( F) должно на деле представлять собой теорему системы F. Согласно теореме Гёделя, такое, вообще говоря, возможно только в том случае, если формальная система F  противоречива. Если же система Fпротиворечива, то одной из теорем этой системы является утверждение «1 = 2». Следовательно, утверждение «1 = 2» должно быть, в принципе, доступно нашему математическому пониманию — очевидное противоречие!

Несмотря на это, следует, по крайней мере, учесть саму  возможностьтого, что математики действуют (не зная о том) в рамках системы F, которая является, по существу, необоснованной. К этому вопросу я еще вернусь в §3.4, пока же (в пределах данного раздела) будем полагать, что на самом деле процедуры, лежащие в основе математического понимания, целиком и полностью обоснованны. Приданных обстоятельствах, если мы продолжаем настаивать на том, что все правила действия нашей формальной системы Fс конечным набором аксиом безоговорочно истинны, нам остается лишь признать, что противоречие действительно имеет место. Следовательно, среди правил действия системы Fдолжно быть по крайней мере одно правило, обоснованность которого не может неопровержимо установить ни один математик (хотя в действительности это правило является обоснованным).

Все вышеприведенные рассуждения опирались на то допущение, что система Fзадается конечным набором аксиом. В качестве возможного альтернативного решения можно предположить, что количество аксиом в системе Fбесконечно. Относительно этой возможности необходимо сделать некоторые комментарии. Для того чтобы систему Fможно было определить как формальную в требуемом смысле — т.е. как систему, в рамках которой всегда можно однозначно установить (посредством некоторой заранее заданной вычислительной процедуры), что предполагаемое доказательство того или иного положения действительно является доказательством в соответствии с правилами системы, — необходимо, чтобы ее бесконечный набор аксиом можно было выразить каким-то конечно определяемым образом. Вообще говоря, всегда допускается некоторая свобода в отношении выбора конкретного способа представления формальной системы, в соответствии с которым операции системы определяются либо как аксиомы, либо как правила действия. Так, стандартная аксиоматическая система теории множеств — система Цермело—Френкеля (обозначаемая здесь как ZF) — включает в себя бесконечное количество аксиом, выражаемых посредством структур, называемых «схемами аксиом». Путем соответствующего переформулирования систему ZFможно выразить таким образом, что количество действительных аксиом станет конечным ^{40} . Более того, действуя определенным образом, такое можно проделать с любой схемой аксиом, являющейся «формальной» в требуемом нами вычислительном смысле [20].

Может создаться впечатление, что вышеприведенное рассуждение (целью которого является исключение из списка возможных вариантов случая II) применимо к любой (обоснованной) системе F, вне зависимости от того, конечно или бесконечно количество ее аксиом. Это и в самом деле так, однако в процессе приведения бесконечной схемы аксиом к конечному виду мы можем ввести новые правила действия, которые могут оказаться не столь самоочевидно обоснованными. Так, представляя себе, в  соответствии с вышеизложенными соображениями, времена, когда нам станут известны все аксиомы и правила действия системы F(при этом также предполагается, что все теоремы этой гипотетической системы в точности совпадают с теоремами, которые в принципе доступны человеческим пониманию и интуиции), мы никоим образом не можем быть уверены в принципиальной возможности неопровержимого установления обоснованности правил действия такой системы F, в отличие от ее аксиом (даже если эти правила действительно являются обоснованными). Дело в том, что, в отличие от аксиом, правила действия не принадлежат к теоремам формальной системы. Мы же полагаем, что неопровержимо установить можно лишь обоснованность теорем системы F.

Не совсем ясно, возможно ли продолжить данное рассуждение, оставаясь при этом в рамках строгой логики. Если мы полагаем справедливой возможность II, то нам приходится признать, что существует некая формальная система F(на основании которой человек постигает истинность Π ₁-высказываний), целиком и полностью понимаемая математиками, обладающая конечным набором аксиом, справедливость которых не вызывает никаких сомнений, и конечной системой правил действия R, которая, впрочем, содержит по крайней мере одну операцию, полагаемую фундаментально сомнительной. Каждая отдельно взятая теорема системы Fнеизбежно оказывается утверждением, истинность которого может быть неопровержимо установлена, — что, собственно говоря, удивительно, учитывая тот факт, что многие из этих теорем выводятся с помощью сомнительных правил системы R. Кроме того, хотя математик и может (в принципе) установить истинность каждой из упомянутых теорем в отдельности, единообразнойпроцедуры для этого не существует. Можно ограничить область рассмотрения теми теоремами системы F, которые представляют собой Π ₁-высказывания. Применяя сомнительную систему правил R, мы можем вычислительным способом сгенерировать перечень тех Π ₁-высказываний, справедливость которых может быть однозначно установлена математиками. В конечном счете, человек, воспользовавшись пониманием и интуицией, оказывается способен установить справедливость каждого из этих Π ₁-высказываний в отдельности. Однако в каждом конкретном случае для такого установления применяются методы рассуждений, существенно отличающиеся от правила R, с помощью которого было получено данное Π ₁-высказывание. Раз за разом нам приходится добавлять в систему все новые, все более изощренные плоды человеческого разума — с тем, чтобы можно было неопровержимо доказать истинность каждого последующего Π ₁-высказывания. Словно по волшебству, истинными оказываются все Π ₁-высказывания, впрочем истинность некоторых из них можно установить лишь после привлечения какого-либо фундаментально нового метода рассуждения, причем необходимость в этом возникает вновь и вновь, на все более глубоких уровнях. Более того, любоеΠ ₁-высказывание, неоспоримую истинность которого можно установить — причем неважно, каким методом, — оказывается уже включенным в тот самый перечень, который мы сгенерировали ранее с помощью системы правил R. Наконец, существует еще и особое  истинноеΠ ₁-высказывание G( F), которое явным образом выводится из знания формальной системы F, однако истинность которого не можетбыть неопровержимо установлена ни одним математиком. В лучшем случае, математик сможет понять, что истинность G( F) непосредственно обусловлена обоснованностью сомнительной системы правил действия R, которая, по всей видимости, обладает некоей чудесной способностью определять, истинность каких именно Π ₁-высказываний может быть неопровержимо установлена человеком.