Редукция (логика)

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Редукция (лат. reductio — сведение, возведение, приведение обратно) — логический приём преобразования каких-либо данных к более удобному с какой-либо точки зрения виду; сведение сложного к более простому, доступному для анализа или решения.

Общее прототипическое значение — сокращение, уменьшение.

Правила редукции[править | править исходный текст]

коньюнкции
[ \land ] \frac{\Gamma , A \land B , \Delta}{\Gamma, A, B, \Delta}
отрицания коньюнкции
[ \neg \land ] \frac{\Gamma , \neg ( A \land B ) , \Delta}{\Gamma, \neg A, \Delta \mid \Gamma, \neg B, \Delta}
дизъюнкции
[ \lor ] \frac{\Gamma , A \lor B, \Delta}{\Gamma, A, \Delta \mid \Gamma, B, \Delta}
отрицания дизъюнкции
[ \neg \lor ] \frac{\Gamma , \neg ( A \lor B ) , \Delta}{\Gamma, \neg A, \neg B, \Delta}
импликации
[ \supset ] \frac{\Gamma , A \supset B, \Delta}{\Gamma, \neg A, \Delta \mid \Gamma, B, \Delta}
отрицания импликации
[ \neg \supset ] \frac{\Gamma , \neg ( A \supset B ) , \Delta}{\Gamma, A, \neg B, \Delta}
отрицания отрицания
[ \neg \neg] \frac{\Gamma , \neg \neg A , \Delta}{\Gamma, A, \Delta}
квантора общности
[ \forall ] \frac{\Gamma , \forall x  A (x) , \Delta}{\Gamma, \forall x A(x), A(t), \Delta}
отрицания квантора общности
[ \neg \forall ] \frac{\Gamma , \neg \forall x  A (x) , \Delta}{\Gamma, \neg A(k), \Delta}
квантора существования
[ \exists ] \frac{\Gamma , \exists x  A (x) , \Delta}{\Gamma,  A(k), \Delta}
отрицания квантора существования
[\neg \exists ] \frac{\Gamma , \neg \exists x A (x) , \Delta}{\Gamma, \neg \exists x A (x), \neg A(t), \Delta}
, где t — произвольный терм