استنتاج طبیعی

الگو:منابع وجود دارد در منطق و نظریهٔ برهان، استنتاج طبیعی الگو:به انگلیسی نوعی حساب اثباتی می‌باشد که در آن استدلال منطقی با قواعد استنتاجی که نزدیک به روش «طبیعی» استدلال است، بیان می‌شود. این در تضاد با دستگاه‌های هیلبرتی است که در عوض از اصول موضوعه تا حد امکان برای بیان قوانین منطقی استدلال استنتاجی استفاده می‌کنند.

قواعد

یکی از قواعد استنتاج طبیعی، وضع مقدم است. به‌طور شهودی، این قاعده بیان می‌کند که اگر بدانیم $P$ مستلزم $Q$ است و بدانیم که $P$ درست است، آنگاه می‌توانیم نتیجه بگیریم که $Q$ که به این صورت می‌توان آن را نوشت: $P\to Q,P⊢Q$. نماد $⊢$ به این معنی است که از فرض‌های $P\to Q$ و $P$، با قواعد استنتاج ثابت می‌کنیم (نتیجه می‌گیریم) که $Q$. تعدادی دیگر از قواعد به این شکل هستند:

• قاعدهٔ رفع تالی: $P\to Q,\sim Q⊢\sim P$.
• قاعدهٔ معرفی عطف: $P,Q⊢P\wedge Q$.
• قاعدهٔ حذف عطف: $P\wedge Q⊢P,P\wedge Q⊢Q$.
• قاعدهٔ معرفی فصل: $P⊢P\vee Q$.
• قاعدهٔ حذف فصل: $(P\to Q),(R\to Q),(P\vee R)⊢Q$.
• قاعدهٔ قیاس فصلی: $P\vee Q,\sim P⊢Q$.

مثال‌ها

$P\wedge \sim P⊢Q$

1. $P\wedge \sim P$ (فرض)
2. $P$ (۱، حذف عطف)
3. $\sim P$ (۱، حذف عطف)
4. $\sim P\vee Q$ (۳، معرفی فصل)
5. $Q$ (۲، ۴، قیاس فصلی)

$P\to Q,Q\to R,P⊢R$

1. $P\to Q$ (فرض)
2. $Q\to R$ (فرض)
3. $P$ (فرض)
4. $Q$ (۱، ۳، وضع مقدم)
5. $R$ (۲، ۴، وضع مقدم)

$P\to Q,Q\to R,\sim R⊢\sim P$

1. $P\to Q$ (فرض)
2. $Q\to R$ (فرض)
3. $\sim R$ (فرض)
4. $\sim Q$ (۲، ۳، رفع تالی)
5. $\sim P$ (۱، ۴، رفع تالی)

پیوند به بیرون

• لابورئو، دانیل کلمنته، «مقدمه‌ای بر استنتاج طبیعی».
• دومینو روی اسید. استنتاج طبیعی به عنوان یک بازی دومینو تجسم شده است.
• پلتیه، جف، کتاب‌های درسی تاریخ استنتاج طبیعی و منطق ابتدایی.
• لوی، میشل، یک اثبات‌کنندۀ گزاره‌ای.