قائمة الأنظمة البديهية في المنطق

تحتوي هذه المقالة على قائمة بنماذج لأنظمة استنتاجية على نمط هيلبرت لمنطق القضايا .

أنظمة حساب القضايا الكلاسيكية

يُعدّ حساب القضايا الكلاسيكي المنطقَ الافتراضيّ القياسي. دلالاته المقصودة ثنائية ، وخاصيته الأساسية هي اكتماله التام ، أي أنه كلما استُنتجت صيغةٌ دلاليًا من مجموعة من المقدمات، فإنها تُستنتج أيضًا من تلك المجموعة نحويًا. وقد صِيغت العديد من أنظمة البديهيات الكاملة المتكافئة. وتختلف هذه الأنظمة في اختيار الروابط الأساسية المستخدمة، والتي يجب أن تكون في جميع الحالات كاملة وظيفيًا (أي قادرة على التعبير عن جميع جداول الحقيقة من الرتبة n بالتركيب )، وفي الاختيار الكامل الدقيق للبديهيات على أساس الروابط المختارة.

التضمين والنفي

تستخدم الصيغ هنا الاستلزام والنفي.{،¬}{\displaystyle \{\to ,\neg \}}باعتبارها مجموعة كاملة وظيفيًا من الروابط الأساسية. يتطلب كل نظام منطقي قاعدة استدلال واحدة على الأقل غير صفرية . يستخدم حساب القضايا الكلاسيكي عادةً قاعدة القياس المنطقي ( modus ponens ).

أ،أبب.{\displaystyle {\frac {A,A\to B}{B}}.}

نفترض أن هذه القاعدة مضمنة في جميع الأنظمة أدناه ما لم يُذكر خلاف ذلك.

نظام بديهيات فريجه : [ 1 ]

أ(بأ){\displaystyle A\to (B\to A)}
(أ(بج))((أب)(أج)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
(أ(بج))(ب(أج)){\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
(أب)(¬ب¬أ){\displaystyle (A\to B)\to (\neg B\to \neg A)}
¬¬أأ{\displaystyle \neg \neg A\to A}
أ¬¬أ{\displaystyle A\to \neg \neg A}

نظام بديهيات هيلبرت : [ 1 ]

أ(بأ){\displaystyle A\to (B\to A)}
(أ(بج))(ب(أج)){\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
(بج)((أب)(أج)){\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}
أ(¬أب){\displaystyle A\to (\neg A\to B)}
(أب)((¬أب)ب){\displaystyle (A\to B)\to ((\neg A\to B)\to B)}

الأنظمة البديهية لـ Łukasiewicz : [ 1 ]

  • أولاً:
    (أب)((بج)(أج)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
    (¬أأ)أ{\displaystyle (\neg A\to A)\to A}
    أ(¬أب){\displaystyle A\to (\neg A\to B)}
  • ثانية:
    ((أب)ج)(¬أج){\displaystyle ((A\to B)\to C)\to (\neg A\to C)}
    ((أب)ج)(بج){\displaystyle ((A\to B)\to C)\to (B\to C)}
    (¬أج)((بج)((أب)ج)){\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}
  • ثالث:
    أ(بأ){\displaystyle A\to (B\to A)}
    (أ(بج))((أب)(أج)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
    (¬أ¬ب)(بأ){\displaystyle (\neg A\to \neg B)\to (B\to A)}

نظام بديهيات أراي : [ 2 ]

(أب)((بج)(أج)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
أ(¬أب){\displaystyle A\to (\neg A\to B)}
(¬أب)((بأ)أ){\displaystyle (\neg A\to B)\to ((B\to A)\to A)}

النظام البديهي لوكاسيفيتش وتارسكي : [ 3 ]

[(أ(بأ))([(¬ج(د¬هـ))[(ج(دF))((هـد)(هـF))]]جي)](حجي){\displaystyle [(A\to (B\to A))\to ([(\neg C\to (D\to \neg E))\to [(C\to (D\to F))\to ((E\to D)\to (E\to F))]]\to G)]\to (H\to G)}

نظام بديهيات ميريديث :

((((أب)(¬ج¬د))ج)هـ)((هـأ)(دأ)){\displaystyle ((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))}

نظام بديهيات مندلسون : [ 4 ]

أ(بأ){\displaystyle A\to (B\to A)}
(أ(بج))((أب)(أج)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
(¬أ¬ب)((¬أب)أ){\displaystyle (\neg A\to \neg B)\to ((\neg A\to B)\to A)}

نظام بديهيات راسل : [ 1 ]

أ(بأ){\displaystyle A\to (B\to A)}
(أب)((بج)(أج)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
(أ(بج))(ب(أج)){\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
¬¬أأ{\displaystyle \neg \neg A\to A}
(أ¬أ)¬أ{\displaystyle (A\to \neg A)\to \neg A}
(أ¬ب)(ب¬أ){\displaystyle (A\to \neg B)\to (B\to \neg A)}

أنظمة بديهيات سوبوتشينسكي : [ 1 ]

  • أولاً:
    ¬أ(أب){\displaystyle \neg A\to (A\to B)}
    أ(ب(جأ)){\displaystyle A\to (B\to (C\to A))}
    (¬أج)((بج)((أب)ج)){\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}
  • ثانية:
    (أب)(¬ب(أج)){\displaystyle (A\to B)\to (\neg B\to (A\to C))}
    أ(ب(جأ)){\displaystyle A\to (B\to (C\to A))}
    (¬أب)((أب)ب){\displaystyle (\neg A\to B)\to ((A\to B)\to B)}

التضمين والزيف

بدلاً من النفي، يمكن أيضاً صياغة المنطق الكلاسيكي باستخدام المجموعة الكاملة وظيفياً{،}{\displaystyle \{\to ,\bot \}}من الروابط.

نظام تارسكي- بيرنايز - واجسبرج البديهي:

(أب)((بج)(أج)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
أ(بأ){\displaystyle A\to (B\to A)}
((أب)أ)أ{\displaystyle ((A\to B)\to A)\to A}[ 5 ]
أ{\displaystyle \bot \to A}

نظام بديهيات الكنيسة :

أ(بأ){\displaystyle A\to (B\to A)}
(أ(بج))((أب)(أج)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
((أ))أ{\displaystyle ((A\to \bot )\to \bot )\to A}

أنظمة بديهيات ميريديث:

  • أولاً: [ 6 ] [ 7 ] [ 8 ]
    ((((أب)(ج))د)هـ)((هـأ)(جأ)){\displaystyle ((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))}
  • ثانياً: [ 6 ]
    ((أب)((ج)د))((دأ)(هـ(Fأ))){\displaystyle ((A\to B)\to ((\bot \to C)\to D))\to ((D\to A)\to (E\to (F\to A)))}

النفي والفصل

بدلاً من الاستلزام، يمكن أيضاً صياغة المنطق الكلاسيكي باستخدام المجموعة الكاملة وظيفياً{¬،}{\displaystyle \{\neg ,\lor \}}من الروابط. تستخدم هذه الصيغ قاعدة الاستدلال التالية؛

أ،¬أبب.{\displaystyle {\frac {A,\neg A\lor B}{B}}.}

نظام بديهيات راسل-بيرنايز:

¬(¬بج)(¬(أب)(أج)){\displaystyle \neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))}
¬(أب)(بأ){\displaystyle \neg (A\lor B)\lor (B\lor A)}
¬أ(بأ){\displaystyle \neg A\lor (B\lor A)}
¬(أأ)أ{\displaystyle \neg (A\lor A)\lor A}

أنظمة بديهيات ميريديث: [ 9 ]

  • أولاً:
    ¬(¬(¬أب)(ج(دهـ)))(¬(¬دأ)(ج(هـأ))){\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg D\lor A)\lor (C\lor (E\lor A)))}
  • ثانية:
    ¬(¬(¬أب)(ج(دهـ)))(¬(¬هـد)(ج(أد))){\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg E\lor D)\lor (C\lor (A\lor D)))}
  • ثالث:
    ¬(¬(¬أب)(ج(دهـ)))(¬(¬جأ)(هـ(دأ))){\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg C\lor A)\lor (E\lor (D\lor A)))}

وبالمثل، يمكن تعريف المنطق الافتراضي الكلاسيكي باستخدام العطف والنفي فقط.

العطف والنفي

ابتكر روسر ج. باركلي نظامًا قائمًا على الربط والنفي.{،¬}{\displaystyle \{\wedge ,\neg \}}، مع استخدام قاعدة الاستدلال المنطقي (modus ponens) كقاعدة للاستدلال. في كتابه، [ 10 ] استخدم الاستلزام لعرض مخططات بديهياته.جد{\displaystyle C\rightarrow D}" هو اختصار لـ "¬(ج¬د){\displaystyle \neg (C\wedge \neg D)}":

  • أأأ{\displaystyle A\rightarrow A\wedge A}
  • أبأ{\displaystyle A\wedge B\rightarrow A}
  • (أب)(¬(بج)¬(جأ)){\displaystyle \left(A\rightarrow B\right)\rightarrow \left(\neg \left(B\wedge C\right)\rightarrow \neg \left(C\wedge A\right)\right)}

إذا لم نستخدم الاختصار، فسنحصل على مخططات البديهيات بالشكل التالي:

  • ¬(أ¬(أأ)){\displaystyle \neg (A\wedge \neg (A\wedge A))}
  • ¬((أب)¬أ){\displaystyle \neg ((A\wedge B)\wedge \neg A)}
  • ¬(¬(أ¬ب)¬¬(¬(بج)¬¬(جأ))){\displaystyle \neg \left(\neg \left(A\wedge \neg B\right)\wedge \neg \neg \left(\neg \left(B\wedge C\right)\wedge \neg \neg \left(C\wedge A\right)\right)\right)}

كذلك، يصبح مبدأ الاستدلال (modus ponens) كالتالي:

  • أ،¬(أ¬ب)ب{\displaystyle {\frac {A,\neg \left(A\wedge \neg B\right)}{B}}}

سكتة دماغية لشيفر

نظرًا لأن عملية شيفر (المعروفة أيضًا باسم عامل NAND) كاملة وظيفيًا ، فإنه يمكن استخدامها لإنشاء صياغة كاملة لحساب القضايا. تستخدم صياغات NAND قاعدة استدلال تسمى قاعدة نيكود للقياس المنطقي (modus ponens).

أ،أ|(ب|ج)ج.{\displaystyle {\frac {A,A\mid (B\mid C)}{C}}.}

نظام بديهيات نيكود: [ 6 ]

(أ|(ب|ج))|[(هـ|(هـ|هـ))|((د|ب)|[(أ|د)|(أ|د)])]{\displaystyle (A\mid (B\mid C))\mid [(E\mid (E\mid E))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}

الأنظمة البديهية لوكاسيفيتش: [ 6 ]

  • أولاً:
    (أ|(ب|ج))|[(د|(د|د))|((د|ب)|[(أ|د)|(أ|د)])]{\displaystyle (A\mid (B\mid C))\mid [(D\mid (D\mid D))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}
  • ثانية:
    (أ|(ب|ج))|[(أ|(ج|أ))|((د|ب)|[(أ|د)|(أ|د)])]{\displaystyle (A\mid (B\mid C))\mid [(A\mid (C\mid A))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}

نظام بديهيات واجسبرج: [ 6 ]

(أ|(ب|ج))|[((د|ج)|[(أ|د)|(أ|د)])|(أ|(أ|ب))]{\displaystyle (A\mid (B\mid C))\mid [((D\mid C)\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]}

أنظمة بديهيات أرجون : [ 6 ]

  • أولاً:
(أ|(ب|ج))|[(أ|(ب|ج))|((د|ج)|[(ج|د)|(أ|د)])]{\displaystyle (A\mid (B\mid C))\mid [(A\mid (B\mid C))\mid ((D\mid C)\mid [(C\mid D)\mid (A\mid D)])]}
  • ثانية:
(أ|(ب|ج))|[([(ب|د)|(أ|د)]|(د|ب))|((ج|ب)|أ)]{\displaystyle (A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]}[ 11 ]

كشف التحليل الحاسوبي الذي أجراه مختبر أرجون الوطني عن أكثر من 60 نظامًا إضافيًا من البديهيات الفردية التي يمكن استخدامها لصياغة حساب التفاضل والتكامل الافتراضي NAND. [ 8 ]

حساب القضايا الاستلزامي

حساب القضايا الاستلزامي هو جزء من حساب القضايا الكلاسيكي الذي لا يقبل سوى رابط الاستلزام. وهو ليس كاملاً وظيفياً (لأنه يفتقر إلى القدرة على التعبير عن الكذب والنفي)، ولكنه كامل نحوياً . تستخدم حسابات القضايا الاستلزامية أدناه قاعدة الاستدلال (modus ponens).

نظام بيرنيز-تارسكي البديهي: [ 12 ]

أ(بأ){\displaystyle A\to (B\to A)}
(أب)((بج)(أج)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
((أب)أ)أ{\displaystyle ((A\to B)\to A)\to A}

أنظمة Łukasiewicz و Tarski البديهية:

  • أولاً: [ 12 ]
    [(أ(بأ))[([((جد)هـ)F][(دF)(جF)])جي]]جي{\displaystyle [(A\to (B\to A))\to [([((C\to D)\to E)\to F]\to [(D\to F)\to (C\to F)])\to G]]\to G}
  • ثانياً: [ 12 ]
    [(أب)((جد)هـ)]([F((جد)هـ)][(أF)(دهـ)]){\displaystyle [(A\to B)\to ((C\to D)\to E)]\to ([F\to ((C\to D)\to E)]\to [(A\to F)\to (D\to E)])}
  • ثالث:
    ((أب)(جد))(هـ((دأ)(جأ))){\displaystyle ((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))}
  • رابعاً:
    ((أب)(جد))((دأ)(هـ(جأ))){\displaystyle ((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))}

النظام البديهي لوكاسيفيتش: [ 13 ] [ 12 ]

((أب)ج)((جأ)(دأ)){\displaystyle ((A\to B)\to C)\to ((C\to A)\to (D\to A))}

المنطق الحدسي والمنطق الوسيط

المنطق الحدسي هو نظام فرعي من المنطق الكلاسيكي. ويتم صياغته عادةً باستخدام{،،،}{\displaystyle \{\to ,\land ,\lor ,\bot \}}باعتبارها مجموعة الروابط الأساسية (الكاملة وظيفيًا). وهي ليست كاملة نحويًا لافتقارها إلى الوسط المرفوع A∨¬A أو قانون بيرس ((A→B)→A)→A، اللذين يمكن إضافتهما دون إحداث تناقض منطقي. وتعتمد على قاعدة الاستدلال الشرطي (modus ponens)، بالإضافة إلى البديهيات التالية:

أ(بأ){\displaystyle A\to (B\to A)}
(أ(بج))((أب)(أج)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
(أب)أ{\displaystyle (A\land B)\to A}
(أب)ب{\displaystyle (A\land B)\to B}
أ(ب(أب)){\displaystyle A\to (B\to (A\land B))}
أ(أب){\displaystyle A\to (A\lor B)}
ب(أب){\displaystyle B\to (A\lor B)}
(أج)((بج)((أب)ج)){\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}
أ{\displaystyle \bot \to A}

بدلاً من ذلك، يمكن وضع بديهيات المنطق الحدسي باستخدام{،،،¬}{\displaystyle \{\to ,\land ,\lor ,\neg \}}باعتبارها مجموعة الروابط الأساسية، استبدل البديهية الأخيرة بـ

(أ¬أ)¬أ{\displaystyle (A\to \neg A)\to \neg A}
¬أ(أب){\displaystyle \neg A\to (A\to B)}

المنطق الوسيط يقع بين المنطق الحدسي والمنطق الكلاسيكي. فيما يلي بعض أنواع المنطق الوسيط:

  • منطق جانكوف (KC) هو امتداد للمنطق الحدسي، والذي يمكن وضع بديهياته بواسطة نظام البديهيات الحدسية بالإضافة إلى البديهية [ 14 ].
¬أ¬¬أ.{\displaystyle \neg A\lor \neg \neg A.}
  • يمكن وضع بديهيات منطق غودل-دوميت (LC) على المنطق الحدسي عن طريق إضافة البديهية [ 14 ].
(أب)(بأ).{\displaystyle (A\to B)\lor (B\to A).}

حساب التفاضل والتكامل الضمني الإيجابي

الحساب الاستدلالي الإيجابي هو الجزء الاستدلالي من المنطق الحدسي. وتستخدم الحسابات أدناه قاعدة الاستدلال (modus ponens).

نظام بديهيات لوكاسيفيتش:

أ(بأ){\displaystyle A\to (B\to A)}
(أ(بج))((أب)(أج)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}

أنظمة بديهيات ميريديث:

  • أولاً:
    هـ((أب)(((دأ)(بج))(أج))){\displaystyle E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))}
  • ثانية:
    أ(بأ){\displaystyle A\to (B\to A)}
    (أب)((أ(بج))(أج)){\displaystyle (A\to B)\to ((A\to (B\to C))\to (A\to C))}
  • ثالث:
    ((أب)ج)(د((ب(جهـ))(بهـ))){\displaystyle ((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))}[ 15 ]

أنظمة بديهيات هيلبرت:

  • أولاً:
    (أ(أب))(أب){\displaystyle (A\to (A\to B))\to (A\to B)}
    (بج)((أب)(أج)){\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}
    (أ(بج))(ب(أج)){\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
    أ(بأ){\displaystyle A\to (B\to A)}
  • ثانية:
    (أ(أب))(أب){\displaystyle (A\to (A\to B))\to (A\to B)}
    (أب)((بج)(أج)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
    أ(بأ){\displaystyle A\to (B\to A)}
  • ثالث:
    أأ{\displaystyle A\to A}
    (أب)((بج)(أج)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
    (بج)((أب)(أج)){\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}
    (أ(أب))(أب){\displaystyle (A\to (A\to B))\to (A\to B)}

حساب القضايا الإيجابي

حساب القضايا الإيجابي هو جزء من المنطق الحدسي الذي يستخدم فقط الروابط (غير الكاملة وظيفيًا).{،،}{\displaystyle \{\to ,\land ,\lor \}}يمكن وضع بديهيات لها باستخدام أي من الحسابات المذكورة أعلاه لحسابات الاستلزام الموجب بالإضافة إلى البديهيات

(أب)أ{\displaystyle (A\land B)\to A}
(أب)ب{\displaystyle (A\land B)\to B}
أ(ب(أب)){\displaystyle A\to (B\to (A\land B))}
أ(أب){\displaystyle A\to (A\lor B)}
ب(أب){\displaystyle B\to (A\lor B)}
(أج)((بج)((أب)ج)){\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}

ويمكننا أيضاً، إن رغبنا، أن نُضمّن الرابط{\displaystyle \leftrightarrow }والمسلمات

(أب)(أب){\displaystyle (A\leftrightarrow B)\to (A\to B)}
(أب)(بأ){\displaystyle (A\leftrightarrow B)\to (B\to A)}
(أب)((بأ)(أب)){\displaystyle (A\to B)\to ((B\to A)\to (A\leftrightarrow B))}

يمكن صياغة منطق يوهانسون الأدنى باستخدام أي من أنظمة البديهيات الخاصة بحساب القضايا الإيجابية، وتوسيع لغته باستخدام الرابط الصفري .{\displaystyle \bot }بدون مخططات بديهية إضافية. أو بدلاً من ذلك، يمكن أيضًا وضع بديهيات لها في اللغة{،،،¬}{\displaystyle \{\to ,\land ,\lor ,\neg \}}عن طريق توسيع حساب القضايا الإيجابية باستخدام البديهية

(أ¬ب)(ب¬أ){\displaystyle (A\to \neg B)\to (B\to \neg A)}

أو زوج البديهيات

(أب)(¬ب¬أ){\displaystyle (A\to B)\to (\neg B\to \neg A)}
أ¬¬أ{\displaystyle A\to \neg \neg A}

يمكن صياغة المنطق الحدسي في اللغة التي تحتوي على النفي على أساس بديهي في حساب التفاضل والتكامل الإيجابي بواسطة زوج من البديهيات

(أ¬ب)(ب¬أ){\displaystyle (A\to \neg B)\to (B\to \neg A)}
¬أ(أب){\displaystyle \neg A\to (A\to B)}

أو زوج البديهيات [ 16 ]

(أ¬أ)¬أ{\displaystyle (A\to \neg A)\to \neg A}
¬أ(أب){\displaystyle \neg A\to (A\to B)}

المنطق الكلاسيكي في اللغة{،،،¬}{\displaystyle \{\to ,\land ,\lor ,\neg \}}يمكن الحصول على ذلك من حساب القضايا الموجبة عن طريق إضافة البديهية

(¬أ¬ب)(بأ){\displaystyle (\neg A\to \neg B)\to (B\to A)}

أو زوج البديهيات

(أ¬ب)(ب¬أ){\displaystyle (A\to \neg B)\to (B\to \neg A)}
¬¬أأ{\displaystyle \neg \neg A\to A}

يأخذ حساب فيتش أيًا من أنظمة البديهيات لحساب القضايا الإيجابية ويضيف البديهيات [ 16 ].

¬أ(أب){\displaystyle \neg A\to (A\to B)}
أ¬¬أ{\displaystyle A\leftrightarrow \neg \neg A}
¬(أب)(¬أ¬ب){\displaystyle \neg (A\lor B)\leftrightarrow (\neg A\land \neg B)}
¬(أب)(¬أ¬ب){\displaystyle \neg (A\land B)\leftrightarrow (\neg A\lor \neg B)}

لاحظ أن البديهيتين الأولى والثالثة صحيحتان أيضاً في المنطق الحدسي.

حساب التفاضل والتكامل المكافئ

حساب التكافؤ هو نظام فرعي من حساب القضايا الكلاسيكي الذي يسمح فقط برابطة التكافؤ (غير المكتملة وظيفيًا) ، المشار إليها هنا بـ{\displaystyle \equiv }. قاعدة الاستدلال المستخدمة في هذه الأنظمة هي كما يلي:

أ،أبب.{\displaystyle {\frac {A,A\equiv B}{B}}.}

نظام بديهيات إيسيكي: [ 17 ]

((أج)(بأ))(جب){\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}
(أ(بج))((أب)ج){\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}

نظام بديهية إيسيكي – أراي: [ 18 ]

أأ{\displaystyle A\equiv A}
(أب)(بأ){\displaystyle (A\equiv B)\equiv (B\equiv A)}
(أب)((بج)(أج)){\displaystyle (A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))}

أنظمة بديهيات أراي؛

  • أولاً:
    (أ(بج))((أب)ج){\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}
    ((أج)(بأ))(جب){\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}
  • ثانية:
    (أب)(بأ){\displaystyle (A\equiv B)\equiv (B\equiv A)}
    ((أج)(بأ))(جب){\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}

أنظمة Łukasiewicz البديهية: [ 19 ]

  • أولاً:
    (أب)((جب)(أج)){\displaystyle (A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))}
  • ثانية:
    (أب)((أج)(جب)){\displaystyle (A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))}
  • ثالث:
    (أب)((جأ)(بج)){\displaystyle (A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))}

أنظمة بديهيات ميريديث: [ 19 ]

  • أولاً:
    ((أب)ج)(ب(جأ)){\displaystyle ((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))}
  • ثانية:
    أ((ب(أج))(جب)){\displaystyle A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))}
  • ثالث:
    (أ(بج))(ج(أب)){\displaystyle (A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))}
  • رابعاً:
    (أب)(ج((بج)أ)){\displaystyle (A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))}
  • خامساً:
    (أب)(ج((جب)أ)){\displaystyle (A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))}
  • السادس:
    ((أ(بج))ج)(بأ){\displaystyle ((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)}
  • السابع:
    ((أ(بج))ب)(جأ){\displaystyle ((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)}

نظام بديهيات كالمان : [ 19 ]

أ((ب(جأ))(جب)){\displaystyle A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))}

أنظمة وينكر البديهية: [ 19 ]

  • أولاً:
    أ((بج)((أج)ب)){\displaystyle A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))}
  • ثانية:
    أ((بج)((جأ)ب)){\displaystyle A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))}

نظام بديهيات XCB: [ 19 ]

أ(((أب)(جب))ج){\displaystyle A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)}

انظر أيضاً

مراجع

  1. 1 2 3 4 5 ياسويوكي إيماي، كيوشي إيسيكي، حول أنظمة البديهيات في حسابات القضايا، الجزء الأول، وقائع الأكاديمية اليابانية. المجلد 41، العدد 6 (1965)، 436 439.
  2. يوشيناري أراي، حول أنظمة البديهيات في حسابات القضايا، الجزء الثاني، وقائع الأكاديمية اليابانية. المجلد 41، العدد 6 (1965)، 440 442.
  3. الجزء الثالث عشر: شوتارو تاناكا. حول أنظمة البديهيات لحسابات القضايا، الجزء الثالث عشر. وقائع الأكاديمية اليابانية، المجلد 41، العدد 10 (1965)، 904 907.
  4. إليوت مندلسون، مقدمة في المنطق الرياضي ، فان نوستراند، نيويورك، 1979، ص 31.
  5. قانون بيرس
  6. 1 2 3 4 5 6 [فيتلسون، 2001] "صياغات بديهية جديدة أنيقة لبعض منطق الجمل" بقلم براندن فيتلسون
  7. (كشف التحليل الحاسوبي الذي أجراه مختبر أرجون أن هذا هو أقصر بديهية مفردة بأقل عدد من المتغيرات لحساب القضايا).
  8. 1 2 "بعض النتائج الجديدة في الحسابات المنطقية التي تم الحصول عليها باستخدام الاستدلال الآلي"، زاك إرنست، وكين هاريس، وبراندن فيتلسون، http://www.mcs.anl.gov/research/projects/AR/award-2001/fitelson.pdf
  9. C. Meredith, Single axioms for the systems (C, N), (C, 0) and (A, N) of the two-valued propositional calculus , Journal of Computing Systems, pp. 155–164, 1954.
  10. روسر ج. باركلي، "المنطق للرياضيين"، نيويورك، ماكجرو هيل، 1953.
  11. ، ص 9، طيف تطبيقات الاستدلال الآلي ، لاري ووس؛ arXiv:cs/0205078v1
  12. 1 2 3 4 تحقيقات في حساب الجمل في المنطق، والدلالات، وما وراء الرياضيات: أوراق بحثية من عام 1923 إلى عام 1938 بقلم ألفريد تارسكي ، كوركوران، ج.، تحرير هاكيت. الطبعة الأولى حررها وترجمها جيه إتش وودجر، مطبعة جامعة أكسفورد. (1956)
  13. لوكاسيفيتش، يان (1948). "أقصر بديهية في حساب الاستلزام للقضايا" . وقائع الأكاديمية الملكية الأيرلندية. القسم أ: العلوم الرياضية والفيزيائية . 52 : 25-33 . ISSN 0035-8975 . JSTOR 20488489 .  
  14. 1 2 أ. تشاغروف، م. زاخارياشيف، المنطق الموجه ، مطبعة جامعة أكسفورد، 1997.
  15. C. Meredith, A single axiom of positive logic , Journal of Computing Systems, p. 169–170, 1954.
  16. 1 2 L. H. Hackstaff, Systems of Formal Logic , Springer, 1966.
  17. كيوشي إيسيكي، حول أنظمة البديهيات في حسابات القضايا، المجلد الخامس عشر، وقائع الأكاديمية اليابانية. المجلد 42، العدد 3 (1966)، 217-220 .
  18. يوشيناري أراي، حول أنظمة البديهيات في حسابات القضايا، المجلد السابع عشر، وقائع الأكاديمية اليابانية. المجلد 42، العدد 4 (1966)، 351 354.
  19. 1 2 3 4 5 XCB، آخر البديهيات الفردية الأقصر لحساب التفاضل والتكامل الكلاسيكي ، لاري ووس، دولف أولريش، براندن فيتلسون؛ arXiv:cs/0211015v1