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

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

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

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

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

и

Эти два подправила вместе означают, что всякий раз, когда экземпляр « » появляется в строке доказательства, либо « », либо « » могут быть помещены в следующую строку отдельно. Приведенный выше пример на английском языке является применением первого подправила.

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

В ликвидации конъюнкции Подправила может быть записано в секвенции записи:

и

где это металогическое символ означает , что является синтаксическим следствием из и является также синтаксическим следствием в логической системе ;

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

и

где и суждения, выраженные в некоторой формальной системе .

Ссылки