منطق بسيط

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

$${\displaystyle (B\to (A\land \neg A))\to \neg B,}$$

لأي قضيتين. لـ${\displaystyle B}$يُعتبر ذلك تناقضاً${\displaystyle A\land \neg A}$وهذا بحد ذاته يرسخ قانون عدم التناقض

$${\displaystyle \neg (A\land \neg A).}$$

بافتراض أي${\displaystyle C}$، قاعدة إدخال الشرط المادي تعطي${\displaystyle B\to C}$، وكذلك عندما${\displaystyle B}$و${\displaystyle C}$لا توجد علاقة ذات صلة . وبناءً على ذلك، ومع استبعاد الاستلزام، فإن مبدأ التقديم المذكور أعلاه يعني

$${\displaystyle (A\land \neg A)\to \neg B,}$$

أي بافتراض وجود أي تناقض، يمكن نفي كل قضية. وبما أن إدخال النفي ممكن في هذا المنطق، فإن أي تناقض يثبت أي نفي مزدوج. بدوره، إذا${\displaystyle \neg C}$يمكن إثبات ذلك بالنسبة للبعض${\displaystyle C}$ثم علاوة على ذلك دائماً${\displaystyle C\to \neg \neg B}$. يسمح الانفجار بإزالة النفي المزدوج في النتائج، لكن هذا المبدأ لا يتم اعتماده في المنطق الأدنى.

وبذلك، فإن العديد من التصريحات من هذا النوع${\displaystyle C\to B}$يُعتبر ذلك بمثابة انفجار في منطق بسيط. على سبيل المثال لا الحصر،${\displaystyle \neg (A\lor \neg A)\to B}$.

إحدى الطرق الممكنة لتوسيع حساب التفاضل والتكامل الإيجابي ليشمل المنطق الأدنى هي معالجة${\displaystyle \neg B}$كنتيجة ضمنية، وفي هذه الحالة تنتقل النظريات من حساب الاستلزام البنّاء للمنطق إلى عبارات النفي. ولتحقيق هذه الغاية،${\displaystyle \bot }$يُطرح كقضية، لا يمكن إثباتها إلا إذا كان النظام غير متسق، والنفي${\displaystyle \neg B}$ثم يتم التعامل معها كاختصار لـ${\displaystyle B\to \bot }$بشكل بنّاء،${\displaystyle \bot }$يمثل هذا اقتراحاً لا يوجد سبب يدعو إلى تصديقه.

أي دلالة على هذا الشكل${\displaystyle (A\to C)\to (A\to B)}$يعادل فقط${\displaystyle C\to B}$إذا كان العبث بدائيًا في المنطق، فإن مبدأ الانفجار الكامل (على سبيل المثال في الشكل مع${\displaystyle C=\bot }$وبالتالي، يمكن التعبير عن (كما سبق) بنفس الطريقة أيضًا على النحو التالي:${\displaystyle \bot \to B}$.

فيما يلي حجج سريعة توضح النظريات التي لا تزال قائمة في المنطق الأدنى، وغالبًا ما تستخدم ضمنيًا قاعدة التقييم الصحيحة ونظرية الاستنتاج .

يمكن الحصول على جميع المبادئ المذكورة أعلاه باستخدام نظريات من حساب التفاضل والتكامل الموجب بالإضافة إلى الثابت${\displaystyle \bot }$بدلاً من الصيغة التي تتضمن هذا الثابت، يمكن اعتماد مبدأ التناقض كمسلمات${\displaystyle (B\to A)\to (\neg A\to \neg B)}$بالإضافة إلى مبدأ النفي المزدوج${\displaystyle B\to \neg \neg B}$وهذا يعطي صياغة بديهية بديلة للمنطق الأدنى على الجزء الإيجابي من المنطق الحدسي.

يُثبت المنطق الأدنى التضعيف، أي يسمح بإدخال الاستلزام في الشكل الافتراضي.${\displaystyle C\to (B\to C)}$يلعب هذا المبدأ دوراً في اشتقاقات نظريات الاستنتاج .

قانون الهوية${\displaystyle A\to A}$يظل هذا صحيحًا حتى في المنطق الضعيف جدًا. وباستخدامه، يمكن في المنطق الأدنى استخدام التضعيف لإثبات${\displaystyle B\to (A\to A)}$.

في إثبات الضعف، على سبيل المثال، يختلف المنطق الأدنى عن منطق الصلة . لذا، من الطبيعي أن المنطق الذي نناقشه هنا ليس أدنى بالمعنى الرسمي.

عملياً، في السياق الحدسي، يُمكّن مبدأ الانفجار من إثبات القياس المنفصل في شكل قضية واحدة: $${\displaystyle ((A\lor B)\land \neg A)\to B.}$$ يمكن قراءة ذلك على النحو التالي: بالنظر إلى برهان بناء لـ${\displaystyle A\lor B}$والرفض البنّاء لـ${\displaystyle A}$، يسمح المرء بشكل غير مشروط باختيار الحالة الإيجابية لـ${\displaystyle B}$وهنا ليس فقط النفي المزدوج له. وبهذه الطريقة، يُعد القياس مبدأً لفكّ الفصل. ويمكن اعتباره نتيجةً شكليةً للانفجار، وهو يستلزمه أيضًا. وذلك لأنه إذا${\displaystyle A\lor B}$تم إثبات ذلك من خلال إثبات${\displaystyle B}$ثم${\displaystyle B}$وقد ثبت ذلك بالفعل، بينما إذا${\displaystyle A\lor B}$تم إثبات ذلك من خلال إثبات${\displaystyle A}$، ثم${\displaystyle B}$ويتبع ذلك أيضاً، حيث يسمح النظام الحدسي بالانفجار.

على سبيل المثال، إذا افترضنا وجود حجة بناءة مفادها أن رمي العملة المعدنية ينتج عنه إما صورة أو كتابة (${\displaystyle A}$أو${\displaystyle B}$)، إلى جانب حجة بناءة مفادها أن النتيجة لم تكن في الواقع صورة، فإن الاقتراح الذي يجسد القياس المنطقي يعبر عن أن هذا يشكل بالفعل حجة على حدوث كتابة.

إذا افترضنا اتساق نظام المنطق الحدسي من الناحية الميتافيزيقية، فيمكن قراءة القياس المنطقي على أنه يقول إن البرهان البنّاء لـ${\displaystyle A\lor B}$و${\displaystyle \neg A}$، في غياب بديهيات أخرى غير منطقية تُظهر${\displaystyle B}$، يحتوي في الواقع على عرض توضيحي لـ${\displaystyle B}$.

يثبت يوهانسون في مقاله أنه حتى لو${\displaystyle ((A\lor B)\land \neg A)\to B}$ليست نظرية في المنطق الأدنى، من حيث إمكانية إثبات${\displaystyle (A\lor B)\land \neg A}$، إمكانية إثبات${\displaystyle B}$يتبع ذلك. لذا، تُعدّ هذه الخطوة ما يُسمى قاعدة استدلال مقبولة . ويستخدم برهانه حساب التتابعات لجينتزن في المنطق الحدسي.

تُثبت الأشكال الضعيفة للانفجار القياس المنطقي الانفصالي، وفي الاتجاه الآخر، تُثبت حالة القياس المنطقي مع${\displaystyle A=\neg B}$يقرأ${\displaystyle {\big (}(B\lor \neg B)\land \neg \neg B{\big )}\to B}$وهو ما يعادل حذف النفي المزدوج للقضايا التي يكون فيها الوسط المرفوع صحيحًا $${\displaystyle (B\lor \neg B)\to (\neg \neg B\to B).}$$ بما أن الشرط المادي يمنح حذف النفي المزدوج للقضايا المثبتة، فإن هذا يعادل مرة أخرى حذف النفي المزدوج للقضايا المرفوضة.

وأخيرًا، مع الانفجار، في المنطق الحدسي${\displaystyle A\lor (\bot \to P)}$ينطبق هذا بشكل بديهي على أي${\displaystyle A}$على سبيل المثال، يمكن إثبات هذا الفصل بشكل حدسي أيضًا لـ${\displaystyle A=\bot }$، وهو فصل زائف (وهو أمر لا يمكن إثباته حتى في المنطق الكلاسيكي). وبشكل عام، لا يثبت المنطق الأدنى أيًا من الفصلين.

تُتيح نظرية هايتينغ الحسابية التالية إثبات ادعاءات الوجود التي لا يُمكن إثباتها، باستخدام هذه النتيجة العامة، دون مبدأ الانفجار. وتُعدّ النتيجة في جوهرها مجموعة من ادعاءات الحذف البسيطة باستخدام النفي المزدوج.${\displaystyle \exists }$- جمل تربط مسندًا قابلًا للحساب.

يترك${\displaystyle P}$ليكن أي مسند خالٍ من المحددات الكمية، وبالتالي قابل للتقرير لجميع الأعداد${\displaystyle n}$وبالتالي، فإن قاعدة الوسط المرفوع صحيحة. $${\displaystyle P(n)\lor \neg P(n).}$$ ثم بالحث في${\displaystyle m}$، $${\displaystyle \forall m.\ \neg {\big (}\forall (n<m).\neg P(n){\big )}\to \exists (b<m).P(b)}$$ كتابةً: للأرقام${\displaystyle n}$ضمن نطاق محدود يصل إلى${\displaystyle m}$إذا أمكن استبعاد عدم وجود حالة صحيحة، أي إذا أمكن استبعاد أنه لكل رقم، على سبيل المثال${\displaystyle n=a}$، الاقتراح المقابل${\displaystyle P(a)}$إذا كان من الممكن دائمًا دحض ذلك، فهذا يعني ضمناً وجود بعض${\displaystyle n=b}$من بين هؤلاء${\displaystyle n}$'s for which${\displaystyle P(b)}$يمكن إثبات ذلك.

كما هو الحال مع الأمثلة التي نوقشت سابقًا، يتطلب إثبات ذلك تفكيكًا في جانب المقدمات للحصول على قضايا بدون نفي. إذا تمت صياغة القضية على أنها تبدأ من${\displaystyle m=0}$إذن، فإن هذه الحالة الأولية تعطي بالفعل شكلاً من أشكال الانفجار من جملة فارغة $${\displaystyle \bot \to \exists (b<0).P(b).}$$ القضية التالية${\displaystyle m=1}$يوضح هذا النص كيفية حذف النفي المزدوج للمسند القابل للتقرير، $${\displaystyle \neg \neg P(0)\to P(0).}$$ ال${\displaystyle m=2}$قراءة الحالة $${\displaystyle \neg {\big (}\neg P(0)\land \neg P(1){\big )}\to {\big (}P(0)\lor P(1){\big )},}$$ وهو ما يعادل، كما سبق ذكره، ما يلي: $${\displaystyle \neg \neg {\big (}P(0)\lor P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}.}$$ كلاهما${\displaystyle m=0}$و${\displaystyle m=1}$تُعدّ هذه حالات أخرى من حالات حذف النفي المزدوج للمسند القابل للتقرير. بالطبع، عبارة${\displaystyle \exists (b<m).P(b)}$للثابت${\displaystyle m}$و${\displaystyle P}$قد يكون من الممكن إثبات ذلك بوسائل أخرى، باستخدام مبادئ المنطق الأدنى.

على سبيل المثال، فإن المخطط غير المحدود للمسندات العامة القابلة للتقرير ليس قابلاً للإثبات حدسياً حتى، انظر مبدأ ماركوف .

في هذا القسم، نذكر النظام الناتج عن حصر المنطق الأدنى في الاستلزام فقط. تعتمد حسابات البرمجة الوظيفية بشكل أساسي على رابط الاستلزام، انظر على سبيل المثال حساب الإنشاءات لإطار منطق المسند .

يمكن تعريف النظام من خلال القواعد المتسلسلة التالية : ^{[ 2 ] [ 3 ]}$${\displaystyle {\dfrac {}{\Gamma \cup \{A\}\vdash A}}{\mbox{ axiom}}}$$    ${\displaystyle {\dfrac {\Gamma \cup \{A\}\vdash B}{\Gamma \vdash A\to B}}{\mbox{ intro}}}$    ${\displaystyle {\dfrac {\Gamma \vdash A\to B~~~~~~~~~~\Delta \vdash A}{\Gamma \cup \Delta \vdash B}}{\mbox{ elim.}}}$

كل صيغة من صيغ هذا المنطق الأدنى المقيد تُقابل نوعًا في حساب لامدا ذي الأنواع البسيطة ، انظر تناظر كاري-هوارد . هذا الجزء الاستلزامي من المنطق الأدنى هو نفسه الجزء الاستلزامي الإيجابي من المنطق الحدسي ، وفي سياق نظرية الأنواع، يُشار إليه غالبًا باسم "المنطق الأدنى". ^{[ 4 ]}

سخافة${\displaystyle \bot }$لا يُستخدم هذا الأسلوب في الاستدلال الطبيعي فحسب ، بل يُستخدم أيضًا في الصياغات النظرية للأنواع في ظل نظرية كاري-هوارد. في أنظمة الأنواع،${\displaystyle \bot }$يُعرَّف هذا النوع غالبًا أيضًا بأنه النوع الفارغ. وبالتالي، فإن وجود برهان على هذه القضية يشكل تناقضًا.