Двойное отрицание

В логике высказываний, двойное отрицание - это теорема, которая гласит: «Если утверждение истинно, то оно это не тот случай, когда утверждение неверно ". Это выражается в том, что предложение A логически эквивалентно не (не-A), или формулой A ≡ ~ (~ A), где знак ≡ выражает логическую эквивалентность, а знак ~ выражает отрицание.

Подобно закону исключенного среднего, этот принцип считается законом мысли в классическая логика, но она запрещена интуиционистской логикой. Этот принцип был сформулирован как теорема логики высказываний Расселом и Уайтхедом в Principia Mathematica как:

$\ast \; 4\; \cdot \; 13.\; ⊢.\; p\; \equiv \; \sim \; (\sim \; p)\; \{\backslash \; displaystyle\; \backslash \; mathbf\; \{*\; 4\; \backslash \; cdot\; 13\}.\; \backslash \; \backslash \; \backslash \; vdash.\; \backslash \; p\; \backslash \; \backslash \; Equiv\; \backslash \; \backslash \; Thicksim\; (\backslash \; Thicksim\; p)\}$

«Это принцип двойного отрицания, т. е. пропозиция эквивалентна ложности ее отрицания. "

• 1 Исключение и введение
  • 1.1 Формальная запись
• 2 Доказательства
  • 2.1 В классической системе исчисления высказываний
• 3 См. также
• 4 Ссылки
• 5 Библиография

'Исключение двойного отрицания и введение двойного отрицания - это два действительных правила замены. Это выводы о том, что если A истинно, то не-A истинно, а его обратное, что если не-A истинно, то A истинно. Правило позволяет ввести или исключить отрицание из формального доказательства. Правило основано на эквивалентности, например, ложно, что не идет дождь. и идет дождь.

Правило введения двойного отрицания:

P $\Rightarrow \; \{\backslash \; displaystyle\; \backslash \; Rightarrow\}$$\neg \; \{\backslash \; displaystyle\; \backslash \; neg\}$$\neg \; \{\backslash \; displaystyle\; \backslash \; neg\}$P

и двойное отрицание правило исключения:

$\neg \; \{\backslash \; displaystyle\; \backslash \; neg\}$$\neg \; \{\backslash \; displaystyle\; \backslash \; neg\}$P $\Rightarrow \; \{\backslash \; displaystyle\; \backslash \; Rightarrow\}$P

Where "$\Rightarrow \; \{\backslash \; displaystyle\; \backslash \; Rightarrow\}$"- это металогическийсимвол, представляющий" может быть заменен в доказательстве на ".

В логике, которая имеет оба правила, отрицание - это инволюция.

Формальная нотация

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

$P\; ⊢\; \neg \; \neg \; P\; \{\backslash \; displaystyle\; P\; \backslash \; vdash\; \backslash \; neg\; \backslash \; neg\; P\}$

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

$\neg \; \neg \; P\; ⊢\; P\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; P\; \backslash \; vdash\; P\}$

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

$P\; \neg \; \neg \; P\; \{\backslash \; displaystyle\; \{\backslash \; frac\; \{P\}\; \{\backslash \; neg\; \backslash \; neg\; P\}\}\}$

и

$\neg \; \neg \; PP\; \{\backslash \; displaystyle\; \{\; \backslash \; frac\; \{\backslash \; neg\; \backslash \; neg\; P\}\; \{P\}\}\}$

или как тавтология (простое предложение исчисления высказываний):

$P\; \to \; \neg \; \neg \; P\; \{\backslash \; displaystyle\; P\; \backslash \; to\; \backslash \; neg\; \backslash \; neg\; P\}$

и

$\neg \; \neg \; P\; \to \; P\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; P\; \backslash \; to\; P\}$

Их можно объединить в одну двусмысленную формулу:

$\neg \; \neg \; P\; \leftrightarrow \; P\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; P\; \backslash \; leftrightarrow\; P\}$.

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

Двойное отрицательное исключение - это теорема классической логики, но не более слабых логик, таких как интуиционистская логика и минимальная логика. Введение двойного отрицания - это теорема как интуиционистской логики, так и минимальной логики, как и $\neg \; \neg \; \neg \; A\; ⊢\; \neg \; A\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; \backslash \; neg\; A\; \backslash \; vdash\; \backslash \; neg\; A\}$.

из-за их конструктивного характера, такое утверждение, как «Дело не в том, что дождь» слабее, чем «Дождь». Последнее требует доказательства дождя, тогда как первое требует просто доказательства того, что дождь не будет противоречивым. Это различие также проявляется в естественном языке в форме литот.

В классической системе исчисления высказываний

В дедуктивных системах Гильберта для пропозициональных В логике двойное отрицание не всегда принимается как аксиома (см. список систем Гильберта ), а скорее является теоремой. Опишем доказательство этой теоремы в системе трех аксиом, предложенной Яном Лукасевичем :

A1. $\varphi \; \to \; (\psi \; \to \; \varphi )\; \{\backslash \; displaystyle\; \backslash \; phi\; \backslash \; to\; \backslash \; left\; (\backslash \; psi\; \backslash \; to\; \backslash \; phi\; \backslash \; right)\}$

A2. $(\varphi \; \to \; (\psi \; \to \; \xi ))\; \to \; ((\varphi \; \to \; \psi )\; \to \; (\varphi \; \to \; \xi ))\; \{\backslash \; displaystyle\; \backslash \; left\; (\backslash \; phi\; \backslash \; to\; \backslash \; left\; (\backslash \; psi\; \backslash \; rightarrow\; \backslash \; xi\; \backslash \; right)\; \backslash \; вправо)\; \backslash \; to\; \backslash \; left\; (\backslash \; left\; (\backslash \; phi\; \backslash \; to\; \backslash \; psi\; \backslash \; right)\; \backslash \; to\; \backslash \; left\; (\backslash \; phi\; \backslash \; to\; \backslash \; xi\; \backslash \; right)\; \backslash \; right)\}$

A3. $(\neg \; \varphi \; \to \; \neg \; \psi )\; \to \; (\psi \; \to \; \varphi )\; \{\backslash \; displaystyle\; \backslash \; left\; (\backslash \; lnot\; \backslash \; phi\; \backslash \; to\; \backslash \; lnot\; \backslash \; psi\; \backslash \; right)\; \backslash \; to\; \backslash \; left\; (\backslash \; psi\; \backslash \; to\; \backslash \; phi\; \backslash \; right)\}$

Мы используем лемму $p\; \to \; p\; \{\backslash \; displaystyle\; p\; \backslash \; to\; p\}$доказано здесь, которую мы называем (L1), и используем следующие дополнительные доказанная лемма здесь :

(L2) $p\; \to \; ((p\; \to \; q)\; \to \; q)\; \{\backslash \; displaystyle\; p\; \backslash \; to\; ((p\; \backslash \; to\; q)\; \backslash \; to\; q)\}$

Сначала мы доказать $\neg \; \neg \; p\; \to \; p\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; p\; \backslash \; to\; p\}$. Для краткости мы обозначаем $q\; \to \; (r\; \to \; q)\; \{\backslash \; displaystyle\; q\; \backslash \; to\; (r\; \backslash \; to\; q)\}$через φ 0. Мы также неоднократно используем метод метатеоремы гипотетического силлогизма как сокращение для нескольких шагов доказательства.

(1) $\phi \; 0\; \{\backslash \; displaystyle\; \backslash \; varphi\; \_\; \{0\}\}$(экземпляр (A1))

(2) $(\neg \; \neg \; \phi \; 0\; \to \; \neg \; \neg \; p)\; \to \; (\neg \; p\; \to \; \neg \; \phi \; 0)\; \{\backslash \; displaystyle\; (\backslash \; neg\; \backslash \; neg\; \backslash \; varphi\; \_\; \{0\}\; \backslash \; to\; \backslash \; neg\; \backslash \; neg\; p)\; \backslash \; to\; (\backslash \; neg\; p\; \backslash \; to\; \backslash \; neg\; \backslash \; varphi\; \_\; \{0\})\}$(экземпляр (A3))

(3) $(\neg \; p\; \to \; \neg \; \phi \; 0)\; \to \; (\phi \; 0\; \to \; p)\; \{\backslash \; displaystyle\; (\backslash \; neg\; p\; \backslash \; to\; \backslash \; neg\; \backslash \; varphi\; \_\; \{0\})\; \backslash \; to\; (\backslash \; varphi\; \_\; \{0\}\; \backslash \; to\; p)\}$(экземпляр (A3))

(4) $(\neg \; \neg \; \phi \; 0\; \to \; \neg \; \neg \; p)\; \to \; (\phi \; 0\; \to \; p)\; \{\backslash \; displaystyle\; (\backslash \; neg\; \backslash \; neg\; \backslash \; varphi\; \_\; \{0\}\; \backslash \; to\; \backslash \; neg\; \backslash \; neg\; p)\; \backslash \; to\; (\backslash \; varphi\; \_\; \{0\}\; \backslash \; to\; p)\}$(из (2) и (3) по гипотетической метатеореме силлогизма)

(5) $\neg \; \neg \; p\; \to \; (\neg \; \neg \; \phi \; 0\; \to \; \neg \; \neg \; п)\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; p\; \backslash \; to\; (\backslash \; neg\; \backslash \; neg\; \backslash \; varphi\; \_\; \{0\}\; \backslash \; to\; \backslash \; neg\; \backslash \; neg\; p)\}$(экземпляр (A1))

(6) $\neg \; \neg \; p\; \to \; (\phi \; 0\; \to \; p)\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; p\; \backslash \; to\; (\backslash \; varphi\; \_\; \{0\}\; \backslash \; to\; p)\}$(из (4) и (5) по метатеореме гипотетического силлогизма)

(7) $\phi \; 0\; \to \; ((\phi \; 0\; \to \; p)\; \to \; p)\; \{\backslash \; displaystyle\; \backslash \; varphi\; \_\; \{0\}\; \backslash \; to\; ((\backslash \; varphi\; \_\; \{0\}\; \backslash \; к\; p)\; \backslash \; к\; p)\}$(экземпляр (L2))

(8) $(\phi \; 0\; \to \; p)\; \to \; p\; \{\backslash \; displaystyle\; (\backslash \; varphi\; \_\; \{0\}\; \backslash \; to\; p)\; \backslash \; to\; p\}$(из (1) и (7) по модусу поненс)

(9) $\neg \; \neg \; p\; \to \; p\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; p\; \backslash \; to\; p\}$(из (6) и (8) с помощью гипотетической метатеоремы силлогизма)

Теперь докажем $p\; \to \; \neg \; \neg \; p\; \{\backslash \; displaystyle\; p\; \backslash \; to\; \backslash \; neg\; \backslash \; neg\; p\}$.

(1) $\neg \; \neg \; \neg \; p\; \to \; \neg \; p\; \{\backslash \; displaystyle\; \backslash \; neg\; \backslash \; neg\; \backslash \; neg\; p\; \backslash \; to\; \backslash \; neg\; p\}$(пример первой части теоремы, которую мы только что доказали)

(2) $(\neg \; \neg \; \neg \; p\; \to \; \neg \; p)\; \to \; (p\; \to \; \neg \; \neg \; p)\; \{\backslash \; displaystyle\; (\backslash \; neg\; \backslash \; neg\; \backslash \; neg\; p\; \backslash \; to\; \backslash \; neg\; p)\; \backslash \; to\; (p\; \backslash \; to\; \backslash \; neg\; \backslash \; neg\; p)\}$(экземпляр (A3))

(3) $p\; \to \; \neg \; \neg \; p\; \{\backslash \; displaystyle\; p\; \backslash \; to\; \backslash \; neg\; \backslash \; neg\; p\}$(из (1) и (2) по modus ponens)

И доказательство завершено.

• Негативный перевод Гёделя – Гентцена

• Уильям Гамильтон, 1860, Лекции по метафизике и логике, том. II. Логика; Под редакцией Генри Мансела и Джона Вейтча, Бостон, Гулд и Линкольн.
• Кристоф Сигварт, 1895, Логика: суждение, концепция и вывод; Второе издание, перевод Хелен Денди, Macmillan Co., Нью-Йорк.
• Стивен К. Клини, 1952, Введение в метаматематику, 6-е переиздание с исправлениями 1971, North-Holland Publishing Company, Амстердам, штат Нью-Йорк, ISBN 0-7204-2103-9.
• Стивен К. Клини, 1967, Mathematical Logic, Dover edition 2002, Dover Publications, Inc, Mineola NY ISBN 0-486-42533-9
• Альфред Норт Уайтхед и Бертран Рассел, Principia Mathematica to * 56, 2-е издание 1927 г., перепечатка 1962 г., Cambridge at the University Press.