Математики доказывают теоремы, т. е. выводят следствия из определенных допущений, типично евклидовским способом: высказывания размещаются в некий их список, называемый “доказательством”, или “выводом”. Мы будем говорить о “доказательстве” называть допущения “аксиомами”, если они сохраняют свой атус (т. е. предполагаются истинными) во всей рассматриваемой теории; будем говорить о “выводе” (или “дедукции”), если мы не предполагаем, что все допущения сохраняют свой статус. Каждый переход от одного высказывания в рассматриваемом списке к другому в этом же списке обоснован логически, как проанализировано выше в случае логики высказываний. Например, высказывание вытекает из других высказываний, если оно является следствием (в исчислении высказываний), а это отношение между высказываниями уже определено с помощью истинностных таблиц. Некоторое высказывание может быть помещено в список без ссылок на другие высказывания, предшествующие ему, только тогда, когда оно является допущением или же является общезначимым. В своих определениях “следования” и общезначимости мы остаемся вне языка, в котором формулируются сами называния (предметный язык); для выяснения, каким образом высказывания (или формулы) составлены из атомов, у нас есть другой язык (язык исследователя). Именно в языке исследователя мы получаем различные результаты относительно общезначимости и отношения следования, которые зачастую удобнее в приложениях нежели непосредственное использование истинностных таблиц.Такое рассмотрение логики мы называем »теорией моделей»: заменяя атомы истинностными значениями t и f во всевозможных сочетаниях, мы получаем, так сказать, “модели”, конкретные “реализации”, воплощения того, что могут выражать высказывания.
Сейчас мы переходим к другому способу построения логики. Способ этот, называемый “теорией доказательств”, изучает вопрос, нельзя ли описать логические доказательства и выводы так, как это делается в геометрии. Но поскольку на этот раз сама логика, делается предметом аксиоматико-дедуктивной трактовки, выводы не должны больше основываться на “логических критериях”: они должны опираться лишь на точно сформулированные аксиомы и правила. В теории доказательств некоторые высказывания или формулы принимаются за “аксиомы”, а для получения новых высказываний устанавливаются некоторые “правила вывода”.
Изложим же формулировку теории доказательств для классического исчисления высказываний как ради него самого, так и с целью его приложения к выводу из допущений. Позднее мы увидим, что обе формулировки—теория моделей и теория доказательств — дают эквивалентные результаты.
Аксиомами нашей (теоретико-доказательственной) системы (классического) исчисления высказываний мы объявляем все формулы, имеющие один из видов, указанных после знака “|=” в пп. la — 10b теоремы 2. Сами эти виды мы будем называть схемами аксиом, или аксиомными схемами. Каждая схема аксиом содержит бесконечное число аксиом: при каждом конкретном выборе формул, обозначенных через “А”, “В”, “С”, получается одна из аксиом.
Определим (формальное) доказательство (в исчислении высказываний) как конечный список (вхождений) формул В1, …, Bl, каждая из которых или является некоторой аксиомой исчисления высказываний, или получена по É -правилу из некоторой пары формул, предшествующих ей в этом списке. Доказательство является доказательством своей — последней формулы Вl. Если формула В имеет доказательство, то мы говорим, что В (формально) доказуема или что В является (формальной) теоремой; записываем мы это так: |- В.
Несколько замечаний помогут лучше уяснить разумность такой трактовки исчисления высказываний как аксиоматико-дедуктивной теории. Каждая схема аксиом дает бесконечное число аксиом. Этого можно было бы избежать, «договорившись, что язык, к которому принадлежат атомы, содержит конкретные буквы в качестве “пропозициональных переменных”, и добавив второе правило вывода — “правило подстановки”,- условившись, что Е* можно получать из Е в условиях теоремы 1 , если Р1, . . . ,Рn — пропозициональные переменные. Но такая трактовка представляется нам менее согласованной с обычным математическим чем описанная выше (восходящая к фон Нейману).
Теорема 9.
( I )При m>=1 (II) При m,p>=0
A1,…,Am |- A1, Если A1,…,Am |- B1,
…., ….,
A1,…,Am |- Am, A1,…,Am |- Bp и B1,…,Bp |- C, то A1,…,Am |- C
Теорема 10
(a) Если |- AÉB,то A|-B
(b) Более обще, при любом m>=1, если A1,…,Am-1 |- AmÉB то A1,…,Am-1,Am |-B