Следствия из теорем 10 и 11 сводят понятие выводимости “A1,…, Am |- В” к понятию доказуемости “|-E ” подобно тому, как следствие из теоремы 8 сводит отношение следования “A1, …, Am |=B” к понятию общезначимости “|=Е”.
Если же мы окажемся в состоянии доказать, что “|-Е” и “|=E” равносильны, то мы завершим установление эквивалентности теории моделей и теории доказательств на уровне исчисления высказываний как при рассмотрении “абсолютных логических истин”, так и в случае допущений А1,…,Аm. Именно в этом суть теорем 12 и 14.
Теорема 12.
Всякая доказуемая формула общезначима; в наших обозначениях: Если |- E, то |=E.
Следствие.
Не существует формулы В1, такой, что доказуемы формулы В и Ø В; в наших обозначениях: ни для какой формулы. В не выполняется одновременно |-В | и- Ø B.
Теорема 12 устанавливает “непротиворечивость исчисления высказываний относительно общезначимости”, а ее следствие устанавливает так называемую “простую непротиворечивость”.
Прежде чем доказать обращение теоремы 12 нам придется поосновательнее развить теорию доказательств для исчисления высказываний.
Весьма. полезным орудием для этого послужит нам теорема о дедукции. Начнем со списка из 14 правил, полученных модификацией правил Генцена (1934 — 5), которые мы |назовем правилами “введения” и “удаления” логических символов. Полноты ради в их число мы включим и саму теорему о дедукции под названием “É -введение” и некоторую модификацию МР-“|-” под названием “É -удаление”. Все прочие правила (за исключением “слабого Ø удаления”) сводятся по существу к переформулировке схем аксиом в свете этих двух правил, ради экономии места, будем обозначать через “Г” любой список формул (вoзмoжнo пустой), так что запись “Г, А |- В” означает “А1,…, Аm-1, Am |- В”, где Аm есть А (Г пуст, если m=1).