S , S --> L
-----------
L
где всякий раз каждая посылка, т. е. в упомянутых формулах S и S --> L, есть либо аксиома (или получается из аксиомы при помощи подстановки) или совпадает с заключительной формулой некоторого вывода, уже встречавшегося ранее в доказательстве (или получается из этой формулы при помощи подстановки). Формулу мы будем называть доказуемой, если она является либо аксиомой, либо конечной формулой некоторого доказательства.
Нашей программой мы уже предрешили выбор аксиом для нашей теории доказательства. Несмотря на некоторый произвол в выборе аксиом, здесь, как и в геометрии, различаются качественно отдельные, обособленные группы, из которых мы будем каждый раз приводить некоторые примеры:
I. Аксиомы следования:
A --> (B --> A) (добавление предпосылки);
(B --> C) --> {(A --> B) --> (A --> C)} (исключение высказывания).
II. Аксиомы отрицания:
{А --> (В&!В)} --> !А (закон противоречия);
!!A --> А (закон двойного отрицания)
Из закона противоречия следует, что
(A&!A) --> B,
а из закона двойного отрицания следует закон исключённого третьего:
{(А --> В) & (!A --> B)} --> В.
Аксиомы групп I и II суть не что иное, как аксиомы исчисления высказываний.
III. Трансфинитные аксиомы:
(х)А(х) --> А(а) (заключение от общего к частному, аксиома Аристотеля)
(!х)А(х) --> (Ех)!(A(х)) (если сказуемое справедливо не для всех объектов, то существует противоречащий пример);
!(Ех)А(х) --> (х)!А(х) (если не существует примера, для которого некоторое высказывание имело бы место, то это высказывание ложно для всех х).
При этом выявляется то замечательное обстоятельство, что все эти трансфинитные аксиомы могут быть выведены из одной, а именно той, которая содержит одновременно и ядро так называемой аксиомы произвольного выбора, более всего оспаривавшейся до сих пор в математической литературе. Указанная аксиома такова:
А(а) --> А(ε(А)),
где ε — трансфинитная логическая функция выбора.
К этому добавляются чисто математические аксиомы:
IV. Аксиомы равенства:
а = а, а = b --> (А(а) --> А(b))
V. Аксиомы числа:
а' ≠ 0,
а также аксиома полной индукции:
{A(0)&(x)(A(x) --> A(x'))} --> A(a).
Этим способом мы в состоянии провести нашу теорию доказательства и построить систему доказуемых формул, т. е. математическую науку.
Но на радостях по поводу наших успехов вообще и, в частности, по поводу исчисления логики, которое мы, не затрачивая на то никаких усилий, нашли в качестве столь необходимого оружия, мы не должны всё же забыть о существенной предпосылке, определяющей наши действия. Существует одно условие, правда, только одно, но зато абсолютно необходимое, с которым связано применение метода идеальных элементов; этим условием является