То свойство (формального) вывода, которое выражено в следующей теореме, соответствует хорошо известному способу неформального рассуждения. Чтобы установить импликацию “Если А, то В”, вводят допущение А “в качестве необходимой посылки”» и пытаются вывести В. Точно так же поступают при дополнительных допущениях A1, …. Am-1.
Доказательство длиннее, чем в предыдущих теоремах. Но оно построено по простому плану, да и само сводится к рассмотрению четырех простых случаев.
Теорема 11. (Теорема о дедукции, Эрбран г).)
(а) Если A |- B, то |- AÉ B
(b) Если A1,…,Am-1, Am |- B, то A1,…,Am-1 |- AmÉ B Доказательство.
(b) Прежде всего надо отчетливо уяснить, что означают в силу определения символа “|-” предположение теоремы и ее заключение: и то и другое утверждают существование некоторого вида конечных списков формул, скажем B1,… Вl, и B1′,..,Bp’.
Между ними есть два различия. В первый список (но не во второй) формула может входить с обоснованием: m-е допущение Am. В первом списке последняя формула—это В; а во втором списке последняя формула—это AmÉ В.
Надо доказать, что всякий раз, как дан какой-нибудь вывод формулы В из
А1, …, Аm-1, Аm (данный вывод), можно найти вывод формулы АmÉ В из
А1,…, Аm-1. В действительности существует единый метод, позволяющий всегда по данному выводу находить вывод формулы AmÉ B из А1,…, Am-1 ( результирующийвывод ). Случай 1.
Пусть Вi — это одно из первых m -1 допущений А1,…, Am-1 которые и в получаемом выводе остаются допущениями; для определенности, пусть Вi — это Аj (j
k’. Aj — j-e допущение
k+1′. AjÉ (AmÉ Aj) — схема аксиом 1а
k+2′. AmÉ Ai — МР, k’, k+1′.
Случай 2. Пусть Вi — последнее допущение, т. е. Аm, которое в результирующем выводе не остается допущением (кроме случаев, когда Аm совпадает с одной из формул А1,…, Am-1. Вставим четыре первые формулы из доказательства формулы АÉ А , в которых заменим А на Аm.
Случай 3. Пусть Вi -некоторая аксиома. Поступаем так же, как в случае 1.
Случай 4. Пусть Вi — выводится из двух предшествующих формул Вg и Вh
(g, h < i ) посредством МР.