Устранение конъюнкции - Conjunction elimination

В логика высказываний, устранение соединения (также называемый и устранение, ∧ устранение,^[1] или же упрощение)^[2][3][4] это действительный немедленный вывод, форма аргумента и правило вывода что делает вывод что, если соединение А и Б верно, тогда А правда, и B правда. Правило позволяет укоротить дольше доказательства путем получения одного из конъюнктов конъюнкции на самой прямой.

Пример в английский:

Идет дождь и льет.

Значит идет дождь.

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

${\displaystyle {\frac {P\land Q}{\therefore P}}}$

и

${\displaystyle {\frac {P\land Q}{\therefore Q}}}$

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

Формальное обозначение

В устранение соединения подправила могут быть записаны в последовательный обозначение:

${\displaystyle (P\land Q)\vdash P}$

и

${\displaystyle (P\land Q)\vdash Q}$

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

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

${\displaystyle (P\land Q)\to P}$

и

${\displaystyle (P\land Q)\to Q}$

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

Рекомендации

1. Дэвид А. Даффи (1991). Принципы автоматизированного доказательства теорем. Нью-Йорк: Вили. Раздел 3.1.2.1, стр.46
2. Копи и Коэн^{[нужна цитата ]}
3. Мур и Паркер^{[нужна цитата ]}
4. Hurley^{[нужна цитата ]}