متسلسل

يُفهم التسلسل على أفضل وجه في سياق الأنواع الثلاثة التالية من الأحكام المنطقية :

1. تأكيد غير مشروط . لا توجد صيغ سابقة.
   • مثال: ⊢ ب
   • المعنى: الخيار ب صحيح.
2. التأكيد الشرطي . أي عدد من صيغ المقدمات.
   1. عبارة شرطية بسيطة . صيغة ذات نتيجة واحدة.
      • مثال : A1 _، A2 ، A3 _⊢ B​_​
      • المعنى: إذا كانت A ₁ و A ₂ و A ₃ صحيحة، فإن B صحيحة.
   2. المتتالية . أي عدد من الصيغ المتتالية.
      • مثال _: A1 _، A2 _، A3 ⊢ _B1 ، B2 _، B3 ، B4​​​_​​_​
      • المعنى: إذا كانت A ₁ و A ₂ و A ₃ صحيحة، فإن B ₁ أو B ₂ أو B ₃ أو B ₄ صحيحة.

وبالتالي فإن المتتاليات هي تعميم للتأكيدات الشرطية البسيطة، والتي هي بدورها تعميم للتأكيدات غير الشرطية.

كلمة "أو" هنا هي "أو" الشاملة . ^{[ 1 ]} الدافع وراء الدلالات الانفصالية على الجانب الأيمن من المتتالية يأتي من ثلاث فوائد رئيسية.

1. تناظر قواعد الاستدلال الكلاسيكية للمتتاليات ذات هذه الدلالات.
2. سهولة وبساطة تحويل هذه القواعد الكلاسيكية إلى قواعد حدسية.
3. القدرة على إثبات اكتمال حساب التفاضل والتكامل عندما يتم التعبير عنه بهذه الطريقة.

تم تحديد هذه الفوائد الثلاث جميعها في الورقة التأسيسية التي كتبها جنتزن (1934 ، ص 194) . 

لم يلتزم جميع المؤلفين بالمعنى الأصلي الذي وضعه جنتزن لكلمة "متتالية". فعلى سبيل المثال، استخدم ليمون (1965) كلمة "متتالية" حصراً للدلالة على العبارات الشرطية البسيطة ذات صيغة نتيجة واحدة فقط. ^{[ 2 ]} ويُقدّم هوث وريان (2004) ، صفحة 5 ، التعريف نفسه للمتتالية ذات النتيجة الواحدة . 

في تسلسل عام من الشكل

${\displaystyle \Gamma \vdash \Sigma }$

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

الرمز '${\displaystyle \vdash }$يُشار إلى الرمز ' غالبًا باسم " البوابة الدوارة " أو "المسار الصحيح" أو "نقطة الانطلاق" أو "علامة التأكيد" أو "رمز التأكيد". ويُقرأ أحيانًا، بشكل موحٍ، بمعنى "يُؤدي" أو "يُثبت" أو "يستلزم".

تعني المتتالية من الشكل '⊢ α, β'، للصيغتين المنطقيتين α و β، أن إما α صحيحة أو β صحيحة (أو كليهما). لكن هذا لا يعني أن α أو β تحصيل حاصل. ولتوضيح ذلك، لنأخذ المثال '⊢ B ∨ A, C ∨ ¬A'. هذه متتالية صحيحة لأن إما B ∨ A صحيحة أو C ∨ ¬A صحيحة. لكن لا يُعد أي من هذين التعبيرين تحصيل حاصل بحد ذاته، بل التحييد هو فصل هذين التعبيرين.

وبالمثل، فإن متتالية من الشكل 'α, β ⊢'، للصيغتين المنطقيتين α و β، تعني أن إما α خاطئة أو β خاطئة. لكن هذا لا يعني أن α متناقضة أو β متناقضة. ولتوضيح ذلك، لنأخذ المثال 'B ∧ A, C ∧ ¬A ⊢'. هذه متتالية صحيحة لأن إما B ∧ A خاطئة أو C ∧ ¬A خاطئة. لكن لا يُعد أي من هذين التعبيرين تناقضًا بحد ذاته، بل التناقض يكمن في اقتران هذين التعبيرين.

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

القاعدة النموذجية هي:

${\displaystyle {\frac {\Gamma ,\alpha \vdash \Sigma \qquad \Gamma \vdash \alpha }{\Gamma \vdash \Sigma }}}$

وهذا يشير إلى أنه إذا استطعنا استنتاج ذلك${\displaystyle \Gamma ,\alpha }$العائد${\displaystyle \Sigma }$وذلك${\displaystyle \Gamma }$العائد${\displaystyle \alpha }$إذن يمكننا أيضاً أن نستنتج أن${\displaystyle \Gamma }$العائد ${\displaystyle \Sigma }$(انظر أيضًا المجموعة الكاملة لقواعد الاستدلال في حساب التفاضل والتكامل المتتالي .)

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

في عام ١٩٣٤، لم يُعرّف جنتزن رمز التأكيد '⊢' في المتتالية للدلالة على إمكانية الإثبات، بل عرّفه بأنه يعني تمامًا نفس معنى عامل الاستلزام '⇒'. وباستخدام '→' بدلًا من '⊢' و'⊃' بدلًا من '⇒'، كتب: "المتتالية A₁ _, ..., Aμ _→ B₁ _, ..., Bν _تعني ، من حيث المضمون، نفس معنى الصيغة (A₁ _& ... & Aμ ) ⊃ ( _B₁ ∨ ... ∨ Bν _{) "} . ^{[ ٤ ]} (استخدم جنتزن رمز السهم المتجه لليمين بين المقدمات والنتائج في المتتاليات، واستخدم الرمز '⊃' لعامل الاستلزام المنطقي).

وفي عام 1939، ذكر هيلبرت وبرنايز بالمثل أن المتتالية لها نفس معنى صيغة الاستلزام المقابلة. ^{[ 5 ]}

في عام 1944، أكد ألونسو تشيرش أن تأكيدات جينتزن المتتالية لا تعني إمكانية إثباتها.

"مع ذلك، لا ينبغي الخلط بين استخدام نظرية الاستنتاج كقاعدة أولية أو مشتقة وبين استخدام جينتزن لـ Sequenzen . فسهم جينتزن، →، لا يُقارن برمزنا النحوي، ⊢، بل ينتمي إلى لغته الموضوعية (كما يتضح من حقيقة أن التعبيرات التي تحتوي عليه تظهر كمقدمات ونتائج في تطبيقات قواعد الاستدلال الخاصة به)." ^{[ 6 ]}

أشارت العديد من المنشورات اللاحقة إلى أن رمز التأكيد في المتتاليات يدل على إمكانية إثباتها ضمن النظرية التي تُصاغ فيها هذه المتتاليات. فقد ذكر كل من كاري عام 1963 ^{[ 7 ]} ، وليمن عام 1965 ^{[ 2 ]} ، وهوث وريان عام 2004 ^{[ 8 ]} أن رمز التأكيد في المتتاليات يدل على إمكانية إثباتها. مع ذلك، يذكر بن آري (2012 ، ص 69) أن رمز التأكيد في متتاليات نظام جنتزن، والذي يرمز إليه بـ '⇒'، هو جزء من لغة الموضوع، وليس من اللغة الوصفية . ^{[ 9 ]} 

بحسب براويتز (1965): "يمكن فهم حسابات المتتاليات على أنها حسابات فوقية لعلاقة الاستدلال في أنظمة الاستدلال الطبيعي المقابلة." ^{[ 10 ]} وعلاوة على ذلك: "يمكن اعتبار البرهان في حساب المتتاليات بمثابة تعليمات حول كيفية بناء استدلال طبيعي مقابل." ^{[ 11 ]} بمعنى آخر، يُعد رمز التأكيد جزءًا من لغة الموضوع لحساب المتتاليات، وهو نوع من الحسابات الفوقية، ولكنه في الوقت نفسه يدل على الاستدلال في نظام استدلال طبيعي أساسي.

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

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

بالطبع، توجد تفسيرات بديهية أخرى ممكنة، وهي مكافئة لها من الناحية الكلاسيكية. على سبيل المثال،${\displaystyle \Gamma \vdash \Sigma }$يمكن قراءة ذلك على أنه يؤكد أنه لا يمكن أن تكون كل صيغة في Γ صحيحة وكل صيغة في Σ خاطئة (هذا مرتبط بتفسيرات النفي المزدوج للمنطق الحدسي الكلاسيكي ، مثل نظرية جليفنكو ).

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

وبغض النظر عن أي تناقضات في التعريف الدقيق من الناحية الفنية أعلاه، يمكننا وصف المتتاليات في شكلها المنطقي التمهيدي.${\displaystyle \Gamma }$يمثل مجموعة من الافتراضات التي نبدأ بها عمليتنا المنطقية، على سبيل المثال "سقراط إنسان" و"كل البشر فانون".${\displaystyle \Sigma }$يمثل هذا استنتاجًا منطقيًا يتبع هذه المقدمات. على سبيل المثال، "سقراط فانٍ" ينتج عن صياغة معقولة للنقاط المذكورة أعلاه، ويمكننا أن نتوقع رؤيته في${\displaystyle \Sigma }$جانب البوابة الدوارة . بهذا المعنى،${\displaystyle \vdash }$يعني عملية الاستدلال، أو "لذلك" باللغة الإنجليزية.