Устранение конъюнкции - Conjunction elimination
Правила трансформации |
---|
Исчисление высказываний |
Правила вывода |
Правила замены |
Логика предикатов |
В логике высказываний , устранение конъюнкции (также называются и устранение , ∧ устранение или упрощение ) является действительной непосредственным умозаключением , форма аргумента и правила логического вывода , который делает вывод , что, если соединение А и В истинно, то верно, и B верно. Правило позволяет сократить более длинные доказательства , выводя одну из конъюнктов конъюнкции на прямой.
Пример на английском :
- Идет дождь и льет.
- Значит идет дождь.
Правило состоит из двух отдельных подправил, которые могут быть выражены на формальном языке как:
и
Эти два подправила вместе означают, что всякий раз, когда экземпляр « » появляется в строке доказательства, либо « », либо « » могут быть помещены в следующую строку отдельно. Приведенный выше пример на английском языке является применением первого подправила.
Формальное обозначение
В ликвидации конъюнкции Подправила может быть записано в секвенции записи:
и
где это металогическое символ означает , что является синтаксическим следствием из и является также синтаксическим следствием в логической системе ;
и выражаются как функциональные тавтологии истинности или теоремы логики высказываний:
и
где и суждения, выраженные в некоторой формальной системе .