Исключение конъюнкции

В логике высказываний, исключение конъюнкции (также называемые и исключение, ∧ исключение или упрощение ) - это допустимый немедленный вывод, форма аргумента и правило вывода, которое делает вывод , что если соединение A и B истинно, то A истинно, а B истинно. Правило позволяет сократить более длинные доказательства, выводя одну из конъюнктов конъюнкции на самой прямой.

Пример на английском языке :

Дождь и льет.

Следовательно, идет дождь.

Правило состоит из двух отдельных подправил, которые могут быть выражены в формальный язык как:

$P\; \wedge \; Q\; \therefore \; P\; \{\backslash \; displaystyle\; \{\backslash \; frac\; \{P\; \backslash \; land\; Q\}\; \{\backslash ,\; следовательно,\; P\}\}\}$

и

$P\; \wedge \; Q\; \therefore \; Q\; \{\; \backslash \; displaystyle\; \{\backslash \; frac\; \{P\; \backslash \; land\; Q\}\; \{\backslash \; следовательно\; Q\}\}\}$

Два подправила вместе означают, что всякий раз, когда экземпляр "$P\; \wedge \; Q\; \{\backslash \; displaystyle\; P\; \backslash \; land\; Q\}$"появляется в строке доказательства, либо" $P\; \{\backslash \; displaystyle\; P\}$", или" $Q\; \{\backslash \; displaystyle\; Q\}$" может быть помещен в следующую строку отдельно. Приведенный выше пример на английском языке является применением первого подправила.

Подправила исключения конъюнкции могут быть записаны в секвенции нотации:

$(P\; \wedge \; Q)\; ⊢\; P\; \{\backslash \; displaystyle\; (P\; \backslash \; land\; Q)\; \backslash \; vdash\; P\}$

и

$(P\; \wedge \; Q)\; ⊢\; Q\; \{\backslash \; displaystyle\; (P\; \backslash \; land\; Q)\; \backslash \; vdash\; Q\}$

где $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$- это металогический символ, означающий, что $P\; \{\backslash \; displaystyle\; P\}$является синтаксическим следствием из $P\; \wedge \; Q\; \{\backslash \; displaystyle\; P\; \backslash \; land\; Q\}$и $Q\; \{\backslash \; displaystyle\; Q\}$также является синтаксическим следствием $P\; \wedge \; Q\; \{\backslash \; displaystyle\; P\; \backslash \; land\; Q\}$в логической системе ;

и выражается как функциональные тавтологии или теоремы логики высказываний:

$(P\; \wedge \; Q)\; \to \; P\; \{\backslash \; displaystyle\; (P\; \backslash \; земля\; Q)\; \backslash \; к\; P\}$

и

$(P\; \wedge \; Q)\; \to \; Q\; \{\backslash \; displaystyle\; (P\; \backslash \; land\; Q)\; \backslash \; to\; Q\}$

где $P\; \{\backslash \; displaystyle\; P\}$и $Q\; \{\backslash \; displaystyle\; Q\}$суждения, выраженные в некоторой формальной системе.