نظرية الحذف بالقطع

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

نظرية حذف القطع هي نظرية تتعلق بأشجار البرهان. و"إثبات نظرية حذف القطع" يعني كتابة حجة برهان لهذه النظرية.

عادةً ما يكون برهان نظرية حذف القطع كما يلي.

يسرد جميع قواعد الاستدلال لحساب المتتاليات. شجرة البرهان هي شجرة يمثل كل عقدة فيها تطبيقًا لقاعدة استدلال.

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

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

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

لإثبات أن النظام ينتهي، عادةً ما يتم تصميم نظام ترقيم ترتيبي . لكل شجرة إثبات${\displaystyle T}$حدد رقمًا ترتيبيًا مطابقًا${\displaystyle o(T)}$ثم يوضح أن كل خطوة من خطوات إعادة الكتابة${\displaystyle T\implies T'}$لديه${\displaystyle o(T)>o(T')}$ثم، بما أن الأعداد الترتيبية لها أساس متين، فإن نظام إعادة الكتابة كذلك.

يؤدي هذا المنطق أيضًا إلى التحليل الترتيبي . أي أنه لإثبات أن النظام سينتهي، يجب افتراض أن$${\displaystyle \sup _{T{\text{ is a proof tree}}}o(T)}$$منظم بشكل جيد. على سبيل المثال، في حالة برهان جنتزن الأصلي، أثبت أن$${\displaystyle \sup _{T{\text{ is a proof tree}}}o(T)=\epsilon _{0}}$$العدد إبسيلون الصفري . وعلى العكس، يمكن لحسابات بيانو إثبات أي عدد ترتيبي أقل من${\displaystyle \epsilon _{0}}$له أساس متين، ولكن ليس${\displaystyle \epsilon _{0}}$لذا فإن القول الشائع هو أن "اتساق حسابات بيانو يعادل سلامة أسسها".${\displaystyle \epsilon _{0}}$".

يوجد بشكل عام نوعان من قواعد إعادة الكتابة:

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

لنأخذ في الاعتبار حساب المتتاليات النموذجي لـ LK الافتراضي. نحن نشترط أن تكون المتتاليات مجموعات متعددة منتهية ، حتى نتمكن من تجاهل الإزعاج البيروقراطي لقاعدة التبادل.

قاعدة القطع هي$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad A,\Pi \vdash \Lambda }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} .}$$نقدم خمسة أمثلة توضيحية. تجدر الإشارة إلى أننا نستخدم صيغًا "مضاعفة" لقواعد الاستدلال الخاصة بالربط والفصل، لأنها أكثر ملاءمة لحذف القطع.

الاقتران، التسلسل الأيسر، التبديل$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad {\frac {A,B,C,\Pi \vdash \Lambda }{A,B\land C,\Pi \vdash \Lambda }}\land _{L}}{\Gamma ,B\land C,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} \quad \implies \quad {\frac {{\frac {\Gamma \vdash \Delta ,A\qquad A,B,C,\Pi \vdash \Lambda }{\Gamma ,B,C,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} }{\Gamma ,B\land C,\Pi \vdash \Delta ,\Lambda }}\land _{L}.}$$القطع ببساطة يتحرك خطوة واحدة إلى الأمام${\displaystyle \land _{L}}$بدون تفاعل. ستتصاعد حتى تواجه "مقاومة" على شكل فواصل رئيسية.

الفصل، التسلسل الأيسر، التبديل$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad {\frac {A,B,\Pi \vdash \Lambda \qquad C,\Sigma \vdash \Theta }{A,B\lor C,\Pi ,\Sigma \vdash \Lambda ,\Theta }}\lor _{L}}{\Gamma ,B\lor C,\Pi ,\Sigma \vdash \Delta ,\Lambda ,\Theta }}\operatorname {Cut} \quad \implies \quad {\frac {{\frac {\Gamma \vdash \Delta ,A\qquad A,B,\Pi \vdash \Lambda }{\Gamma ,B,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} \qquad C,\Sigma \vdash \Theta }{\Gamma ,B\lor C,\Pi ,\Sigma \vdash \Delta ,\Lambda ,\Theta }}\lor _{L}.}$$لقد تحرك القطع خطوة واحدة للأعلى، متجاوزًا${\displaystyle \lor _{L}}$.

بديهية الهوية، القاعدة الرئيسية$${\displaystyle {\frac {{\overline {A\vdash A}}^{\operatorname {Id} }\qquad A,\Pi \vdash \Lambda }{A,\Pi \vdash \Lambda }}\operatorname {Cut} \quad \implies \quad A,\Pi \vdash \Lambda .}$$هكذا قد تختفي بعض الجروح في نهاية المطاف، عن طريق إلغاء ورقة من شجرة البرهان.

قاعدة الإضعاف، والتسلسل اليساري، والقاعدة الرئيسية$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad {\frac {\Pi \vdash \Lambda }{A,\Pi \vdash \Lambda }}\operatorname {Weak} _{L}}{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} \quad \implies \quad {\frac {\Pi \vdash \Lambda }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Weak} ^{*}.}$$هنا${\displaystyle \operatorname {Weak} ^{*}}$يشير إلى عدد محدود من تطبيقات التضعيف الأيسر والأيمن. صيغة القطع${\displaystyle A}$يتم إدخالها عن طريق إضعاف المقدمة الصحيحة، بحيث يحدث حدوث${\displaystyle A}$غير مستخدم. يتم تجاهل المقدمة اليسرى، ويتم استعادة النتيجة النهائية الأصلية من${\displaystyle \Pi \vdash \Lambda }$عن طريق الإضعاف.

الانكماش، القاعدة الرئيسية$${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad {\frac {A,A,\Pi \vdash \Lambda }{A,\Pi \vdash \Lambda }}\operatorname {Contr} _{L}}{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} \quad \implies \quad {\frac {{\frac {\Gamma \vdash \Delta ,A\qquad {\frac {\Gamma \vdash \Delta ,A\qquad A,A,\Pi \vdash \Lambda }{\Gamma ,A,\Pi \vdash \Delta ,\Lambda }}\operatorname {Cut} }{\Gamma ,\Gamma ,\Pi \vdash \Delta ,\Delta ,\Lambda }}\operatorname {Cut} }{\Gamma ,\Pi \vdash \Delta ,\Lambda }}\operatorname {Contr} ^{*}.}$$ هنا${\displaystyle \operatorname {Contr} ^{*}}$يشير إلى عدد محدود من تطبيقات الانكماش الأيسر والأيمن. وقد حدد الانكماش في المقدمة اليمنى حالتين من صيغة القطع.${\displaystyle A}$. تبدأ عملية إعادة الصياغة بحذف أحد مواضع ظهور كلمة${\displaystyle A}$ثم يقطع مقابل الظهور الآخر لـ${\displaystyle A}$تُحدد الاختصارات النهائية النسخ المكررة من${\displaystyle \Gamma }$و${\displaystyle \Delta }$.

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

بسبب قاعدة مبدأ الانكماش، يؤدي حذف القطع إلى زيادة حجم البرهان بشكل كبير جدًا. وفقًا لتطابق كاري-هوارد ، يتوافق حذف القطع مع اختزال بيتا لمصطلحات لامدا ذات النوع البسيط . إعادة الكتابة تتوافق مع اختزال بيتا. إعادة الكتابة عبر قاعدة انكماش تتوافق مع اختزال بيتا للشكل${\displaystyle (\lambda fx.f(fx))t}$، وانخفاض بيتا$${\displaystyle \underbrace {(\lambda fx.f(fx))\cdots (\lambda fx.f(fx))} _{n{\text{ times}}}}$$قد يستغرق الأمر${\displaystyle ^{n}2}$الزمن، حيث يكون الترميز هو التكرار .

تتضمن قواعد التحديد الكمي اختزالات رئيسية مماثلة، مع الشرط المعتاد المتمثل في إعادة تسمية المتغيرات الذاتية دائمًا قبل إعادة الكتابة، لتجنب الالتقاط العرضي. على سبيل المثال، القطع الرئيسي بين${\displaystyle \forall _{R}}$و${\displaystyle \forall _{L}}$يتم تبسيطها باستبدال المصطلح المستخدم في القاعدة اليسرى في برهان المتغيرات الذاتية من القاعدة اليمنى، ثم القطع على الحالة الناتجة. وبالتالي، تحافظ خطوة إعادة الكتابة على المتتالية النهائية مع استبدال القطع على${\displaystyle \forall x\,A(x)}$عن طريق قطع في حالة${\displaystyle A(t)}$.