WikiDer > Устранение конъюнкции

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

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

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

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

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

${ displaystyle { frac {P land Q} { поэтому P}}}$

и

${ displaystyle { frac {P land Q} { поэтому 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}$ суждения, выраженные в некоторых формальная система.

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