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

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

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

Правила редукции

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