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

بعد هذا، ما يلي الآن هو مراجعة الطريقة التي ترتبط بها تعبيرات المنطق الاقتراحي ببعضها البعض لتشكيل استنتاج. الآلية التي يتم من خلالها بناء هذه العلاقات هي النظام الاستنتاجي الرسمي.

ما هو النظام الاستنتاجي الرسمي؟

الأنظمة الاستنتاجية الرسمية، أو أنظمة الحساب الاستنتاجي، لها ثلاثة مكونات أساسية:

1. لغة رسمية.
2. مخطط أكسيوماتي.
3. قواعد استنتاج أولية.

لقد راجعنا بالفعل كل ما يتعلق باللغات الرسمية. الآن دورنا لنقدم مخططات الأكسيومات وقواعد الاستنتاج الأولية.

لبناء نظام استنتاج الحساب الاقتراحي سنبدأ بتجميع النظام الاستنتاجي انطلاقًا من أكسيومات Łukasiewicz, وكقاعدة استنتاج أولية سنستخدم المودس بوننس.

أكسيومات Łukasiewicz للمنطق الاقتراحي

إذا كان \alpha, \beta و \gamma تعبيرات في حساب المقترحات، فإن الآتي هو أكسيومات حساب المقترحات:

المودس بوننس: المحرك الاستنتاجي لحساب المقترحات

إذا كانت \alpha و \beta تعبيرات صالحة في حساب المقترحات، ينص المودس بوننس على أنه من \alpha و (\alpha \rightarrow \beta) يتم استنتاج \beta. يتم كتابة هذا الاستدلال على النحو التالي:

هنا تم اختصار تمثيل المودس بوننس بين الخطوات (1) و (2) من خلال الكتابة “MP(1,2)”، ويتم تمثيل خلاصة كل هذا من خلال التدوين التالي:

لذلك \{\alpha, (\alpha \rightarrow \beta)\}\vdash \beta

سنرى قريبًا أنه يمكن بناء جميع تقنيات الاستنتاج في حساب المقترحات من أكسيومات Łukasiewicz والمودس بوننس، والتي تجمع قواعد الاستدلال الأساسية للتفكير العادي وتشكل الأساس لـ المنطق الكلاسيكي.

الاستدلالات والنظريات والفروض

في أنظمة الاستنتاج للمنطق الاقتراحي يتم تنفيذ الاستدلالات (أو الاستنتاجات)، وهذه هي أي تتابع للتعبيرات حيث كل منها إما فرضية أو تعبير مستحصل من الفروض باستخدام فقط أكسيومات Łukasiewicz والمودس بوننس. نظرية هي نتيجة استنتاج بدون فروض. الفرضية يمكن أن تكون أي تعبير ليس أكسيوماً ولا يتم استنتاجه منها. بشكل عام، عندما يكون لدينا مجموعة من الفروض \Gamma وتعبير \alpha يتم الحصول عليه باستخدام بعض عناصر \Gamma والأكسيومات والمودس بوننس، نكتب “\Gamma \vdash \alpha” ونقول أن

من \Gamma يتم استنتاج \alpha

إذا كان \Gamma مجموعة فارغة، فبدلاً من كتابة “\emptyset\vdash \alpha” نكتب “ \vdash \alpha .” وهذا يُقرأ “\alpha هي نظرية”. يمكن توسيع هذه الطريقة في تمثيل النظريات لتمثيل الأكسيومات بحيث إذا كانت \alpha و \beta و \gamma تعبيرات، فإن أكسيومات Łukasiewicz يمكن كتابتها على النحو التالي

ومن هذا يقال إن الأكسيومات هي بيانات واضحة بحد ذاتها، أو أن النظريات هي تعبيرات يتم استنتاجها من فراغ، أو أن الأكسيومات والنظريات هي خصائص لحساب المقترحات.

كيف يتم تنفيذ دليل في المنطق الاقتراحي؟

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

نظرية

إذا كانت \alpha تعبيرًا في المنطق الاقتراحي، فإنه يتم الوفاء بما يلي

\vdash (\alpha\rightarrow \alpha)

برهان

لذلك \vdash (\alpha\rightarrow\alpha)

نهاية البرهان.

كما يمكن رؤية ذلك، في الأنظمة الاستنتاجية والمنطق الاقتراحي، البراهين ليست بسيطة، ولكن بمجرد أن يتم بناؤها تصبح سهلة التكرار.

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

مفهوم التكافؤ المثبت

إذا كانت \alpha و \beta تعبيرات مختلفة ويتحقق في نفس الوقت أن \{\alpha\}\vdash \beta و \{\beta\} \vdash \alpha، فإنه يقال إن \alpha و \beta متكافئتان مثبتتان ويكتب \alpha \dashv \vdash \beta. ويمكن تلخيص هذا رمزياً كالآتي:

\left(\{\alpha\}\vdash\beta \wedge \{\beta\}\vdash\alpha \right) \Leftrightarrow \left(\alpha\dashv\vdash\beta\right)

وهذا يُقرأ: من \alpha يُستنتج \beta، ومن \beta يُستنتج \alpha إذا وفقط إذا كانت \alpha و \beta متكافئتين مثبتتين.

هذه خاصية أساسية في المنطق الاقتراحي

الميتا-نظرية الاستدلال

إذا كانت \alpha و \beta تعبيرات في حساب المقترحات، و \Gamma مجموعة من الفروض؛ فإنه يُقال إذا من \Gamma \cup \{\alpha\} يتم استنتاج \beta، فإنه من \Gamma يُستنتج (\alpha \rightarrow \beta). ويمكن التعبير عن هذا رمزياً كالتالي:

\left(\Gamma \cup \{\alpha\}\vdash \beta \right) \Rightarrow \left( \Gamma\vdash(\alpha\rightarrow\beta)\right)

برهان:

لكي يتحقق \Gamma \cup \{\alpha\}\vdash \beta، من الضروري أن يكون هناك استنتاج على النحو التالي:

لذلك \Gamma\cup\{\alpha\} \vdash \beta

لكي يكون هذا ممكناً، من الضروري أن تكون واحدة على الأقل من التعبيرات \gamma_1, \cdots \gamma_n,\overline{\gamma_1},\cdots,\overline{\gamma_m} على شكل (\alpha\rightarrow \beta)، ولكن كل هذه الأسطر تتضمن فقط عناصر من \Gamma وأكسيومات Łukasiewicz في استنتاجها، لذا يجب أن يتحقق \Gamma\vdash (\alpha \rightarrow \beta). وبالتالي يثبت النظرية

نهاية البرهان.

المقابل لنظرية الاستدلال

في نفس الشروط الموضوعة لنظرية الاستدلال، سيكون لدينا ما يلي

\left(\Gamma\vdash(\alpha \rightarrow \beta)\right) \Rightarrow \left( \Gamma \cup \{\alpha\}\vdash \beta \right)

برهان:

إذا تحقق \Gamma\vdash (\alpha\rightarrow \beta)، فسيكون لدينا استنتاج بالشكل التالي

الآن، إذا أضفنا \alpha كفرضية إلى هذا الاستدلال، فسيكون لدينا السطور التالية

لذلك \Gamma \cup \{\alpha\} \vdash \beta

وهذا ما كنا نرغب في إثباته.

نهاية البرهان.

الاستدلالات حول التعبيرات والاستدلالات حول الاستدلالات

البراهين مثل التي تم إجراؤها سابقًا للوصول إلى النتيجة \vdash (\alpha\rightarrow \alpha) هي حالات للاستدلالات المبنية على التعبيرات، لأن كل خطوة تحتوي على تعبير محدد. بطريقة مماثلة، من الممكن إجراء استدلالات مبنية على استدلالات أخرى، حيث يكون كل خطوة استدلالًا في حد ذاته. في الواقع، كلا الأمرين يتم إجراؤهما بطريقة مماثلة، لكن الثاني يتيح لنا استخدام نظرية الاستدلال ونظيرتها، مما يمنح مرونة كبيرة لتقنية التفكير. لنرى ذلك، دعونا نثبت مرة أخرى أن \vdash (\alpha \rightarrow \alpha)، ولكن الآن باستخدام الاستدلالات بدلاً من التعبيرات. بديل لذلك هو التالي:

لاحظ أن هذا الاستدلال ليس أقصر من الذي قمنا به سابقًا، لكنه أسهل بكثير للقيام به، حيث استخدمنا فقط نظرية الاستدلال ونظيرتها والنظام الأكسيومي A1 لبناء البرهان.

في الظاهر، في التطوير الذي قمنا به للتو استخدمنا أكسيوما واحدًا من Łukasiewicz وتجاهلنا الأكسيومات الأخرى والمودس بوننس. هل يعني ذلك أننا بتفكيرنا بهذه الطريقة نتجاهل الأكسيومات الأخرى والمودس بوننس؟ الإجابة نعم ولا. من ناحية، يمكننا التظاهر بأننا نتجاهل بعض الأكسيومات والمودس بوننس لأننا لا نستخدمها بشكل صريح، ولكن يجب أن نتذكر أن كلًا من نظرية الاستدلال ونظيرتها هي نتيجة لأكسيومات Łukasiewicz والمودس بوننس، مما يعني أن استخدامها، كما فعلنا في الاستدلال الذي رأينا للتو، يعتبر استخدامًا ضمنيًا لها.

قاعدة التماثل

إذا كان \tau نظرية، فسيكون لدينا أنه، بالنظر إلى أي تعبير \beta، سيتحقق ما يلي

\{\beta\}\vdash\tau

هذه في الحقيقة قاعدة سهلة جدًا للإثبات، حيث أن \tau كونها نظرية، سيتحقق أن \vdash \tau. أي أنه يوجد استدلال لا يحتاج إلى إضافة فروض للوصول إلى التعبير \tau، لذا إضافة تعبير إضافي إلى الفروض (الفارغة) لن يخلق فرقًا.

بطريقة مماثلة لهذا يمكن طرح النتيجة التالية: إذا من مجموعة فروض \Gamma يتم استنتاج \gamma، فسيتحقق ما يلي

\Gamma\cup\{\alpha\}\vdash\gamma

حيث أن \alpha هو تعبير أيًا كان.

تركيب وتأملات حول الأنظمة الاستنتاجية والمنطق الاقتراحي

عندما نمنح لغة المنطق الاقتراحي قاعدة استنتاج وتعبيرات أساسية: المودس بوننس وأكسيومات Łukasiewicz، ما نقوم به يشبه بناء “آلة استنتاجية” و”محرك يزودها بالطاقة للدخول في الحركة”. من هنا تبدأ جميع القواعد الأساسية للاستنتاج في الظهور بشكل طبيعي والتي سنبدأ في مراجعتها في المشاركات التي تلي هذه مباشرةً.

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