تدوين سوبس-ليمون

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

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

تدوين Suppes-Lemmon هو تدوين لحساب المسند مع المساواة، لذلك يمكن فصل وصفه إلى جزأين: بناء الجملة العام للإثبات والقواعد الخاصة بالسياق .

قواعد حساب المسند مع المساواة

البرهان المذكور أعلاه صحيح، ولكن ليس من الضروري أن تكون البراهين صحيحة لتتوافق مع الصيغة العامة لنظام البرهان. مع ذلك، لضمان صحة أي متتالية، يجب الالتزام بقواعد محددة بدقة. يمكن تقسيم هذه القواعد إلى أربع مجموعات: قواعد القضايا (1-11)، وقواعد المسندات (12-15)، وقواعد المساواة (15-16)، وقاعدة الاستبدال ( 18). يتيح جمع هذه المجموعات بالترتيب بناء حساب قضايا ، ثم حساب مسندات، ثم حساب مسندات مع المساواة، ثم حساب مسندات مع المساواة، مما يسمح باشتقاق قواعد جديدة. في الجدول أدناه، تم تمييز قواعد القضايا المشتقة (10-11). وهي ناتجة عن قواعد جنتزن الأولية (غير المميزة) . القاعدتان 8 ( حذف النفي المزدوج ) و9 ( البرهان بالخلف ) متكافئتان. يمكن حذف أحدها (أو دمجه في القواعد المشتقة).

قائمة قواعد الاستدلال

	اسم القاعدة	شرح	وصف	افتراض
1	الافتراضات	أ	يبرر الحرف "أ" أي صيغة منطقية. والافتراض الوحيد هو رقم السطر الخاص به.	الافتراض الوحيد هو رقم السطر الخاص به.
2	مقدمة	أ، ب ∧I	إذا كانت القضايا${\displaystyle P}$و${\displaystyle Q}$عند السطرين أ و ب ، فإن " أ ، ب ∧ أنا" تبرر${\displaystyle P\wedge Q}$.	الافتراضات هي المجموعة الجماعية للمقترحات المتصلة.
3	∧-الإزالة	أ ∧ هـ	إذا كان السطر أ عبارة عن رابط${\displaystyle P\wedge Q}$يمكن للمرء أن يستنتج إما${\displaystyle P}$أو${\displaystyle Q}$باستخدام " a ∧E". يسمح كل من ∧I و ∧E برتابة الاستلزام، كما هو الحال عندما تكون القضية${\displaystyle P}$يتم ضمها إلى${\displaystyle Q}$مع ∧I ومفصولة بـ ∧E، فإنها تحتفظ${\displaystyle Q}$افتراضات.	الافتراضات هي السطر أ .
4	∨-مقدمة	أ ∨I	لخط a مع اقتراح${\displaystyle P}$يمكن للمرء أن يقدم${\displaystyle P\vee Q}$بالإشارة إلى " a ∨I".	الافتراضات هي أ .
5	∨-الإزالة	أ، ب، ج، د، هـ ∨ هـ	للفصل${\displaystyle P\vee Q}$، إذا افترض المرء${\displaystyle P}$و${\displaystyle Q}$ويتوصل بشكل منفصل إلى الاستنتاج${\displaystyle R}$ومن كل ذلك، يمكن للمرء أن يستنتج${\displaystyle R}$تُذكر القاعدة على النحو التالي: " أ ، ب ، ج ، د ، هـ ∨ هـ"، حيث يحتوي الخط أ على الفصل الأولي .${\displaystyle P\vee Q}$، يفترض السطران ب و د${\displaystyle P}$و${\displaystyle Q}$على التوالي، وينتهي الخطان ج و هـ${\displaystyle R}$مع${\displaystyle P}$و${\displaystyle Q}$في مجموعات الافتراضات الخاصة بهم.	الافتراضات هي المجموعات المشتركة للخطين الختاميين${\displaystyle R}$، ج و هـ ، مطروحًا منها الخطوط بافتراض${\displaystyle P}$و${\displaystyle Q}$، ب و د .
6	البرهان الشرطي (→I)	ب، أ سي بي	إذا كان هناك خط مع اقتراح${\displaystyle P}$يفترض السطر ب مع الاقتراح${\displaystyle Q}$، " ب ، أ سي بي" يبرر${\displaystyle Q\to P}$.	بغض النظر عن جميع افتراضات (أ )، يتم الاحتفاظ بـ (ب) .
7	Modus Ponendo Ponens (→E)	أ، ب MPP	إذا كان هناك سطران أ و ب سابقًا في البرهان يحتويان${\displaystyle P\to Q}$و${\displaystyle P}$"على التوالي، MPP" " أ ، ب " يبرر${\displaystyle Q}$.	الافتراضات هي المجموعة الجماعية للخطين أ و ب .
8	النفي المزدوج (¬¬E)	رقم وطني	" a DN" يبرر إضافة أو طرح رمزي نفي من الصيغة المنطقية في سطر سابق في البرهان، مما يجعل هذه القاعدة ثنائية الشرط.	مجموعة الافتراضات هي تلك المذكورة في السطر المذكور.
9	الاختزال إلى العبث	ب، أ RAA	للاقتراح${\displaystyle P\wedge \neg P}$على الإنترنت، مع الاستشهاد بافتراض${\displaystyle Q}$في السطر ب ، يمكن الاستشهاد بـ " ب ، أ ر أ أ" واستخلاص${\displaystyle \neg Q}$انطلاقاً من افتراضات الخط أ بصرف النظر عن الخط ب .	الافتراضات الخاصة بالخط أ بصرف النظر عن ب .
10	القياس المنطقي الانفصالي	أ، ب DS	من${\displaystyle P\lor Q}$في السطر أ و${\displaystyle \neg P}$عند السطر ب ، يمكن للمرء أن يستنتج${\displaystyle Q}$. من${\displaystyle P\lor Q}$في السطر أ و${\displaystyle \neg Q}$عند السطر ب ، يمكن للمرء أن يستنتج${\displaystyle P}$.	الافتراضات هي المجموعة الجماعية للخطين أ و ب .
11	الوضع المتجاهل	أ، ب اختبار MTT	للمقترحات${\displaystyle P\to Q}$و${\displaystyle \neg Q}$يمكن الاستشهاد بـ " أ ، ب إم تي تي" في السطرين أ و ب لاستنتاج${\displaystyle \neg P}$وهذا مثبت من القواعد الأخرى المذكورة أعلاه.	الافتراضات هي تلك الخاصة بالخطين أ و ب .
12	مقدمة عالمية	واجهة المستخدم	للمسند${\displaystyle Ra}$في السطر أ ، يمكن الاستشهاد بـ " واجهة المستخدم" لتبرير التحديد الكمي الشامل،${\displaystyle (\forall x)Rx}$بشرط ألا يكون أي من الافتراضات الواردة في السطر ( أ) يحتوي على المصطلح${\displaystyle a}$في أي مكان.	الافتراضات هي تلك الواردة في السطر أ .
13	الاستبعاد الشامل	مستخدم	بالنسبة للمسند الكمي العالمي${\displaystyle (\forall x)Rx}$في السطر أ ، يمكن الاستشهاد بـ " وحدة الاتحاد الأوروبي" لتبرير ذلك${\displaystyle Ra}$. UE عبارة عن ازدواجية مع UI حيث يمكن للمرء التبديل بين المتغيرات الكمية والمتغيرات الحرة باستخدام هذه القواعد.	الافتراضات هي تلك الواردة في السطر أ .
14	مقدمة وجودية	أ. إي	للمسند${\displaystyle Ra}$على الإنترنت، يمكن للمرء أن يستشهد بـ " مؤشر الوجود" لتبرير التحديد الكمي الوجودي.${\displaystyle (\exists x)Rx}$.	الافتراضات هي تلك الواردة في السطر أ .
15	الإزالة الوجودية	أ، ب، ج EE	بالنسبة للمسند الكمي الوجودي${\displaystyle (\exists x)Rx}$في السطر أ ، إذا افترضنا${\displaystyle Ra}$أن يكون صحيحًا في السطر ب، واستنتج${\displaystyle P}$باستخدامها في السطر ج ، يمكننا الاستشهاد بـ " أ ، ب ، ج إي إي" لتبرير${\displaystyle P}$. على المدى${\displaystyle a}$لا يمكن أن يظهر في الخاتمة${\displaystyle P}$، أي من افتراضاتها باستثناء السطر ب ، أو على السطر أ . EE و EI في حالة ازدواجية، كما يمكن للمرء أن يفترض${\displaystyle Ra}$واستخدم الذكاء العاطفي للوصول إلى استنتاج من${\displaystyle (\exists x)Rx}$.	الافتراضات هي الافتراضات الواردة في السطر أ وأي افتراضات في السطر ج باستثناء الافتراضات الواردة في السطر ب .
16	مقدمة عن المساواة	=أنا	يمكن للمرء أن يقدم في أي وقت${\displaystyle a=a}$الاستشهاد بـ "=I" دون أي افتراضات.	لا توجد افتراضات.
17	القضاء على عدم المساواة	أ، ب = هـ	للمقترحات${\displaystyle a=b}$و${\displaystyle P}$في السطرين أ و ب ، يمكن الاستشهاد بـ " أ ، ب = هـ" لتبرير تغيير أي مصطلحات${\displaystyle a}$في${\displaystyle P}$ل${\displaystyle b}$.	الافتراضات هي مجموعة الخطوط أ و ب .
18	مثال الاستبدال	أ، ب SI(S) X	لتسلسل${\displaystyle P,Q\vdash R}$تم إثبات ذلك في البرهان X وحالات الاستبدال لـ${\displaystyle P}$و${\displaystyle Q}$في السطرين أ و ب ، يمكن الاستشهاد بـ " أ ، ب SI(S) X" لتبرير إدخال مثال استبدال لـ${\displaystyle R}$.	افتراضات الخطين أ و ب .

القاعدة المشتقة التي لا تفترض أي افتراضات تُعدّ نظرية، ويمكن تقديمها في أي وقت دون افتراضات. يرمز لها البعض بـ "TI(S)"، اختصارًا لـ "نظرية" بدلًا من "متتالية". كما يكتفي البعض الآخر بالرمز "SI" أو "TI" في الحالتين عندما لا تكون هناك حاجة إلى استبدال، لأن حججهم تتطابق تمامًا مع حجج البرهان المرجعي.

مثال على إثبات متتالية (نظرية في هذه الحالة):

برهان على مبدأ الانفجار باستخدام رتابة الاستلزام . وقد أطلق البعض على التقنية التالية، الموضحة في الأسطر من 3 إلى 6، اسم قاعدة التوسيع (المحدود) للمقدمات: ^{[ 6 ]}

مثال على الاستبدال و ∨E:

يشمل التطور التاريخي لأنظمة الاستدلال الطبيعي ذات التخطيط الجدولي، والتي تعتمد على القواعد، والتي تشير إلى القضايا السابقة بأرقام الأسطر (والأساليب ذات الصلة مثل الخطوط العمودية أو النجوم) المنشورات التالية.

• 1940: في كتاب مدرسي، أشار كواين ^{[ 7 ]} إلى التبعيات السابقة بأرقام الأسطر بين قوسين مربعين، متوقعًا بذلك تدوين أرقام الأسطر لسوبس عام 1957.
• في عام ١٩٥٠، أوضح كواين (١٩٨٢ ، الصفحات ٢٤١-٢٥٥) في كتابه المدرسي طريقةً لاستخدام نجمة واحدة أو أكثر على يسار كل سطر من البرهان للإشارة إلى التبعيات. وهذا يُعادل استخدام كلين للخطوط العمودية. (ليس من الواضح تمامًا ما إذا كانت علامة النجمة التي استخدمها كواين قد ظهرت في الطبعة الأصلية لعام ١٩٥٠ أم أُضيفت في طبعة لاحقة). 
• 1957: مقدمة في إثبات النظريات المنطقية العملية في كتاب مدرسي من تأليف سوبس (1999 ، الصفحات 25-150) . وقد أشارت هذه المقدمة إلى التبعيات (أي القضايا السابقة) من خلال أرقام الأسطر على يسار كل سطر. 
• 1963: يستخدم ستول (1979 ، ص 183-190، 215-219) مجموعات من أرقام الأسطر للإشارة إلى التبعيات السابقة لأسطر الحجج المنطقية المتسلسلة بناءً على قواعد الاستدلال بالاستنتاج الطبيعي. 
• 1965: الكتاب المدرسي الكامل لليمون (1965) هو مقدمة لإثباتات المنطق باستخدام طريقة تعتمد على طريقة سوبس.
• 1967: في كتاب مدرسي، قدم كلين (2002 ، الصفحات 50-58، 128-130) عرضًا موجزًا ​​لنوعين من البراهين المنطقية العملية، أحدهما يستخدم اقتباسات صريحة للقضايا السابقة على يسار كل سطر، والآخر يستخدم خطوطًا عمودية على اليسار للإشارة إلى التبعيات. ^{[ 8 ]} 

• الاستنتاج الطبيعي
• حساب المتتابعات
• الأنظمة الاستنتاجية

• كوبورن، باري؛ ميلر، ديفيد (أكتوبر 1977). "تعليقان على كتاب ليمون "منطق البداية"" . مجلة نوتردام للمنطق الصوري . 18 (4): 607-610 . doi : 10.1305/ndjfl/1093888128 . ISSN 0029-4527 . 
• جنتزن، جيرهارد كارل إريك (1934). "Unter suchungen über das logische Schließen. I" . الرياضيات Zeitschrift . 39 (2): 176-210 . دوى : 10.1007 / BF01201353 . (ترجمة إنجليزية : تحقيقات في الاستدلال المنطقي عند سزابو.)
• جنتزن، غيرهارد كارل إريك (1935). "Unter suchungen über das logische Schließen. II" . الرياضيات Zeitschrift . 39 (3): 405-431 . دوى : 10.1007 / bf01201363 .
• كلين، ستيفن كول (2002) [1967]. المنطق الرياضي . مينولا، نيويورك: منشورات دوفر. ISBN 978-0-486-42533-7.
• ليمون، إدوارد جون (1965). مدخل إلى المنطق . توماس نيلسون. ISBN 0-17-712040-1.
• بيليتييه، فرانسيس جيفري؛ هازن، ألين (2024). "أنظمة الاستدلال الطبيعي في المنطق" . في زالتا، إدوارد ن.؛ نودلمان، أوري (محرران). موسوعة ستانفورد للفلسفة (  طبعة ربيع 2024). مختبر أبحاث الميتافيزيقا، جامعة ستانفورد . تاريخ الاسترجاع: 25 مايو 2025 .
• كواين، ويلارد فان أورمان (1981) [1940]. المنطق الرياضي (  طبعة منقحة). كامبريدج، ماساتشوستس: مطبعة جامعة هارفارد. ISBN 978-0-674-55451-1.
• كواين، ويلارد فان أورمان (1982) [1950]. مناهج المنطق (  الطبعة الرابعة). كامبريدج، ماساتشوستس: مطبعة جامعة هارفارد. ISBN 978-0-674-57176-1.
• ستول، روبرت روث (1979) [1963]. نظرية المجموعات والمنطق . مينولا، نيويورك: منشورات دوفر. ISBN 978-0-486-63829-4.
• سوبس، باتريك كولونيل (1999) [1957]. مقدمة في المنطق . مينولا، نيويورك: منشورات دوفر. ISBN 978-0-486-40687-9.
• سزابو، م. إ. (1969). الأوراق المجمعة لغيرهارد جنتزن . أمستردام: نورث هولاند.

• بيليتييه، جيف، " تاريخ كتب الاستدلال الطبيعي والمنطق الابتدائي " .