Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 64
Текст из файла (страница 64)
Т е о р е м а. Всякая формула бее формульных переменных и кванторов всеобщности, выводимая ие наших аксиом, является верифицируемой. Что касается обеих сделанных здесь оговорок, то ограничение, связанное с кваеторами всеобщности, может быть снято таким образом, что процедуру исключения кванторов всеобщности, а именно замену каждого выражения вида ч»хЯ (х) выражением ~Эх~Я (х) (и аналогичные замены для других связанных переменных), мы включим в процедуру редукции формулы.
Тем самым понятие редуцируелюсти, а вместе с ним и понятие верифицируемости распространится на формулы с кванторами всеобщности. После этого теорема о том, что всяка выводимая формула верифицируема, окажется справедливой для любых формул, не содержащих формульных переменных. Что касается выводимых формул, содержащих формульные переменные, то для них справедливо утверждение о том, что если получающаяся из них в результате подстановки формула сама формульных переменных не содержит, то она верифицируема. (Заметим, что в этом утверждении речь идет только о таких подстановках, при которых подставляемые формулы оказываются построенными из символов нашего формализма.) Из проведенного нами рассуждения мы можем также заключить, что при выводе формул, не содержащих формульных переменных, можно вообще избежать применения формульных переменных, заледенив те исходные формулы, в которых формульные переменные встречаются,— это будут тождественные формулы исчисления высказываний, основные формулы (а) и (Ь) и формула ([е) — соответствующими схемами аксиом.
Каждая такая схема аксиом состоит в договоренности о том, что всякую формулу определенного заданного вида разрешается использовать в качестве исходной формулы. Так, например, тождественной формуле А~/ 1А соответствует договоренность о том, что каждая формула Я~/ 1Я может быть допущена в качестве исходной формулы, а формуле у"хА (х) -». А (а) соответствует договоренность о том, что в качестве исходной может быть допущена любая формула вида ЧЕЯ (х) -». Я (а). ~О д. Реяесерт, и.
Ееркеее !гл. ч> ПЕРЕХОД К ОДНОЙ СИСТЕМЕ АКСИОМ 367 НАЧАЛА АРИФМЕТИКИ 306 При этом понятие ф о р м у л ы ограничивается таким образом, что формульные переменные с аргументами или беэ иих в качестве злементарных формул более не допускаются и тем самым вообще предотвращается появление формульных переменных. Поскольку для нас главным является не само изображение логических теорем посредством формул, а формализация логики как способа вывода, для формальной дедукции этот способ на самом деле равносилен примененному нами способу, использующему исходные формулы с формульными переменными.
Это непосредственно усматривается из процедуры возвратного переноса подстановок в исходные формулы и исключения оставшихся форл>ульных переменных '). Действительно, с помощью этой процедуры мы приходим к такой фигуре разложения, у которой на месте тех исходных формул, которые содержали формульные переменные, стоят аналогично построенные, но свободные от формульных переменных исходные формулы, которые получаются из первоначальных формул подстановкой т). В дальнейшем мы будем иметь в виду установленный здесь факт возможности обходиться без использования формульных переменных. 4 4.
Переход к одной (в области формул, не содержащих формульных переменных) дедуктивно завершенной системе аксиом !. Выводимость ряда верифицируемых формул в рассматриваемой системе аксиом; доказательство с помощью «цифр второго рода» . Теперь мы вернемся к нашему основному результату, который утверждает, что всякая формула без формульных переменных, построенная из введенных нами символов и выводиыая средствами исчисления предикатов иэ аксиом ') ((>)> (7е)>,(<.)> (<е)> (<о)> (Р>)> (Рт), является также и верифицируемой. Этот результат подсказывает нам вопрос о том, не имеет ли место и обратная теорема, т. е. не является ли любая построенная из введенных нами символов верифицируемая формула выводимой из упомянутых аксиом средствами исчисления предикатов.
На этот вопрос следует дать отрицательный ответ. Именно, можно указать различные примеры формул, построенных иа введенных нами символов, которые, будучи верифицируемыми, выво- >) См. с. 278 — 283. е) Схемы аксиом как средство, пеевелкющее кобе>кать употребления формулькых переменных, были впервые пркмекекы Дж. фок Неймаком в работе: )>) е п >и а и и !.
чоп. Епг Н!1Ьег>есЬеп Ве>че)е>ьеег!е.— Ыв>Ь. Х., !927, 26, эй С о) См. е. 273. дил>ыми не являются. Такова, например, формула а < Ь вЂ” >- а' = Ь !/а' < Ь. О одной стороны, как легко видеть, она является верифицируемой, а с другой стороны, она не может быть выведена из наших аксиом. Это можно доказать с помощью некоторой модификации метода, примененного нами для установления непротиворечивости рассматриваемой нами системы аксиом. Мы расширим понятие цифры, введя в качестве цифр нового рода символ а и те фигуры а1>), которые получатся из а в результате однократного или многократного навешивания символа штриха.
Эти цифры, в отличие от цифр в обычном смысле слова (ц и ф р первого рода),л>ыбудемназывать цифрами второг о р о д а. Это определение и название будут иснольэоваться только в рамках излагаемого здесь доказательства. Подстановка цифр второго рода и построенных из них формул в нашем дедуктивном формализме допускаться не будет. Мы будем использовать их лишь для модификации определения понятия верифицируемости. Эту модификацию мы получим, надлежащим образом обобщив определениятерминов н ум е р и ч е с к и й, и с т и ни ы й, л о ж н ы й и соответствующим образом видоизменив процедуру редукции.
Формулу мы будем называть нумерической, если она является равенством или неравенством между цифрами (первого или второго рода) или если она получается из формул этого типа с помощью связок исчисления высказываний. Определение истинности и ложности для нумерических равенств, а также для неравенств между двумя цифрами первого рода и между двумя цифраыи второго рода остается прежним; в соответствии со сказанным, неравенство а(!) < а(!) считается истинным, если а() отлично от а( ) и является составной частью и! ), в противном случае оно считается ложным. Для нера! венств между цифрой первого рода и цифрой второго рода мы соглашаеыся о нижеследующем: для каждой цифры второго рода и нера- венство 0<п п<0 истинно, а неравенство истинно, а неравенство 3 < и то* ложно.
Для каждой отличной от 0 цифры первого рода Ь и для каждой цифры второго рода и неравенство п<3 [гл. Тг НАЧАЛА АРИФМЕТИКИ ПЕРЕХОД К ОДНОЙ СИСТЕМЕ АКСИОМ ложно. Исходя из определений истинности и ложности для равенств и неравенств, зги определения можно сформулировать (в точности так же, как зто делалось раньше) и для случая произвольной нумерической формулы. Для этих обобщенных определений истинности и ложности процедуру редукции можно будет втщоизменить таким образом, что теорема об однозначности и теорема о частичной редукции снова окажутся верными.
В самом деле, чтобы удовлетворить атому требованию, мы должны будем изменить только и. 4 процедуры редукции ") и подобрать соответствующие замены для выражений Зяб (х(0)з с учетом изменения содержательного смысла формул, вызванного появлением цифр второго рода; в первоначальной процедуре редукции зти замены производились в соответствии с обычным содержательньгм смыслом формул. Теперь в случае равенства хВ)=с или неравенств х(~~$<фс и с < х(О мы должны различать случаи, когда на месте х или а стоит цифра первого нли цифра второго рода.
Это различие мы можем формализовать, так как свойства быть цифрой первого рода и соответственно цифрой второго рода можно изобразить с помощью формул 0' <ае и соответственно а' < О'. Эти формулы изображают укааанные свойства в том смысле, что при всякой замене переменной а цифрой первого рода первая формула переходит в истинную, а вторая — в ложную нумерическую формулу; а при каждой замене а цифрой второго рода первая формула переходит в ложную, а вторая — в истинную пумерическую формулу. Ввиду сказанного, мы приходим к следующим изменениям в процедуре редукции.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
