Экспорт (логика)

Экспорт

Тип	Правило замены
Поле	Пропозициональное исчисление
Символическое заявление	$((P\land Q)\to R)\Leftrightarrow (P\to (Q\to R))$

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

$((P\land Q)\to R)\Leftrightarrow (P\to (Q\to R))$

Где " $\Leftrightarrow$«является металогическим символом , обозначающим «можно заменить в доказательстве на». В строгой терминологии, $((P\land Q)\to R)\Rightarrow (P\to (Q\to R))$ является законом экспорта, поскольку он «экспортирует» предложение из антецедента $(P\land Q)\to R$ к его последствию. Его обратный закон — закон импорта . $(P\to (Q\to R))\Rightarrow ((P\land Q)\to R)$, «импортирует» предложение из следствия $P\to (Q\to R)$ к своему предшественнику.

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

Правило экспорта можно записать в последовательной записи:

$((P\land Q)\to R)\dashv \vdash (P\to (Q\to R))$

где $\dashv \vdash$ металогический символ, означающий, что $(P\to (Q\to R))$ является синтаксическим эквивалентом $((P\land Q)\to R)$ в некоторой логической системе ;

или в форме правила :

${\frac {(P\land Q)\to R}{P\to (Q\to R)}}$, ${\frac {P\to (Q\to R)}{(P\land Q)\to R}}.$

где правило заключается в том, что везде, где экземпляр " $(P\land Q)\to R$" появляется в строке доказательства, его можно заменить на " $P\to (Q\to R)$", и наоборот.

Импорт-экспорт — это имя, данное утверждению как теореме или истинностной тавтологии логики высказываний:

$((P\land Q)\to R)\leftrightarrow (P\to (Q\to R))$

где $P$, $Q$, и $R$ Это предложения, выраженные в некоторой логической системе .

Естественный язык

Истинные ценности

В любой момент, если P→Q истинно, его можно заменить на P→(P∧Q).
Одним из возможных случаев P→Q является то, что P истинно, а Q истинно; таким образом, P∧Q также истинно, и P→(P∧Q) истинно.
Другой возможный случай устанавливает P как ложь, а Q как истину. Таким образом, P∧Q ложно, а P→(P∧Q) ложно; ложь → ложь — правда.
Последний случай имеет место, когда и P, и Q ложны. Таким образом, P∧Q ложно, а P→(P∧Q) истинно.

Пример

Идет дождь и светит солнце, это означает, что есть радуга.
Таким образом, если идет дождь, то светит солнце, подразумевает наличие радуги.

Если моя машина включена, то когда я переключаю передачу на D, машина начинает двигаться. Если моя машина заведена и я переключил передачу на D, то машина должна тронуться.

Доказательство

Следующее доказательство использует классически допустимую цепочку эквивалентностей. Используемые правила — это импликация , закон Де Моргана и ассоциативное свойство соединения материальная .

Предложение	Вывод
$P\rightarrow (Q\rightarrow R)$	Данный
$\neg P\lor (Q\rightarrow R)$	материальный смысл
$\neg P\lor (\neg Q\lor R)$	материальный смысл
$(\neg P\lor \neg Q)\lor R$	ассоциативность
$\neg (P\land Q)\lor R$	Закон де Моргана
$(P\land Q)\rightarrow R$	материальный смысл

Отношение к функциям

Экспорт связан с каррированием через соответствие Карри-Ховарда .