نظرية البرهان الهيكلي

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

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

يأتي مصطلح "البنية" في نظرية البرهان البنيوي من مفهوم تقني تم تقديمه في حساب المتتاليات: يمثل حساب المتتاليات التأكيد الذي يتم إجراؤه في أي مرحلة من مراحل الاستدلال باستخدام عوامل تشغيل خاصة غير منطقية تسمى عوامل التشغيل البنيوية: في${\displaystyle A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}}$الفواصل الموجودة على يسار رمز البوابة الدوارة هي عوامل تُفسَّر عادةً على أنها روابط، والفواصل الموجودة على يمينه على أنها روابط فصل، بينما يُفسَّر رمز البوابة الدوارة نفسه على أنه استلزام. مع ذلك، من المهم ملاحظة وجود فرق جوهري في السلوك بين هذه العوامل والروابط المنطقية التي تُفسَّر بها في حساب التفاضل والتكامل اللاحق: تُستخدم العوامل البنيوية في كل قاعدة من قواعد الحساب، ولا تُؤخذ في الاعتبار عند تحديد ما إذا كانت خاصية الصيغة الفرعية تنطبق. علاوة على ذلك، فإن القواعد المنطقية أحادية الاتجاه: يُنشأ البناء المنطقي بواسطة القواعد المنطقية، ولا يمكن حذفه بعد إنشائه، بينما يمكن إدخال العوامل البنيوية وحذفها أثناء عملية الاشتقاق.

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

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

${\displaystyle {\frac {\Gamma \vdash \Delta ,A\quad A,\Pi \vdash \Sigma }{\Gamma ,\Pi \vdash \Delta ,\Sigma }}\quad ({\text{Cut}}),}$

أين،${\displaystyle \Gamma ,\Delta ,\Pi ,}$و${\displaystyle \Sigma }$هي عبارة عن سلاسل من الصيغ. صيغة القطع${\displaystyle A}$يُستخدم هذا الأسلوب بفعالية كشرط وسيط يُقدّم ثم يُحذف. تكمن أهمية حذف هذه القاعدة في أن البراهين الناتجة الخالية من القطع تتمتع بخاصية الصيغة الفرعية، التي تضمن أن كل صيغة تظهر في أي مكان في اشتقاق خالٍ من القطع هي صيغة فرعية لصيغة في المتتالية النهائية. لذلك، يكون البرهان تحليليًا بالكامل لأنه لا يتطلب إدخال أي مفاهيم خارجية، باستثناء تلك الموجودة بالفعل في العبارة المراد إثباتها. تُستخدم خاصية القطع هذه لإثبات اتساق المنطق الكلاسيكي والحدسي ، وتُستخدم أيضًا في دلالات نظرية البرهان .

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

يرتبط التناقض المنطقي والانسجام من خلال تناظرات حساب المتتاليات . بنية المتتالية،${\displaystyle \Gamma \vdash \Delta }$، أين${\displaystyle \Gamma ,\Delta }$تُشكّل المجموعات المتعددة المحدودة من الصيغ، وتُرسّخ ثنائية أساسية بين المقدمات (يسارًا) واللاحقات (يمينًا). وتتحقق هذه الثنائية بشكل صريح من خلال قواعد الإدخال اليسرى واليمنى لكل رابط منطقي. على سبيل المثال، قواعد الربط (${\displaystyle \land }$) والانفصال (${\displaystyle \lor }$) هي ثنائية:

${\displaystyle {\begin{array}{ccc}{\text{(}}{\land }{\text{L)}}&{\dfrac {A,B,\Gamma \vdash \Delta }{A\land B,\Gamma \vdash \Delta }}&{\text{(}}{\land }{\text{R)}}&{\dfrac {\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}{\Gamma \vdash \Delta ,A\land B}}\\\\{\text{(}}{\lor }{\text{L)}}&{\dfrac {A,\Gamma \vdash \Delta \qquad B,\Gamma \vdash \Delta }{A\lor B,\Gamma \vdash \Delta }}&{\text{(}}{\lor }{\text{R)}}&{\dfrac {\Gamma \vdash \Delta ,A,B}{\Gamma \vdash \Delta ,A\lor B}}\end{array}}}$

يعكس هذا التناظر بين اليمين واليسار انسجامًا أعمق بين المعنى النحوي للرابط، المحدد فقط بقواعد إدخاله، عبر مبدأ القلب، وسلوكه الحذفي. وتضمن نظرية الحذف القطعي هذا الانسجام النظري. قاعدة القطع، ${\displaystyle {\text{(Cut)}}\quad {\dfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Lambda }{\Gamma ,\Sigma \vdash \Delta ,\Lambda }},}$ يمثل هذا شكلاً من أشكال الربط الدلالي؛ وتُظهر مقبوليته أن نظام البرهان متسق داخليًا وتحليلي، أي أن البراهين لا تحتاج إلى الإشارة إلى مفاهيم خارجية، مثل الصيغة.${\displaystyle A}$، والتي لا تظهر في الاستنتاج. الاختزال الناجح لقطع على صيغة معقدة إلى قطع على صيغها الفرعية، عبر اختزالات الحالة الرئيسية بين القواعد اليسرى واليمنى، على سبيل المثال، اختزال قطع على${\displaystyle A\land B}$تم تقديمه من قبل كليهما (${\displaystyle \land }$R) و (${\displaystyle \land }$يمثل L التجسيد الحسابي للتوازن الأمثل بين إمكانية إدخال الرابط وإمكانية حذفه. وبالتالي، فإن حذف القطع يؤكد انسجام القواعد التشغيلية، مما يضمن اتساق النظام المنطقي وامتلاك براهينه لخصائص تطبيع جيدة.

بعض قواعد الاستدلال محلية ، وهي خاصية مرغوبة. ^{[ 3 ]} على سبيل المثال، لنأخذ  قاعدة ! في المنطق الخطي :$${\displaystyle {\frac {\vdash A,?B_{1},\dots ,?B_{n}}{\vdash !A,?B_{1},\dots ,?B_{n}}}}$$للتأكد من  تطبيق قاعدة ! بشكل صحيح على خطوة معينة من حساب التفاضل والتكامل التسلسلي${\displaystyle {\frac {\vdash A,B_{1},\dots ,B_{n}}{\vdash A',B_{1},\dots ,B_{n}}}}$ليس من الضروري فقط التحقق من ذلك${\displaystyle A'=?A}$ولكن من الضروري أيضًا التحقق من أن كل واحد من${\displaystyle B_{i}}$تحتوي على  علامة التعجب (!) كرابط منطقي خارجي. وبهذا المعنى، فإن القاعدة ليست محلية ، لأنه لتطبيقها، يجب التحقق من عدد غير محدود من الصيغ.

كمثال أكثر شيوعًا، في حساب التتابعات الكلاسيكي LK، تكون قواعد الاستدلال لـ OR هي$${\displaystyle {\frac {A,\Gamma \vdash \Delta \quad B,\Gamma \vdash \Delta }{A\lor B,\Gamma \vdash \Delta }}(\lor \vdash ),\quad {\frac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}(\vdash \lor _{1}),\quad {\frac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}(\vdash \lor _{2})}$$القاعدة${\displaystyle \lor \vdash }$ليس محليًا، لأنه من أجل التحقق من تطبيقه بشكل صحيح في خطوة ما$${\displaystyle {\frac {A,\Gamma \vdash \Delta \quad B,\Gamma '\vdash \Delta '}{C,\Gamma \vdash \Delta }}}$$يجب على المرء أن يتحقق ليس فقط من ذلك${\displaystyle C=A\lor B}$ولكن أيضاً ذلك${\displaystyle \Gamma =\Gamma ',\Delta =\Delta '}$القواعد${\displaystyle \vdash \lor _{1},\vdash \lor _{2}}$محليون. ^{[ 4 ]}

استُلهمت فكرة الموضعية في الأصل من اعتبارات البرمجة المنطقية المتوازية . وتتلخص الفكرة فيما يلي: سلسلة كبيرة${\displaystyle \Gamma \vdash \Delta }$قد تُخزَّن البيانات بطريقة موزعة، عبر عدة معالجات ومواقع ذاكرة متعددة. يمكن تنفيذ خطوة الاستدلال المحلي بكمية محدودة من التفاعل، بينما يمكن تنفيذ خطوات الاستدلال غير المحلي بكمية كبيرة من التفاعل. على سبيل المثال، تحديدًا، من أجل تنفيذ${\displaystyle {\frac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}}$يحتاج المعالج إلى إنتاج تسلسل جديد.${\displaystyle \Gamma '\vdash \Delta '}$بحيث${\displaystyle \Gamma '}$يشير ببساطة إلى نفس عنوان الذاكرة مثل${\displaystyle \Gamma }$، و${\displaystyle \Delta '}$يشير إلى${\displaystyle A\lor B}$، متبوعًا بعنوان الذاكرة الثاني لـ${\displaystyle B,\Delta }$على النقيض من ذلك، فإن تطبيق قاعدة ما${\displaystyle \lor \vdash }$يتطلب ذلك التحقق من تطابق سلسلتين، وهو ما يستغرق${\displaystyle O(n)}$العمليات، حيث${\displaystyle n}$يمثل عدد الصيغ في التسلسل.

يُوسّع إطار التسلسل الفائق بنية التسلسل العادي إلى مجموعة متعددة من التسلسلات، باستخدام رابط بنيوي إضافي | (يُسمى شريط التسلسل الفائق ) لفصل التسلسلات المختلفة. وقد استُخدم لتوفير حسابات تحليلية، على سبيل المثال، للمنطق الموجه ، والمنطق الوسيط ، والمنطق البنيوي الفرعي ^{[ 5 ] [ 6 ] [ 7 ].} التسلسل الفائق هو بنية

${\displaystyle \Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}$

حيث كل${\displaystyle \Gamma _{i}\vdash \Delta _{i}}$هي متتالية عادية، تُسمى مكونًا من المتتالية الفائقة. وكما هو الحال مع المتتاليات، يمكن أن تستند المتتاليات الفائقة إلى مجموعات، أو مجموعات متعددة، أو متتاليات، ويمكن أن تكون مكوناتها متتالية ذات نتيجة واحدة أو متعددة النتائج . يعتمد تفسير صيغة المتتاليات الفائقة على المنطق قيد الدراسة، ولكنه دائمًا تقريبًا شكل من أشكال الفصل. التفسيرات الأكثر شيوعًا هي الفصل البسيط.

${\displaystyle (\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

بالنسبة للمنطق الوسيط، أو كفصل للمربعات

${\displaystyle \Box (\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor \Box (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

للمنطق الموجه.

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

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma \vdash \Pi }}}$

وقاعدة الانكماش الخارجي

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}}}$

تُوفّر القواعد التي تُعالج بنية التسلسل الفائق مزيدًا من التعبيرية في إطار التسلسل الفائق. ومن الأمثلة المهمة على ذلك قاعدة التقسيم المشروط ^{[ 6 ].}

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma ,\Omega \vdash \Box \Pi ,\Theta }{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma \vdash \Box \Pi \mid \Omega \vdash \Theta }}}$

بالنسبة للمنطق الموجه S5 ، حيث${\displaystyle \Box \Sigma }$هذا يعني أن كل صيغة في${\displaystyle \Box \Sigma }$وهو على شكل${\displaystyle \Box A}$.

مثال آخر هو قاعدة الاتصال للمنطق الوسيط LC ^{[ 6 ]}

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Omega \vdash A\qquad \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Theta \vdash B}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Omega \vdash B\mid \Theta \vdash A}}}$

لاحظ أن مكونات قاعدة الاتصال هي متواليات ذات نتيجة واحدة.

حساب التفاضل والتكامل المتسلسل المتداخل هو صياغة رسمية تشبه حساب التفاضل والتكامل ثنائي الجوانب للهياكل .

• سارة نيغري ؛ يان فون بلاتو (2001). نظرية البرهان البنيوي . مطبعة جامعة كامبريدج. ISBN 978-0-521-79307-0.
• آن جيرب ترويلسترا ; هيلموت شويتنبرغ (2000). نظرية الإثبات الأساسية (  الطبعة الثانية). مطبعة جامعة كامبريدج. رقم ISBN 978-0-521-77911-1.