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

В логике высказываний , устранении конъюнкции (называемой также и ликвидации , ∧ ликвидация , ^[1] или упрощение ) ^{[2] [3] [4]} является действительным немедленным выводом , форма аргумента и правило вывода , который делает вывод , что, если соединение A и B истинно, тогда A истинно, а 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}$

Ссылки [ править ]