قاعدة القطع

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

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

تُكتب قاعدة القطع عادةً في الترميز الرسمي في حساب المتتابعات على النحو التالي  :

${\displaystyle {\begin{array}{c}\Gamma \vdash A,\Delta \quad \Gamma ',A\vdash \Delta '\\\hline \Gamma ,\Gamma '\vdash \Delta ,\Delta '\end{array}}}$قطع ^{[ 1 ]}

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