الأنظمة الاستنتاجية الصورية

ما النظام الاستنتاجي الصوري

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

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

مخططات المسلّمات وحالاتها الخاصة

لا تذكر أنظمة منطق القضايا مسلّماتها واحدةً واحدة، لأنها غير منتهية، بل بواسطة مخططات: عبارات من اللغة الواصفة مكتوبة بمتغيرات واصفة، مثل $(\varphi \rightarrow (\psi \rightarrow \varphi))$. والمخطط ليس صيغة؛ إنه قالب. والحالة الخاصة من المخطط هي الصيغة الناتجة عن تعويض كل متغير واصف بصيغة تعويضًا منتظمًا: تُعوَّض جميع ورودات المتغير الواصف نفسه بالصيغة نفسها، وإن جاز أن تتلقى متغيرات واصفة مختلفة الصيغةَ نفسها أو صيغًا مختلفة.