حساب التفاضل والتكامل المتسلسل

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

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

• أسلوب هيلبرت . كل سطر هو تكرار غير مشروط (أو نظرية).
• أسلوب جينتزن. كل سطر عبارة عن تكرار شرطي (أو نظرية) مع عدم وجود أي شرط أو أكثر على اليسار.
  • الاستدلال الطبيعي . كل سطر (شرطي) يحتوي على قضية واحدة مؤكدة على اليمين.
  • حساب التفاضل والتكامل المتسلسل. كل سطر (شرطي) يحتوي على صفر أو أكثر من القضايا المؤكدة على اليمين.

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

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

في نظرية الإثبات والمنطق الرياضي ، حساب التفاضل والتكامل المتسلسل هو عائلة من الأنظمة الرسمية التي تشترك في أسلوب معين من الاستدلال وخصائص رسمية معينة. تم تقديم أول أنظمة حساب التفاضل والتكامل المتتالية، LK و LJ ، في عامي 1934/1935 بواسطة جيرهارد جينتزن ^[1] كأداة لدراسة الاستنتاج الطبيعي في المنطق من الدرجة الأولى (في الإصدارات الكلاسيكية والحدسية ، على التوالي). كانت ما يسمى بـ "النظرية الرئيسية" لجينتزن حول LK وLJ هي نظرية القطع والحذف ، [ ^{2] [3]} وهي نتيجة ذات عواقب نظرية بعيدة المدى ، بما في ذلك الاتساق . أظهر جينتزن قوة ومرونة هذه التقنية بعد بضع سنوات، حيث طبق حجة القطع والحذف لإعطاء دليل (ما وراء المحدود) على اتساق حساب بيانو ، في استجابة مفاجئة لنظريات عدم الاكتمال لغودل . منذ هذا العمل المبكر، تم تطبيق الحسابات المتسلسلة، والتي تسمى أيضًا أنظمة جينتزن ، ^{[4] [5] [6] [7]} والمفاهيم العامة المتعلقة بها، على نطاق واسع في مجالات نظرية الإثبات، والمنطق الرياضي، والاستنتاج الآلي .

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

${\displaystyle B}$

أين توجد أي صيغة للمنطق من الدرجة الأولى (أو أي منطق ينطبق عليه نظام الاستنتاج، على سبيل المثال ، حساب القضايا أو المنطق من الدرجة الأعلى أو المنطق النمطي ). النظريات هي تلك الصيغ التي تظهر كحكم ختامي في إثبات صحيح. لا يحتاج نظام على غرار هيلبرت إلى التمييز بين الصيغ والأحكام؛ فنحن نصنع واحدة هنا فقط للمقارنة مع الحالات التالية. ${\displaystyle B}$

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

في الاستدلال الطبيعي، تكون الأحكام على شكل

${\displaystyle A_{1},A_{2},\ldots ,A_{n}\vdash B}$

حيث أن s و هي مرة أخرى صيغ و . بعبارة أخرى، يتكون الحكم من قائمة (ربما فارغة) من الصيغ على الجانب الأيسر من رمز الباب الدوار " "، مع صيغة واحدة على الجانب الأيمن، ^{[8] [9] [10]} (على الرغم من أن تبديلات s غالبًا ما تكون غير مهمة). النظريات هي تلك الصيغ التي (مع جانب أيسر فارغ) هي استنتاج لإثبات صالح. (في بعض عروض الاستنباط الطبيعي، لا يتم كتابة s و الباب الدوار صراحةً؛ بدلاً من ذلك يتم استخدام تدوين ثنائي الأبعاد يمكن استنتاجهما منه.) ${\displaystyle A_{i}}$${\displaystyle B}$${\displaystyle n\geq 0}$${\displaystyle \vdash }$${\displaystyle A_{i}}$${\displaystyle B}$${\displaystyle \vdash ب}$${\displaystyle A_{i}}$

الدلالات القياسية للحكم في الاستنباط الطبيعي هي أنه يؤكد أنه كلما كانت ^[11] و و وما إلى ذلك، كلها صحيحة، فسوف تكون صحيحة أيضًا. الأحكام ${\displaystyle A_{1}}$${\displaystyle A_{2}}$${\displaystyle B}$

${\displaystyle A_{1},\ldots ,A_{n}\vdash B}$

و

${\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow B}$

متكافئان بالمعنى القوي الذي يجعل إثبات أحدهما يمكن أن يمتد إلى إثبات الآخر.

أخيرًا، يعمم حساب التفاضل والتكامل المتسلسل شكل حكم الاستنتاج الطبيعي إلى

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}$

كائن نحوي يسمى متتالي. تسمى الصيغ الموجودة على الجانب الأيسر من الباب الدوار بالمقدمة ، وتسمى الصيغ الموجودة على الجانب الأيمن بالمتتالية أو اللاحقة ؛ ويطلق عليهما معًا المتتاليات أو المتتاليات . ^[12] مرة أخرى، و هي صيغ، و و أعداد صحيحة غير سالبة، أي أن الجانب الأيسر أو الجانب الأيمن (أو لا شيء أو كلاهما) قد يكون فارغًا. كما هو الحال في الاستنتاج الطبيعي، فإن النظريات هي تلك حيث هي استنتاج لإثبات صحيح. ${\displaystyle A_{i}}$${\displaystyle B_{i}}$${\displaystyle n}$${\displaystyle k}$${\displaystyle B}$${\displaystyle \vdash B}$

الدلالات القياسية للتسلسل هي تأكيد على أنه كلما كان كل شيء صحيحًا، فسيكون واحد على الأقل صحيحًا أيضًا. ^[13] وبالتالي فإن التسلسل الفارغ، الذي يكون فيه كل من المقدمات فارغًا، يكون خاطئًا. ^[14] إحدى الطرق للتعبير عن هذا هي أن الفاصلة الموجودة على يسار البوابة الدوارة يجب أن يُنظر إليها على أنها "و"، والفاصلة الموجودة على يمين البوابة الدوارة يجب أن يُنظر إليها على أنها "أو" (شاملة). التسلسلات ${\displaystyle A_{i}}$ ${\displaystyle B_{i}}$

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}}$

و

${\displaystyle \vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})}$

متكافئان بالمعنى القوي الذي يمكن من خلاله تمديد إثبات أي من المتتاليتين إلى إثبات المتتالية الأخرى.

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

${\displaystyle \vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}}$

(على الأقل أحد الـ A خاطئ، أو أحد الـ B صحيح)

أو كما

${\displaystyle \vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})}$

(لا يمكن أن تكون جميع الـ A صحيحة وجميع الـ B خاطئة).

في هذه الصياغات، الفرق الوحيد بين الصيغ على جانبي البوابة الدوارة هو أن أحد الجانبين منفي. وبالتالي، فإن تبديل اليسار باليمين في متتالية يتوافق مع نفي جميع الصيغ المكونة. وهذا يعني أن التناظر مثل قوانين دي مورجان ، والذي يتجلى كنفي منطقي على المستوى الدلالي، يترجم مباشرة إلى تناظر يسار-يمين للمتتاليات - والواقع أن قواعد الاستدلال في حساب المتتاليات للتعامل مع الاقتران (∧) هي صور طبق الأصل لتلك التي تتعامل مع الانفصال (∨).

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

أكد جينتزن على التمييز الحاد بين أنظمة الاستنتاج الطبيعي ذات المخرج الواحد (NK و NJ) وأنظمة حساب التفاضل والتكامل المتتالية متعددة المخرجات (LK و LJ). وكتب أن نظام الاستنتاج الطبيعي الحدسي NJ كان قبيحًا إلى حد ما. ^[15] وقال إن الدور الخاص للوسط المستبعد في نظام الاستنتاج الطبيعي الكلاسيكي NK قد تمت إزالته في نظام حساب التفاضل والتكامل المتتالي الكلاسيكي LK. ^[16] وقال إن حساب التفاضل والتكامل المتتالي LJ أعطى تناسقًا أكبر من الاستنتاج الطبيعي NJ في حالة المنطق الحدسي، كما هو الحال أيضًا في حالة المنطق الكلاسيكي (LK مقابل NK). ^[17] ثم قال إنه بالإضافة إلى هذه الأسباب، فإن حساب التفاضل والتكامل المتتالي مع صيغ المتتالية المتعددة مخصص بشكل خاص لنظريته الرئيسية ("Hauptsatz"). ^[18]

كلمة "sequent" مأخوذة من كلمة "Sequenz" في ورقة جينتزن عام 1934. ^{[1] يعلق} كليين على الترجمة إلى الإنجليزية على النحو التالي: "يقول جينتزن "Sequenz"، والتي نترجمها إلى "sequent"، لأننا استخدمنا بالفعل "sequence" لأي تتابع للأشياء، حيث أن الكلمة الألمانية هي "Folge". ^[19]

يمكن اعتبار حساب التفاضل والتكامل المتسلسل أداة لإثبات الصيغ في المنطق القياسي ، على غرار طريقة الجداول التحليلية . فهو يعطي سلسلة من الخطوات التي تسمح للمرء بتقليل مشكلة إثبات صيغة منطقية إلى صيغ أبسط وأبسط حتى يصل إلى صيغ تافهة. ^[20]

خذ بعين الاعتبار الصيغة التالية:

${\displaystyle ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}$

يتم كتابة هذا بالشكل التالي، حيث تكون القضية التي يجب إثباتها على يمين رمز الباب الدوار : ${\displaystyle \vdash }$

${\displaystyle \vdash ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)}$

والآن، بدلاً من إثبات ذلك من البديهيات، يكفي أن نفترض مقدمة الاستدلال ثم نحاول إثبات نتيجته. ^[21] ومن ثم ننتقل إلى التسلسل التالي:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r}$

مرة أخرى، يتضمن الجانب الأيمن استنتاجًا، يمكن افتراض مقدمته بشكل أكبر بحيث لا يلزم إثبات سوى استنتاجه:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r),(p\land q)\vdash r}$

نظرًا لأن الحجج الموجودة في الجانب الأيسر من المفترض أن تكون مرتبطة بواسطة أداة الربط ، فيمكن استبدال ذلك بما يلي:

${\displaystyle (p\rightarrow r)\lor (q\rightarrow r),p,q\vdash r}$

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

${\displaystyle p\rightarrow r,p,q\vdash r}$

${\displaystyle q\rightarrow r,p,q\vdash r}$

في حالة الحكم الأول، نعيد كتابة الأمر كما يلي ونقسم التسلسل مرة أخرى للحصول على: ${\displaystyle p\rightarrow r}$${\displaystyle \lnot p\lor r}$

${\displaystyle \lnot p,p,q\vdash r}$

${\displaystyle r,p,q\vdash r}$

تم الانتهاء من التسلسل الثاني؛ ويمكن تبسيط التسلسل الأول إلى:

${\displaystyle p,q\vdash p,r}$

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

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

فيما يلي القواعد التي يتم بها التعامل مع الشجرة. كلما تم تقسيم أحد المتتاليات إلى اثنين، فإن رأس الشجرة يحتوي على رأسين فرعيين، وتتفرع الشجرة. بالإضافة إلى ذلك، يمكن للمرء تغيير ترتيب الحجج في كل جانب بحرية؛ تمثل Γ وΔ الحجج الإضافية المحتملة. ^[20]

المصطلح المعتاد للخط الأفقي المستخدم في تخطيطات نمط جينتزن للاستنتاج الطبيعي هو خط الاستدلال . ^[23]

غادر	يمين
${\displaystyle L\land {\text{rule: }}\quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}}$	${\displaystyle R\land {\text{rule: }}{\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}}$
${\displaystyle L\lor {\text{rule: }}{\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}}$	${\displaystyle R\lor {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}}$
${\displaystyle L\rightarrow {\text{rule: }}{\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}}$	${\displaystyle R\rightarrow {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}}$
${\displaystyle L\lnot {\text{rule: }}\quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}}$	${\displaystyle R\lnot {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}}$
البديهية: ${\displaystyle \Gamma ,A\vdash \Delta ,A}$

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

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

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

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

يقدم هذا القسم قواعد حساب المتتاليات LK (اختصارًا لـ Logistische Kalkül) كما قدمها جينتزن في عام 1934. ^[24] الدليل (الشكلي) في هذا الحساب هو تسلسل من المتتاليات، حيث يمكن اشتقاق كل من المتتاليات من المتتاليات التي تظهر في وقت سابق في المتتالية باستخدام إحدى القواعد أدناه .

سيتم استخدام التدوين التالي:

• ${\displaystyle \vdash }$تُعرف باسم الباب الدوار ، وهي تفصل الافتراضات الموجودة على اليسار عن المقترحات الموجودة على اليمين
• ${\displaystyle A}$وتشير إلى صيغ منطق المسند من الدرجة الأولى (قد يقتصر هذا أيضًا على المنطق القياسي)،${\displaystyle B}$
• ${\displaystyle \Gamma ,\Delta ,\Sigma }$، وهي عبارة عن تسلسلات محدودة (ربما فارغة) من الصيغ (في الواقع، لا يهم ترتيب الصيغ؛ انظر § القواعد البنيوية)، تسمى السياقات، ${\displaystyle \Pi }$
  • عندما يكون على يسار ، يتم اعتبار تسلسل الصيغ متصلاً (يُفترض أن تكون جميعها صحيحة في نفس الوقت)،${\displaystyle \vdash }$
  • بينما على يمين ، يتم اعتبار تسلسل الصيغ منفصلًا (يجب أن تكون إحدى الصيغ على الأقل صالحة لأي تعيين للمتغيرات)،${\displaystyle \vdash }$
• ${\displaystyle t}$يشير إلى مصطلح تعسفي،
• ${\displaystyle x}$وتشير إلى المتغيرات.${\displaystyle y}$
• يقال أن المتغير يحدث حرًا داخل صيغة إذا لم يكن مرتبطًا بمقادير أو .${\displaystyle \forall }$${\displaystyle \exists }$
• ${\displaystyle A[t/x]}$يشير إلى الصيغة التي تم الحصول عليها عن طريق استبدال المصطلح لكل حدوث حر للمتغير في الصيغة مع القيد الذي ينص على أن المصطلح يجب أن يكون حرًا للمتغير في (أي عدم حدوث أي متغير في يصبح مقيدًا في ).${\displaystyle t}$${\displaystyle x}$${\displaystyle A}$${\displaystyle t}$${\displaystyle x}$${\displaystyle A}$${\displaystyle t}$${\displaystyle A[t/x]}$
• ${\displaystyle WL}$, , , , , : تمثل هذه الستة نسختين من كل قاعدة من القواعد البنيوية الثلاث؛ واحدة للاستخدام على يسار ('L') من a ، والأخرى على يمينها ('R'). يتم اختصار القواعد إلى 'W' للإضعاف (يسار/يمين) ، و'C' للانكماش ، و'P' للتبديل .${\displaystyle WR}$${\displaystyle CL}$${\displaystyle CR}$${\displaystyle PL}$${\displaystyle PR}$${\displaystyle \vdash }$

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

البديهية	يقطع
${\displaystyle {\cfrac {\qquad }{A\vdash A}}\quad (I)}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})}$

القواعد المنطقية اليسرى	القواعد المنطقية الصحيحة
${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})}$
${\displaystyle {\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})}$	${\displaystyle {\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})}$
${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\lor B\vdash \Delta }}\quad ({\lor }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Gamma \vdash B,\Delta }{\Gamma \vdash A\land B,\Delta }}\quad ({\land }R)}$
${\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)}$	${\displaystyle {\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)}$
${\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)}$	${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)}$
${\displaystyle {\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)}$
${\displaystyle {\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)}$	${\displaystyle {\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)}$

القواعد الهيكلية اليسرى	القواعد البنيوية الصحيحة
${\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})}$
${\displaystyle {\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})}$	${\displaystyle {\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})}$
${\displaystyle {\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})}$	${\displaystyle {\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})}$

القيود: في القواعد و ، يجب ألا يظهر المتغير حراً في أي مكان في التسلسلات السفلية المعنية.${\displaystyle ({\forall }R)}$${\displaystyle ({\exists }L)}$${\displaystyle y}$

يمكن تقسيم القواعد المذكورة أعلاه إلى مجموعتين رئيسيتين: قواعد منطقية وقواعد بنيوية . تقدم كل قاعدة منطقية صيغة منطقية جديدة إما على يسار أو يمين البوابة الدوارة . وعلى النقيض من ذلك، تعمل القواعد البنيوية على بنية المتتاليات، متجاهلة الشكل الدقيق للصيغ. الاستثناءان لهذا المخطط العام هما بديهية الهوية (I) وقاعدة (Cut). ${\displaystyle \vdash }$

على الرغم من صياغتها بطريقة رسمية، فإن القواعد المذكورة أعلاه تسمح بقراءة بديهية للغاية من حيث المنطق الكلاسيكي. فكر، على سبيل المثال، في القاعدة . تنص على أنه كلما تمكن المرء من إثبات أنه يمكن استنتاج ذلك من بعض تسلسل الصيغ التي تحتوي على ، فيمكنه أيضًا الاستنتاج من الافتراض (الأقوى) الذي ينطبق. وبالمثل، تنص القاعدة على أنه إذا كان و كافيًا لاستنتاج ، فمن وحده يمكننا إما أن نستنتج أو يجب أن يكون خاطئًا، أي ينطبق. يمكن تفسير جميع القواعد بهذه الطريقة. ${\displaystyle ({\land }L_{1})}$${\displaystyle \Delta }$${\displaystyle A}$${\displaystyle \Delta }$${\displaystyle A\land B}$${\displaystyle ({\neg }R)}$${\displaystyle \Gamma }$${\displaystyle A}$${\displaystyle \Delta }$${\displaystyle \Gamma }$${\displaystyle \Delta }$${\displaystyle A}$${\displaystyle {\neg }A}$

للحصول على فكرة عن قواعد الكم، ضع في اعتبارك القاعدة . بالطبع، لا يمكن عمومًا استنتاج أن القاعدة صحيحة فقط من حقيقة أن القاعدة صحيحة. ومع ذلك، إذا لم يتم ذكر المتغير y في مكان آخر (أي أنه لا يزال من الممكن اختياره بحرية، دون التأثير على الصيغ الأخرى)، فيمكن للمرء أن يفترض أن القاعدة صحيحة لأي قيمة لـ y. وبالتالي، يجب أن تكون القواعد الأخرى واضحة تمامًا. ${\displaystyle ({\forall }R)}$${\displaystyle \forall {x}A}$${\displaystyle A[y/x]}$${\displaystyle A[y/x]}$

بدلاً من النظر إلى القواعد كأوصاف للاستنتاجات القانونية في منطق المسند، يمكن للمرء أيضًا اعتبارها تعليمات لبناء دليل لبيان معين. في هذه الحالة، يمكن قراءة القواعد من الأسفل إلى الأعلى؛ على سبيل المثال، يقول أنه لإثبات أن يتبع من الافتراضات و ، يكفي إثبات أنه يمكن استنتاجه من ويمكن استنتاجه من ، على التوالي. لاحظ أنه، نظرًا لبعض المقدمات، ليس من الواضح كيف يمكن تقسيمها إلى و . ومع ذلك، لا يوجد سوى عدد محدود من الاحتمالات التي يجب التحقق منها لأن المقدم بالافتراض محدود. يوضح هذا أيضًا كيف يمكن النظر إلى نظرية الإثبات على أنها تعمل على البراهين بطريقة تركيبية: مع الأخذ في الاعتبار البراهين لكل من و ، يمكن للمرء بناء دليل لـ . ${\displaystyle ({\land }R)}$${\displaystyle A\land B}$${\displaystyle \Gamma }$${\displaystyle \Sigma }$${\displaystyle A}$${\displaystyle \Gamma }$${\displaystyle B}$${\displaystyle \Sigma }$${\displaystyle \Gamma }$${\displaystyle \Sigma }$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\land B}$

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

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

لاحظ أن جميع القواعد لها رفاق متطابقون، باستثناء القواعد الخاصة بالاستدلال. وهذا يعكس حقيقة مفادها أن اللغة المعتادة للمنطق من الدرجة الأولى لا تتضمن رابط "لا يُستدل عليه" الذي قد يكون ثنائي الاستدلال الذي وضعه دي مورجان. وإضافة مثل هذا الرابط مع قواعده الطبيعية من شأنه أن يجعل حساب التفاضل والتكامل متماثلاً تماماً من اليسار إلى اليمين. ${\displaystyle \not \leftarrow }$

وهذا هو اشتقاق " "، المعروف باسم قانون الأوسط المستبعد ( tertium non datur في اللاتينية). ${\displaystyle \vdash A\lor \lnot A}$

		${\displaystyle (I)}$
${\displaystyle A\vdash A}$
		${\displaystyle (\lnot R)}$
${\displaystyle \vdash \lnot A,A}$
		${\displaystyle (\lor R_{2})}$
${\displaystyle \vdash A\lor \lnot A,A}$
		${\displaystyle (PR)}$
${\displaystyle \vdash A,A\lor \lnot A}$
		${\displaystyle (\lor R_{1})}$
${\displaystyle \vdash A\lor \lnot A,A\lor \lnot A}$
		${\displaystyle (CR)}$
${\displaystyle \vdash A\lor \lnot A}$

التالي هو إثبات حقيقة بسيطة تتضمن محددات كمية. لاحظ أن العكس ليس صحيحًا، ويمكن رؤية زيفه عند محاولة استنتاجه من الأسفل إلى الأعلى، لأنه لا يمكن استخدام متغير حر موجود في الاستبدال في القواعد و . ${\displaystyle (\forall R)}$${\displaystyle (\exists L)}$

		${\displaystyle (I)}$
${\displaystyle p(x,y)\vdash p(x,y)}$
		${\displaystyle (\forall L)}$
${\displaystyle \forall x\left(p(x,y)\right)\vdash p(x,y)}$
		${\displaystyle (\exists R)}$
${\displaystyle \forall x\left(p(x,y)\right)\vdash \exists y\left(p(x,y)\right)}$
		${\displaystyle (\exists L)}$
${\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \exists y\left(p(x,y)\right)}$
		${\displaystyle (\forall R)}$
${\displaystyle \exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \forall x\left(\exists y\left(p(x,y)\right)\right)}$

ولإثبات أمر أكثر إثارة للاهتمام ، سنجد أنه من السهل العثور على الاشتقاق، الذي يوضح فائدة LK في الإثبات الآلي. ${\displaystyle {\left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}}$

${\displaystyle (I)}$ ${\displaystyle A\vdash A}$     ${\displaystyle (\lnot R)}$ ${\displaystyle \vdash \lnot A,A}$     ${\displaystyle (PR)}$ ${\displaystyle \vdash A,\lnot A}$            ${\displaystyle (I)}$ ${\displaystyle B\vdash B}$     ${\displaystyle (WR)}$ ${\displaystyle B\vdash B,C}$            ${\displaystyle (I)}$ ${\displaystyle C\vdash C}$     ${\displaystyle (WR)}$ ${\displaystyle C\vdash B,C}$         ${\displaystyle (\lor L)}$ ${\displaystyle B\lor C\vdash B,C}$     ${\displaystyle (PR)}$ ${\displaystyle B\lor C\vdash C,B}$     ${\displaystyle (\lnot L)}$ ${\displaystyle B\lor C,\lnot C\vdash B}$              ${\displaystyle (I)}$ ${\displaystyle \lnot A\vdash \lnot A}$         ${\displaystyle (\rightarrow L)}$ ${\displaystyle \left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A}$     ${\displaystyle (\land L_{1})}$ ${\displaystyle \left(B\lor C\right),\lnot C,\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (PL)}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\lnot C\vdash \lnot A}$     ${\displaystyle (\land L_{2})}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (CL)}$ ${\displaystyle \left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$     ${\displaystyle (PL)}$ ${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(B\lor C\right)\vdash \lnot A}$		${\displaystyle (\rightarrow L)}$
${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A,\lnot A}$
		${\displaystyle (CR)}$
${\displaystyle \left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A}$
		${\displaystyle (PL)}$
${\displaystyle \left(A\rightarrow \left(B\lor C\right)\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A}$
		${\displaystyle (\rightarrow R)}$
${\displaystyle \left(A\rightarrow \left(B\lor C\right)\right)\vdash \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)}$
		${\displaystyle (\rightarrow R)}$
${\displaystyle \vdash \left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}$

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

بالنسبة لبعض الصيغ (أي المتغيرات) لحساب التفاضل والتكامل المتسلسل، فإن الإثبات في مثل هذا الحساب يكون متماثلًا مع جدول تحليلي مغلق ومقلوب . ^[25]

وتستحق القواعد الهيكلية بعض المناقشة الإضافية.

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

يضمن الانكماش (C) والتبديل (P) عدم أهمية الترتيب (P) أو تعدد حدوثات (C) عناصر المتتاليات. وبالتالي، يمكننا بدلاً من المتتاليات أن نفكر في المجموعات أيضًا .

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

يمكن إثبات أن نظام القواعد هذا سليم وكامل فيما يتعلق بالمنطق من الدرجة الأولى ، أي أن العبارة تتبع دلاليًا مجموعة من المقدمات إذا وفقط إذا كان من الممكن استنتاج المتتالية من خلال القواعد المذكورة أعلاه. ^[26]${\displaystyle A}$${\displaystyle \Gamma }$ ${\displaystyle (\Gamma \vDash A)}$ ${\displaystyle \Gamma \vdash A}$

في حساب التفاضل والتكامل المتسلسل، تكون قاعدة القطع مقبولة . يشار إلى هذه النتيجة أيضًا باسم نظرية جينتزن الرئيسية . ^{[2] [3]}

يمكن تعديل القواعد المذكورة أعلاه بطرق مختلفة:

هناك قدر من حرية الاختيار فيما يتعلق بالتفاصيل الفنية لكيفية صياغة التسلسلات والقواعد البنيوية دون تغيير التسلسلات التي يستمدها النظام.

أولاً وقبل كل شيء، وكما ذكرنا أعلاه، يمكن اعتبار المتتاليات مكونة من مجموعات أو مجموعات متعددة . في هذه الحالة، لا تكون قواعد التبديل وصيغ التقلص ضرورية.

تصبح قاعدة الإضعاف مقبولة إذا تم تغيير البديهية (I) لاستنتاج أي تسلسل من الشكل . يمكن بعد ذلك نقل أي إضعاف يظهر في الاشتقاق إلى بداية الإثبات. قد يكون هذا تغييرًا مناسبًا عند بناء الأدلة من الأسفل إلى الأعلى. ${\displaystyle \Gamma ,A\vdash A,\Delta }$

يمكن أيضًا تغيير ما إذا كانت القواعد التي تحتوي على أكثر من مقدمة تشترك في نفس السياق لكل من تلك المقدمات أو تقسم سياقاتها بينها: على سبيل المثال، يمكن صياغتها بدلاً من ذلك على النحو التالي ${\displaystyle ({\lor }L)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}.}$

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

يمكننا أن نقدم ثابت العبث الذي يمثل الخطأ ، مع البديهية: ${\displaystyle \bot }$

${\displaystyle {\cfrac {}{\bot \vdash \quad }}}$

أو إذا كان من المفترض أن يكون الضعف قاعدة مقبولة كما هو موضح أعلاه، فعندئذٍ وفقًا للمبدأ:

${\displaystyle {\cfrac {}{\Gamma ,\bot \vdash \Delta }}}$

مع ذلك ، يمكن إدراج النفي كحالة خاصة من الاستدلال، من خلال التعريف . ${\displaystyle \bot }$${\displaystyle (\neg A)\iff (A\to \bot )}$

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

من المدهش أن بعض التغييرات الصغيرة في قواعد LK تكفي لتحويلها إلى نظام إثبات للمنطق الحدسي . ^[27] ولتحقيق هذه الغاية، يتعين على المرء أن يقتصر على تسلسلات تحتوي على صيغة واحدة على الأكثر على الجانب الأيمن، ^[28] وتعديل القواعد للحفاظ على هذا الثابت. على سبيل المثال، تتم إعادة صياغتها على النحو التالي (حيث C هي صيغة تعسفية): ${\displaystyle ({\lor }L)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash C\qquad \Gamma ,B\vdash C}{\Gamma ,A\lor B\vdash C}}\quad ({\lor }L)}$

يُطلق على النظام الناتج اسم LJ. وهو سليم وكامل فيما يتعلق بالمنطق الحدسي ويسمح بإثبات مماثل للقطع والحذف. ويمكن استخدام هذا في إثبات خصائص الانفصال والوجود .

في الواقع، القواعد الوحيدة في LK التي يجب تقييدها بالنتائج ذات الصيغة الواحدة هي ، (والتي يمكن اعتبارها حالة خاصة من ، كما هو موضح أعلاه) و . عندما يتم تفسير النتائج ذات الصيغة المتعددة على أنها انفصالات، فإن جميع قواعد الاستدلال الأخرى في LK قابلة للاشتقاق في LJ، بينما تصبح القواعد و${\displaystyle ({\to }R)}$${\displaystyle (\neg R)}$${\displaystyle {\to }R}$${\displaystyle ({\forall }R)}$${\displaystyle ({\to }R)}$${\displaystyle ({\forall }R)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash B\lor C}{\Gamma \vdash (A\to B)\lor C}}}$

و(عندما لا يحدث حرا في التسلسل السفلي) ${\displaystyle y}$

${\displaystyle {\cfrac {\Gamma \vdash A[y/x]\lor C}{\Gamma \vdash (\forall xA)\lor C}}.}$

هذه القواعد ليست صالحة حدسيًا.

• حساب التفاضل والتكامل الدائري
• حساب التتابع المتداخل
• الدقة (المنطق)
• نظرية الإثبات

• Buss, Samuel R. (1998). "مقدمة إلى نظرية الإثبات". في Samuel R. Buss (المحرر). Handbook of proof theory. Elsevier. ص 1-78. ISBN 0-444-89840-9.
• كاري، هاسكل بروكس (1977) [1963]. أسس المنطق الرياضي . نيويورك: شركة دوفر للنشر. رقم ISBN 978-0-486-63462-3.
• جنتزن، جيرهارد كارل إريك (1934). "Unter suchungen über das logische Schließen. I". الرياضيات Zeitschrift . 39 (2): 176-210. دوى :10.1007/BF01201353. S2CID  121546341.
• جنتزن، غيرهارد كارل إريك (1935). "Unter suchungen über das logische Schließen. II". الرياضيات Zeitschrift . 39 (3): 405-431. دوى :10.1007/bf01201363. S2CID  186239837.
• جيرارد، جان إيف ؛ بول تايلور؛ إيف لافونت (1990) [1989]. البراهين والأنواع . مطبعة جامعة كامبريدج (أطروحات كامبريدج في علوم الكمبيوتر النظرية، 7). رقم ISBN 0-521-37181-3.
• هيلبرت, ديفيد ; بيرنيز، بول (1970) [1939]. Grundlagen der Mathematik II (الطبعة الثانية). برلين، نيويورك: سبرينغر-فيرلاغ. رقم ISBN 978-3-642-86897-9.
• كليين، ستيفن كول (2009) [1952]. مقدمة في الميتاماثيماتيك . دار نشر إيشي الدولية. رقم ISBN 978-0-923891-57-2.
• كلين، ستيفن كول (2002) [1967]. المنطق الرياضي . مينولا، نيويورك: منشورات دوفر. رقم ISBN 978-0-486-42533-7.
• ليمون، إدوارد جون (1965). المنطق البدائي . توماس نيلسون. ISBN 0-17-712040-1.
• مانكوسو، باولو؛ جالفان، سيرجيو؛ زاك، ريتشارد (2021). مقدمة إلى نظرية الإثبات - إثباتات التطبيع والحذف والقطع والاتساق . مطبعة جامعة أكسفورد . ص. 431. ISBN 978-0-19-289593-6.
• سموليان، رايموند ميريل (1995) [1968]. المنطق من الدرجة الأولى . نيويورك: منشورات دوفر. رقم ISBN 978-0-486-68370-6.
• Suppes, Patrick Colonel (1999) [1957]. مقدمة في المنطق . مينولا، نيويورك: منشورات دوفر. ISBN 978-0-486-40687-9.

• نظرية الإثبات (حسابات متتالية) في موسوعة ستانفورد للفلسفة
• "حساب التفاضل والتكامل المتسلسل"، موسوعة الرياضيات ، EMS Press ، 2001 [1994]
• تسلية قصيرة: حساب التفاضل والتكامل المتسلسل
• دروس تفاعلية في حساب التفاضل والتكامل المتسلسل