نظرية الاستنتاج

في المنطق الرياضي ، تُعدّ نظرية الاستنتاج نظريةً فوقيةً تُبرّر إجراء البراهين الشرطية انطلاقًا من فرضيةٍ ما في الأنظمة التي لا تُؤَسِّس تلك الفرضية بشكلٍ صريح، أي لإثبات استلزامٍ ما.${\displaystyle A\to B}$يكفي أن نفترض${\displaystyle A}$كفرضية، ثم المضي قدماً في استخلاص النتائج${\displaystyle B}$توجد نظريات الاستنتاج في كلٍّ من منطق القضايا ومنطق الرتبة الأولى . ^{[ 1 ] [ 2 ]} تُعدّ نظرية الاستنتاج أداةً مهمةً في أنظمة الاستنتاج على نمط هيلبرت، لأنها تُتيح كتابة براهين أكثر وضوحًا وأقصر بكثير مما يُمكن كتابته بدونها. في بعض أنظمة البرهان الرسمية الأخرى، تُوفّر قاعدة استدلال صريحة نفس الميزة؛ على سبيل المثال، يُطلق على هذا في الاستنتاج الطبيعي اسم "إدخال الاستلزام" .

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

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

1. "إثبات" البديهية 1: P → ( Q → P ) ^{[ 6 ]}

   • الفرضية P 1
     • السؤال الثاني: الفرضية
     • ص 3. تكرار لـ 1
   • Q → P 4. الطرح من 2 إلى 3

   • P → ( Q → P ) 5. استنتاج من 1 إلى 4 وهو المطلوب إثباته
2. "أثبت" البديهية 2: ( P → ( Q → R )) → (( P → Q ) → ( P → R ))

   • P → ( Q → R ) 1. الفرضية
     • P → Q 2. الفرضية
       • الفرضية الثالثة
       • س 4. وضع الدليل 3.2
       • Q → R 5. modus ponens 3,1
       • R 6. modus ponens 4,5
     • P → R 7. الطرح من 3 إلى 6
   • ( P → Q ) → ( P → R ) 8. الاستنتاج من 2 إلى 7

   • ( P → ( Q → R )) → (( P → Q ) → ( P → R )) 9. الاستنتاج من 1 إلى 8. وهو المطلوب إثباته.
3. باستخدام البديهية 1 لإثبات (( P →( Q → P ))→ R )→ R :

   • ( P → ( Q → P )) → R 1. الفرضية
   • P →( Q → P ) 2. البديهية 1
   • R 3. modus ponens 2,1

   • (( P → ( Q → P )) → R ) → R 4. الاستنتاج من 1 إلى 3. وهو المطلوب إثباته.

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

1. الفرضية هي خطوة يتم فيها إضافة مقدمة إضافية إلى المقدمات الموجودة بالفعل. لذا، إذا تم استنتاج الخطوة السابقة S على النحو التالي:

${\displaystyle E_{1},E_{2},...,E_{n-1},E_{n}\vdash S,}$

ثم يضيف المرء مقدمة أخرى H ويحصل على:

${\displaystyle E_{1},E_{2},...,E_{n-1},E_{n},H\vdash H.}$

يتم التعبير عن ذلك بالانتقال من المستوى n من المسافة البادئة إلى المستوى n + 1 وقول ^{[ 9 ]}

• الخطوة السابقة
  • فرضية H

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

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

• فرضية H
• ......... (خطوات أخرى)
• ج (استنتاج مستخلص من ح )

• استنتاج H → C

في النسخ البديهية من منطق القضايا، عادةً ما يكون لدينا من بين مخططات البديهيات (حيث يتم استبدال P و Q و R بأي قضايا):

• البديهية الأولى هي: P → ( Q → P )
• البديهية الثانية هي: ( P → ( Q → R )) → (( P → Q ) → ( P → R ))
• طريقة القياس هي: من P و P → Q يستنتج Q

تم اختيار هذه المخططات البديهية لتسهيل استنباط نظرية الاستنتاج منها. لذا قد يبدو للوهلة الأولى أننا نصادر على المطلوب . مع ذلك، يمكن تبريرها بالتحقق من كونها تحصيل حاصل باستخدام جداول الصواب، وأن قاعدة القياس المنطقي (modus ponens) تحافظ على الصواب.

من مخططات البديهيات هذه، يمكن للمرء أن يستنتج بسرعة مخطط النظرية P → P (انعكاسية الاستلزام)، والذي يتم استخدامه أدناه:

1. ( P → (( Q → P ) → P )) → (( P → ( Q → P )) → ( P → P )) من مخطط البديهية 2 مع P و ( Q → P ) و P
2. P →(( Q → P )→ P ) من مخطط البديهية 1 مع P ، ( Q → P )
3. ( P → ( Q → P )) → ( P → P ) من قاعدة القياس المنطقي (modus ponens) المطبقة على الخطوتين 2 و1
4. P →( Q → P ) من مخطط البديهية 1 مع P و Q
5. P → P من قاعدة القياس المنطقي (modus ponens) المطبقة على الخطوتين 4 و3

لنفترض أن لدينا Γ و H معًا يثبتان C ، ونريد أن نبين أن Γ يثبت H → C. لكل خطوة S في الاستنتاج، سواء كانت مقدمة في Γ (خطوة تكرار) أو بديهية، يمكننا تطبيق قاعدة القياس المنطقي (modus ponens) على البديهية 1، S → ( H → S )، لنحصل على H → S. إذا كانت الخطوة هي H نفسها (خطوة فرضية)، نطبق مخطط النظرية لنحصل على H → H. إذا كانت الخطوة هي نتيجة تطبيق قاعدة القياس المنطقي على A و A → S ، نتأكد أولًا من تحويلهما إلى H → A و H → ( A → S )، ثم نأخذ البديهية 2، ( H → ( A → S )) → (( H → A ) → ( H → S ))، ونطبق قاعدة القياس المنطقي لنحصل على ( H → A ) → ( H → S )، ثم نطبقها مرة أخرى لنحصل على H → S. في نهاية البرهان ، سنحصل على H → C كما هو مطلوب، إلا أنه الآن يعتمد فقط على Γ، وليس على H. لذا ستختفي خطوة الاستنتاج، وتُدمج في الخطوة السابقة التي كانت الاستنتاج المستمد من H.

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

أثناء التحويل، قد يكون من المفيد وضع جميع تطبيقات قاعدة الاستنتاج على البديهية 1 في بداية الاستنتاج (مباشرة بعد خطوة H → H ).

عند تحويل قاعدة الاستدلال المنطقي (modus ponens)، إذا كانت A خارج نطاق H ، فسيكون من الضروري تطبيق البديهية 1، A → ( H → A )، ثم قاعدة الاستدلال المنطقي (modus ponens) للحصول على H → A. وبالمثل، إذا كانت A → S خارج نطاق H ، فيُطبَّق البديهية 1، ( A → S ) → ( H → ( A → S ))، ثم قاعدة الاستدلال المنطقي (modus ponens) للحصول على H → ( A → S ). لا ينبغي القيام بكلتا الخطوتين، إلا إذا كانت خطوة قاعدة الاستدلال المنطقي (modus ponens) هي النتيجة، لأنه إذا كانت كلتاهما خارج النطاق، لكان من المفترض نقل قاعدة الاستدلال المنطقي (modus ponens) إلى الأعلى قبل H ، وبالتالي ستكون خارج النطاق أيضًا.

في إطار تناظر كاري-هوارد ، تُشابه عملية التحويل المذكورة أعلاه لنظرية الاستنتاج الميتافيزيقية عملية التحويل من مصطلحات حساب لامدا إلى مصطلحات المنطق التوافقي ، حيث يُقابل المُسلَّم 1 مُركِّب K، ويُقابل المُسلَّم 2 مُركِّب S. لاحظ أن مُركِّب I يُقابل مخطط النظرية P → P.

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

${\displaystyle A\to A}$

يساعد في تحويل خطوات الفرضية.

${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

يساعد في تحويل قاعدة الاستدلال عندما لا تعتمد المقدمة الرئيسية على الفرضية، ويحل محل البديهية 2 مع تجنب استخدام البديهية 1.

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

يساعد في تحويل قاعدة الاستدلال عندما لا تعتمد المقدمة الصغرى على الفرضية، ويحل محل البديهية 2 مع تجنب استخدام البديهية 1.

يمكن استخدام هاتين النظريتين معًا بدلاً من البديهية 2، على الرغم من أن البرهان المحول سيكون أكثر تعقيدًا:

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle (A\to (A\to C))\to (A\to C)}$

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

${\displaystyle ((A\to B)\to A)\to A}$

ويمكن استخدامه أيضًا للحصول على النظرية الثانية من النظريتين، والتي يمكن استخدامها بدلاً من البديهية 2.

نبرهن على نظرية الاستنتاج في نظام استنتاجي على نمط هيلبرت لحساب القضايا. ^{[ 10 ]}

يترك${\displaystyle \Delta }$أن تكون مجموعة من الصيغ و${\displaystyle A}$و${\displaystyle B}$الصيغ، بحيث${\displaystyle \Delta \cup \{A\}\vdash B}$نريد أن نثبت ذلك${\displaystyle \Delta \vdash A\to B}$.

منذ${\displaystyle \Delta \cup \{A\}\vdash B}$، وهناك دليل على${\displaystyle B}$من${\displaystyle \Delta \cup \{A\}}$نبرهن النظرية بالاستقراء على طول البرهان n ؛ وبالتالي فإن فرضية الاستقراء هي أنه لأي${\displaystyle \Delta }$،${\displaystyle A}$و${\displaystyle B}$بحيث يكون هناك دليل على${\displaystyle B}$من${\displaystyle \Delta \cup \{A\}}$بطول يصل إلى n ،${\displaystyle \Delta \vdash A\to B}$يحجز.

إذا كانت قيمة n تساوي 1، فإن${\displaystyle B}$هو عضو في مجموعة الصيغ${\displaystyle \Delta \cup \{A\}}$وبالتالي إما${\displaystyle B=A}$وفي هذه الحالة${\displaystyle A\to B}$هو ببساطة${\displaystyle A\to A}$، والتي يمكن استنتاجها بالتعويض من p → p ، والتي يمكن استنتاجها من البديهيات، وبالتالي أيضًا${\displaystyle \Delta \vdash A\to B}$، أو${\displaystyle B}$هو في${\displaystyle \Delta }$وفي هذه الحالة${\displaystyle \Delta \vdash B}$ويترتب على ذلك من البديهية p → ( q → p ) مع التعويض أن${\displaystyle \Delta \vdash B\to (A\to B)}$وبالتالي، وفقًا لقاعدة الاستدلال، فإن${\displaystyle \Delta \vdash A\to B}$.

والآن، لنفترض فرضية الاستقراء لإثباتات يصل طولها إلى n ، ولنفترض${\displaystyle B}$أن تكون صيغة قابلة للإثبات من${\displaystyle \Delta \cup \{A\}}$مع برهان طوله n + 1. إذن هناك احتمالان:

1. ${\displaystyle B}$هو عضو في مجموعة الصيغ${\displaystyle \Delta \cup \{A\}}$في هذه الحالة، نتابع كما هو الحال بالنسبة لـ n = 1.
2. ${\displaystyle B}$يتم التوصل إلى ذلك باستخدام قاعدة الاستدلال المنطقي (modus ponens). ثم توجد صيغة C بحيث${\displaystyle \Delta \cup \{A\}}$يثبت${\displaystyle C}$و${\displaystyle C\to B}$ثم يُستخدم مبدأ القياس المنطقي لإثبات ذلك.${\displaystyle B}$. البراهين على${\displaystyle C}$و${\displaystyle C\to B}$تتضمن على الأكثر n خطوة، وبناءً على فرضية الاستقراء لدينا${\displaystyle \Delta \vdash A\to C}$و${\displaystyle \Delta \vdash A\to (C\to B)}$. من خلال البديهية ( p → ( q → r )) → (( p → q ) → ( p → r )) مع التعويض، ينتج أن ${\displaystyle \Delta \vdash (A\to (C\to B))\to ((A\to C)\to (A\to B))}$وباستخدام قاعدة الاستدلال مرتين، نحصل على${\displaystyle \Delta \vdash A\to B}$.

وبالتالي، في جميع الحالات، تنطبق النظرية أيضًا على n + 1، وبالاستقراء يتم إثبات نظرية الاستنتاج.

تُعتبر نظرية الاستنتاج صالحة أيضًا في منطق الرتبة الأولى بالشكل التالي:

• إذا كانت T نظرية و F و G صيغتين حيث F مغلقة ، و${\displaystyle T\cup \{F\}\vdash G}$، ثم${\displaystyle T\vdash F\rightarrow G}$.

هنا، الرمز${\displaystyle \vdash }$يعني "هو نتيجة نحوية لـ". نوضح أدناه كيف يختلف برهان نظرية الاستنتاج هذه عن برهان نظرية الاستنتاج في حساب القضايا.

في أكثر نسخ مفهوم البرهان الرسمي شيوعًا، توجد، بالإضافة إلى مخططات بديهيات حساب القضايا (أو الفهم بأن جميع التكرارات في حساب القضايا يجب اعتبارها مخططات بديهيات في حد ذاتها)، بديهيات الكمية ، وبالإضافة إلى قاعدة الاستدلال ، قاعدة استدلال إضافية واحدة ، تُعرف باسم قاعدة التعميم : "من K ، استنتج ∀ vK ".

لتحويل برهان G من T ∪ { F } إلى برهان F → G من T ، يتم التعامل مع خطوات برهان G التي تُعدّ بديهيات أو تنتج عن تطبيق قاعدة القياس المنطقي (modus ponens) بنفس طريقة البراهين في منطق القضايا. أما الخطوات الناتجة عن تطبيق قاعدة التعميم، فيتم التعامل معها عبر بديهية المُكمِّم التالية (الصحيحة عندما لا يكون المتغير v حرًا في الصيغة H ):

• (∀ v ( H → K ))→( H →∀ vK ).

بما أن F في حالتنا مفترضة أنها مغلقة، يمكننا اعتبار H هي F. تسمح هذه البديهية باستنتاج F → ∀ vK من F → K والتعميم، وهو ما نحتاجه بالضبط عندما تُطبق قاعدة التعميم على K في برهان G.

في منطق الرتبة الأولى، يمكن تخفيف شرط أن تكون F صيغة مغلقة بشرط ألا تكون المتغيرات الحرة في F قد تغيرت في استنتاج G من${\displaystyle T\cup \{F\}}$في حالة تغيير متغير حر v في F أثناء الاستنتاج، نكتب${\displaystyle T\cup \{F\}\vdash ^{v}G}$(الرقم العلوي في البوابة الدوارة الذي يشير إلى تغيير قيمة v) والصيغة المقابلة لنظرية الاستنتاج هي${\displaystyle T\vdash (\forall vF)\rightarrow G}$[ ^{11 ]​}

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

أولاً، نكتب برهانًا باستخدام طريقة تشبه طريقة الاستنتاج الطبيعي:

• السؤال 1. الفرضية
  • س ← ر 2. الفرضية
  • R 3. modus ponens 1,2
• ( Q → R ) → R 4. الاستنتاج من 2 إلى 3

• Q → (( Q → R ) → R ) 5. استنتاج من 1 إلى 4. وهو المطلوب إثباته.

ثانيًا، نحول الاستنتاج الداخلي إلى برهان بديهي:

• ( Q → R )→( Q → R ) 1. مخطط النظرية ( A → A )
• (( Q → R )→( Q → R ))→((( Q → R )→ Q )→(( Q → R )→ R )) 2. البديهية 2
• (( Q → R )→ Q )→(( Q → R )→ R ) 3. طريقة العمل 1,2
• س →(( س → ص )→ س ) 4. البديهية 1
  • السؤال 5. الفرضية
  • ( س → ص ) → س 6. طريقة العمل 5,4
  • ( س → ص ) → ص 7. طريقة العمل 6,3
• Q → (( Q → R ) → R ) 8. استنتاج من 5 إلى 7 وهو المطلوب إثباته

ثالثًا، نحول الاستنتاج الخارجي إلى برهان بديهي:

• ( Q → R )→( Q → R ) 1. مخطط النظرية ( A → A )
• (( Q → R )→( Q → R ))→((( Q → R )→ Q )→(( Q → R )→ R )) 2. البديهية 2
• (( Q → R )→ Q )→(( Q → R )→ R ) 3. طريقة العمل 1,2
• س →(( س → ص )→ س ) 4. البديهية 1
• [(( Q → R )→ Q )→(( Q → R )→ R )]→[ Q →((( Q → R )→ Q )→(( Q → R )→ R ))] 5. البديهية 1
• س → ((( Q → R )→ Q )→(( Q → R )→ R )) 6. طريقة العمل 3,5
• [ Q →((( Q → R )→ Q )→(( Q → R )→ R ))]→([ Q →(( Q → R )→ Q )]→[ Q →(( Q → R )→ R )]) 7. البديهية 2
• [ Q →(( Q → R )→ Q )]→[ Q →(( Q → R )→ R )] 8. طريقة العمل 6,7
• Q →(( Q → R )→ R ) 9. طريقة العمل 4,8 QED

يمكن تلخيص هذه الخطوات الثلاث بإيجاز باستخدام معادلة كاري-هوارد :

• أولاً، في حساب التفاضل والتكامل اللامدا، تكون الدالة f = λa. λb. ba من النوع q → ( q → r ) → r
• ثانيًا، عن طريق حذف لامدا على b، f = λa. si (ka)
• ثالثًا، عن طريق حذف لامدا على a، f = s (k (si)) k

• نظرية الحذف بالقطع
• إثبات مشروط
• الكاري
• حساب القضايا
• قانون بيرس

• فيتش، فريدريك برينتون (1952). المنطق الرمزي: مقدمة . نيويورك: شركة رونالد برس. LCCN 52006196 . 
• فرانكس، كورتيس. "نظرية الاستنتاج" (ملف PDF) . جامعة نوتردام . تم الاطلاع عليه بتاريخ 21 يوليو 2020 .
• هيويت، كارل (2008). "منظمات تنظيمية للحوسبة السحابية للعملاء قابلة للتوسع، وقوية، ومراعية للخصوصية". مجلة IEEE للحوسبة عبر الإنترنت . 12 (5): 96-99 . doi : 10.1109/MIC.2008.107 . S2CID 27828219 . سبتمبر/أكتوبر 2008
• كلين، ستيفن كول (2002) [1967]. المنطق الرياضي . نيويورك: منشورات دوفر . ISBN 978-0-486-42533-7MR 1950307 .​ 
• كلين، ستيفن كول (1980). مقدمة في ما وراء الرياضيات . نورث هولاند. ISBN 9780720421033.
• كولينباخ، أولريش (2008). نظرية البرهان التطبيقية: تفسيرات البرهان واستخدامها في الرياضيات . سلسلة دراسات سبرينغر في الرياضيات. برلين، نيويورك: سبرينغر-فيرلاغ . ISBN 978-3-540-77532-4MR 2445721 .​ 
• راوتنبرغ، وولفغانغ (2010). مقدمة موجزة في المنطق الرياضي (  الطبعة الثالثة). نيويورك : سبرينغر ساينس + بيزنس ميديا . doi : 10.1007/978-1-4419-1221-3 . ISBN 978-1-4419-1220-6..
• شوينفيلد، جوزيف ر. (2001) [1967]. المنطق الرياضي (  الطبعة الثانية). إيه كيه بيترز . ISBN 978-1-56881-135-2.
• سميث، بيتر (13 أكتوبر 2010). "أنواع أنظمة الإثبات" (ملف PDF) . مجلة Logic Matters . تاريخ الاسترجاع: 29 مايو 2025 .

• يُعد كتاب "مقدمة في المنطق الرياضي" من تأليف فيلنيس ديتلوفس وكارليس بودنيكس مرجعًا شاملًا. انظر القسم 1.5.
• "نظرية الاستنتاج"