ДЕДУКЦИИ ТЕОРЕМА

ДЕДУКЦИИ ТЕОРЕМА - общее название ряда теорем, позволяющих устанавливать доказуемость импликации A ⊃ B в случае, когда дан логический вывод формулы В из формулы А. В простейшем случае классического, интуиционистского и т. п. исчислений высказываний Д. т. утверждает: если Г, А ⊢ В (из допущений Г, А выводимо В), то

Г ⊢ (A ⊃ B) (*)

(Г может быть пусто). При наличии кванторов аналогичное утверждение неверно:

А(х) ⊢ ∀х А(х),

но не

⊢ А(х) ⊃ ∀x A(х).

Одна из формулировок Д. т. для традиционных исчислений предикатов (классического, интуиционистского и т. п.): если Г, А ⊢ В, то

T⊢(∀A ⊃ B),

где ∀A означает результат приписывания ∀ -кванторов (см. Квантор) по всем свободным переменным формулы А. В частности, если А - замкнутая формула, Д. т. принимает форму (*). Эта формулировка Д. т. дает возможность сводить поиск вывода в аксиоматич. теориях к поиску вывода в исчислении предикатов: формула В выводима из аксиом A₁, ..., A_n тогда и только тогда, когда в исчислении предикатов выводима формула

∀A₁ ⊃ (∀A₂ ⊃ ... ⊃ (∀A_n ⊃ B)...).

Похожим образом формулируется Д. т. для логик, где имеются связки, «похожие» на кванторы. Так, для модальных логик S4 и S5 Д. т. имеет вид: если Г, А ⊢ В, то

Г ⊢ (□A ⊃ B)

Более тонкие формулы Д. т. получаются, если вводить ∀-кванторы не по всем свободным переменным, а лишь по тем, к-рые связываются кванторами в процессе вывода. Говорят, что переменная y варьируется для формулы А в данном выводе, если у входит свободно в А и в рассматриваемом выводе имеется применение правила введения ∀ в заключение импликации (или введения ∃ в посылку), при к-ром вводится квантор по у, причем посылка этого применения зависит в данном выводе от А. Теперь Д. т. для традиционных исчислений предикатов уточняется так: если Г, А ⊢ В, то

Г ⊢ (∀y₁ ... y_n A ⊃ B),

где y₁, ..., y_n - полный список переменных, к-рые варьируются для А в данном выводе. В частности, если никакая свободная переменная из А не варьируется, то Д. т. принимает форму (*). При формулировке соответствующего уточнения Д. т. для модальных логик следует считать, что варьирование происходит в правилах введения □ в заключение импликации и ◇ - в посылку.

При установлении Д. т. для исчислений релевантной импликации (т. е. для систем, согласованных с истолкованием A ⊃ B как «В выводимо с существенным использованием допущения A») приходится либо модифицировать само понятие вывода, либо считать, что варьирование происходит при всяком использовании «постороннего» допущения; напр., при переходе от пары А, Г ⊢ С, Г ⊢ D к A, Г ⊢ (C&D) варьируется формула A, т. к. она не входит во второй член пары.

Если А не варьируется в данном выводе, то Д. т. принимает форму (*), а если А варьируется, то Д. т. принимает вид: если А, Г ⊢ В, то

Г ⊢ ((A & t) ⊃ В),

где t - константа «истина» (или конъюнкция формул (p ⊃ p) для всех пропозициональных переменных р, выходящих в A, Г, В).

Лит.: [1] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [2] Карри X. Б., Основания математической логики, пер. с англ., М., 1969.

Г. Е. Минц.

Источники:

1. Математическая энциклопедия: Гл. ред. И. М. Виноградов, т. 2 Д - Коо.-М.: «Советская Энциклопедия», 1979.-1104 стб., ил.