النفي المزدوج

يمكن كتابة قاعدة إدخال النفي المزدوج باستخدام تدوين التسلسل :

${\displaystyle P\vdash \neg \neg P}$

يمكن كتابة قاعدة حذف النفي المزدوج على النحو التالي:

${\displaystyle \neg \neg P\vdash P}$

في شكل قاعدة :

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

و

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

أو كجملة تكرارية (جملة حسابية بسيطة):

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

و

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

يمكن دمج هذه في صيغة ثنائية الشرط واحدة:

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

بما أن التكافؤ هو علاقة تكافؤ ، فإن أي حالة من ¬¬ A في صيغة جيدة التكوين يمكن استبدالها بـ A ، مما يترك قيمة الصدق للصيغة جيدة التكوين دون تغيير.

يُعدّ حذف النفي المزدوج نظريةً في المنطق الكلاسيكي ، ولكنه ليس كذلك في أنواع المنطق الأضعف كالمنطق الحدسي والمنطق الأدنى . أما إدخال النفي المزدوج فهو نظرية في كلٍّ من المنطق الحدسي والمنطق الأدنى، وكذلك${\displaystyle \neg \neg \neg A\vdash \neg A}$.

بسبب طبيعتها البنّاءة، تُعتبر عبارة مثل " ليس صحيحًا أنها لا تمطر" أضعف من عبارة "إنها تمطر". فالأخيرة تتطلب دليلًا على المطر، بينما الأولى تتطلب فقط دليلًا على أن المطر لن يكون متناقضًا. ويظهر هذا التمييز أيضًا في اللغة الطبيعية في شكل التورية .

في أنظمة الاستدلال الاستنتاجي على نمط هيلبرت لمنطق القضايا، لا يُعتبر النفي المزدوج دائمًا بديهية (انظر قائمة أنظمة هيلبرت )، بل هو بالأحرى نظرية. نصف برهان هذه النظرية في نظام البديهيات الثلاث الذي اقترحه يان لوكاسيفيتش :

أ1.${\displaystyle \phi \to \left(\psi \to \phi \right)}$

أ2.${\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}$

أ3.${\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}$

نستخدم اللمة${\displaystyle p\to p}$تم إثبات ذلك هنا ، والذي نشير إليه باسم (L1)، ونستخدم اللمة الإضافية التالية، التي تم إثباتها هنا :

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

نثبت أولاً${\displaystyle \neg \neg p\to p}$للاختصار، نرمز إلى${\displaystyle q\to (r\to q)}$بواسطة φ _0. كما نستخدم بشكل متكرر طريقة نظرية القياس الافتراضي كاختصار لعدة خطوات إثبات.

(1)${\displaystyle \varphi _{0}}$   (مثال على (A1))

(2)${\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\neg p\to \neg \varphi _{0})}$   (مثال على (A3))

(3)${\displaystyle (\neg p\to \neg \varphi _{0})\to (\varphi _{0}\to p)}$   (مثال على (A3))

(4)${\displaystyle (\neg \neg \varphi _{0}\to \neg \neg p)\to (\varphi _{0}\to p)}$   (من (2) و (3) بواسطة نظرية القياس المنطقي الافتراضي)

(5)${\displaystyle \neg \neg p\to (\neg \neg \varphi _{0}\to \neg \neg p)}$   (مثال على (A1))

(6)${\displaystyle \neg \neg p\to (\varphi _{0}\to p)}$   (من (4) و (5) بواسطة نظرية القياس المنطقي الافتراضي)

(7)${\displaystyle \varphi _{0}\to ((\varphi _{0}\to p)\to p)}$   (مثال على (L2))

(8)${\displaystyle (\varphi _{0}\to p)\to p}$   (من (1) و (7) عن طريق الاستدلال المنطقي)

(9)${\displaystyle \neg \neg p\to p}$   (من (6) و (8) بواسطة نظرية القياس المنطقي الافتراضي)

نثبت الآن${\displaystyle p\to \neg \neg p}$.

(1)${\displaystyle \neg \neg \neg p\to \neg p}$   (مثال على الجزء الأول من النظرية التي أثبتناها للتو)

(2)${\displaystyle (\neg \neg \neg p\to \neg p)\to (p\to \neg \neg p)}$   (مثال على (A3))

(3)${\displaystyle p\to \neg \neg p}$   (من (1) و (2) عن طريق الاستدلال المنطقي)

والدليل قد اكتمل.