قابلية الحسم (المنطق)

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

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

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

لا يمكن حسم منطق الرتبة الأولى بشكل عام؛ وعلى وجه الخصوص، فإن مجموعة الصلاحيات المنطقية في أي توقيع يتضمن المساواة ورمز مسند واحد على الأقل ذي وسيطين أو أكثر لا يمكن حسمها. ^{[ 1 ]} كما أن الأنظمة المنطقية التي توسع منطق الرتبة الأولى، مثل منطق الرتبة الثانية ونظرية الأنواع ، غير قابلة للحسم أيضاً.

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

لا يمكن تمثيل بعض الأنظمة المنطقية بشكل كافٍ بمجموعة النظريات وحدها. (على سبيل المثال، لا يحتوي منطق كلين على أي نظريات على الإطلاق). في مثل هذه الحالات، تُستخدم غالبًا تعريفات بديلة لقابلية الحسم لنظام منطقي، والتي تتطلب طريقة فعالة لتحديد شيء أكثر عمومية من مجرد صحة الصيغ؛ على سبيل المثال، صحة المتتاليات ، أو علاقة النتيجة {(Г, A ) | Г ⊧ A } للمنطق.

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

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

تُسمى النظرية المتسقة التي تتميز بأن كل امتداد متسق لها غير قابل للتقرير، نظرية غير قابلة للتقرير جوهريًا . في الواقع، كل امتداد متسق سيكون غير قابل للتقرير جوهريًا. نظرية الحقول غير قابلة للتقرير، ولكنها ليست غير قابلة للتقرير جوهريًا. من المعروف أن حساب روبنسون غير قابل للتقرير جوهريًا، وبالتالي فإن كل نظرية متسقة تتضمن حساب روبنسون أو تفسره هي أيضًا غير قابلة للتقرير (جوهريًا).

تشمل أمثلة النظريات القابلة للتقرير من الدرجة الأولى نظرية الحقول المغلقة الحقيقية ، وحساب بريسبرغر ، في حين أن نظرية المجموعات وحساب روبنسون هما مثالان على النظريات غير القابلة للتقرير.

تتضمن بعض النظريات القابلة للتقرير (مونك 1976، ص  234): ^{[ 2 ]}

• مجموعة من الصلاحيات المنطقية من الدرجة الأولى في التوقيع مع المساواة فقط، والتي وضعها ليوبولد لوفنهايم في عام 1915.
• مجموعة من الصلاحيات المنطقية من الدرجة الأولى في توقيع مع المساواة ووظيفة أحادية واحدة، والتي وضعها إهرنفويشت في عام 1959.
• نظرية الرتبة الأولى للأعداد الطبيعية في الإشارة مع المساواة والجمع، وتُسمى أيضاً حساب بريسبورغر . وقد أثبت اكتمالها موجزيس بريسبورغر في عام 1929.
• نظرية الرتبة الأولى للأعداد الطبيعية في التوقيع مع المساواة والضرب، وتسمى أيضًا حساب سكوليم .
• نظرية الجبر البولياني من الدرجة الأولى ، التي وضعها ألفريد تارسكي في عام 1940 (تم اكتشافها في عام 1940 ولكن تم الإعلان عنها في عام 1949).
• نظرية الرتبة الأولى للحقول المغلقة جبريًا ذات خاصية معينة ، والتي وضعها تارسكي في عام 1949.
• نظرية الرتبة الأولى للحقول المرتبة المغلقة الحقيقية ، التي وضعها تارسكي في عام 1949 (انظر أيضًا مسألة الدالة الأسية لتارسكي ).
• نظرية الدرجة الأولى للهندسة الإقليدية ، التي وضعها تارسكي في عام 1949.
• نظرية الرتبة الأولى للمجموعات الأبيلية ، التي وضعها شميليف في عام 1955.
• نظرية الدرجة الأولى للهندسة الزائدية ، التي وضعها شوابهاوزر في عام 1959.
• اللغات الفرعية القابلة للتقرير المحددة لنظرية المجموعات التي تم بحثها في ثمانينيات القرن العشرين وحتى اليوم. (كانتون وآخرون ، 2001)
• النظرية الأحادية من الدرجة الثانية للأشجار (انظر S2S ).

تشمل الطرق المستخدمة لتحديد قابلية الحسم إزالة الكميات ، واكتمال النموذج ، واختبار Łoś–Vaught .

تتضمن بعض النظريات غير القابلة للحسم ما يلي: ^{[ 2 ]}

• مجموعة الصحة المنطقية في أي توقيع من الدرجة الأولى مع المساواة و إما: رمز مسند من رتبة لا تقل عن 2، أو رمزان وظيفيان أحاديان، أو رمز وظيفي واحد من رتبة لا تقل عن 2، والتي وضعها تراختنبروت في عام 1953.
• نظرية الرتبة الأولى للأعداد الطبيعية مع الجمع والضرب والمساواة، التي وضعها تارسكي وأندريه موستوفسكي في عام 1949.
• نظرية الرتبة الأولى للأعداد النسبية مع الجمع والضرب والمساواة، التي وضعتها جوليا روبنسون في عام 1949.
• نظرية الزمر من الرتبة الأولى ، التي وضعها ألفريد تارسكي عام ١٩٥٣. ^{[ ٣ ]} والجدير بالذكر أن نظرية الزمر العامة ليست الوحيدة غير القابلة للتقرير، بل إن العديد من النظريات الأكثر تحديدًا غير قابلة للتقرير أيضًا، على سبيل المثال (كما أثبت مالسيف عام ١٩٦١) نظرية الزمر المنتهية . كما أثبت مالسيف أن نظرية أنصاف الزمر ونظرية الحلقات غير قابلتين للتقرير. وأثبت روبنسون عام ١٩٤٩ أن نظرية الحقول غير قابلة للتقرير.
• إن حساب روبنسون (وبالتالي أي امتداد متسق، مثل حساب بيانو ) غير قابل للتقرير بشكل أساسي، كما أثبت ذلك رافائيل روبنسون في عام 1950.
• نظرية الرتبة الأولى مع المساواة ورمزين للدالة. ^{[ 4 ]}

تُستخدم طريقة قابلية التفسير غالبًا لإثبات عدم قابلية الحسم للنظريات. فإذا كانت نظرية T غير قابلة للحسم جوهريًا قابلة للتفسير في نظرية متسقة S ، فإن S تكون أيضًا غير قابلة للحسم جوهريًا. ويرتبط هذا ارتباطًا وثيقًا بمفهوم الاختزال المتعدد-الواحد في نظرية الحوسبة .

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

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

لا ينبغي الخلط بين قابلية الحسم والاكتمال . على سبيل المثال، نظرية الحقول المغلقة جبريًا قابلة للحسم ولكنها غير مكتملة، بينما مجموعة جميع العبارات الصحيحة من الدرجة الأولى حول الأعداد الطبيعية في اللغة التي تحتوي على + و × مكتملة ولكنها غير قابلة للحسم. وللأسف، وبسبب الغموض المصطلحي، يُستخدم مصطلح "عبارة غير قابلة للحسم" أحيانًا كمرادف لعبارة مستقلة .

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

تم تصنيف بعض الألعاب وفقًا لقابليتها للحسم:

• يمكن تحديد كش مات في n من القطع في الشطرنج اللانهائي (مع مراعاة القيود المفروضة على القواعد وقطع اللعب). ^{[ 5 ] [ 6 ]} ومع ذلك، توجد أوضاع (بعدد محدود من القطع) تُعتبر فيها الفوز حتميًا، ولكنها لا تُحقق كش مات في n لأي قيمة محدودة لـ n . ^{[ 7 ]}
• بعض ألعاب الفرق التي تتضمن معلومات غير كاملة على لوحة محدودة (ولكن بوقت غير محدود) تكون غير قابلة للحسم. ^{[ 8 ]}

• مشكلة اتخاذ القرار
• التحديد الكمي الوجودي