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

Conjunction elimination

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

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

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

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

и

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

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

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

и

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

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

и

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

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

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