در منطق و نظریهٔ برهان ، استنتاج طبیعی (به انگلیسی : Natural deduction ) نوعی حساب اثباتی میباشد که در آن استدلال منطقی با قواعد استنتاجی که نزدیک به روش «طبیعی» استدلال است، بیان میشود. این در تضاد با دستگاههای هیلبرت است که در عوض از بدیهیات تا حد امکان برای بیان قوانین منطقی استدلال استنتاجی استفاده میکنند.[ ۱]
یکی از قواعد استنتاج طبیعی، وضع مقدم است.[ ۱] [ ۲] بهطور شهودی، این قاعده بیان میکند که اگر بدانیم
P
{\displaystyle P}
مستلزم
Q
{\displaystyle Q}
است و بدانیم که
P
{\displaystyle P}
درست است، آنگاه میتوانیم نتیجه بگیریم که
Q
{\displaystyle Q}
[ ۱] که به این صورت میتوان آن را نوشت:
P
→
Q
,
P
⊢
Q
{\displaystyle P\to Q,P\vdash Q}
. نماد
⊢
{\displaystyle \vdash }
به این معنی است که از فرضهای
P
→
Q
{\displaystyle P\to Q}
و
P
{\displaystyle P}
، با قواعد استنتاج ثابت میکنیم (نتیجه میگیریم) که
Q
{\displaystyle Q}
.[ ۳] تعدادی دیگر از قواعد به این شکل هستند:[ ۱] [ ۲]
قاعدهٔ رفع تالی :
P
→
Q
,
∼
Q
⊢
∼
P
{\displaystyle P\to Q,{\mathord {\sim }}Q\vdash {\mathord {\sim }}P}
.
قاعدهٔ معرفی عطف:
P
,
Q
⊢
P
∧
Q
{\displaystyle P,Q\vdash P\land Q}
.
قاعدهٔ حذف عطف :
P
∧
Q
⊢
P
,
P
∧
Q
⊢
Q
{\displaystyle P\land Q\vdash P,\ P\land Q\vdash Q}
.
قاعدهٔ معرفی فصل :
P
⊢
P
∨
Q
{\displaystyle P\vdash P\lor Q}
.
قاعدهٔ حذف فصل:
(
P
→
Q
)
,
(
R
→
Q
)
,
(
P
∨
R
)
⊢
Q
{\displaystyle (P\to Q),(R\to Q),(P\lor R)\vdash Q}
.
قاعدهٔ قیاس فصلی:
P
∨
Q
,
∼
P
⊢
Q
{\displaystyle P\lor Q,{\mathord {\sim }}P\vdash Q}
.[ ۴]
P
∧
∼
P
⊢
Q
{\displaystyle P\land {\mathord {\sim }}P\vdash Q}
P
∧
∼
P
{\displaystyle P\land {\mathord {\sim }}P}
(فرض)
P
{\displaystyle P}
(۱، حذف عطف)
∼
P
{\displaystyle {\mathord {\sim }}P}
(۱، حذف عطف)
∼
P
∨
Q
{\displaystyle {\mathord {\sim }}P\lor Q}
(۳، معرفی فصل)
Q
{\displaystyle Q}
(۲، ۴، قیاس فصلی)
P
→
Q
,
Q
→
R
,
P
⊢
R
{\displaystyle P\to Q,Q\to R,P\vdash R}
P
→
Q
{\displaystyle P\to Q}
(فرض)
Q
→
R
{\displaystyle Q\to R}
(فرض)
P
{\displaystyle P}
(فرض)
Q
{\displaystyle Q}
(۱، ۳، وضع مقدم)
R
{\displaystyle R}
(۲، ۴، وضع مقدم)
P
→
Q
,
Q
→
R
,
∼
R
⊢
∼
P
{\displaystyle P\to Q,Q\to R,{\mathord {\sim }}R\vdash {\mathord {\sim }}P}
P
→
Q
{\displaystyle P\to Q}
(فرض)
Q
→
R
{\displaystyle Q\to R}
(فرض)
∼
R
{\displaystyle {\mathord {\sim }}R}
(فرض)
∼
Q
{\displaystyle {\mathord {\sim }}Q}
(۲، ۳، رفع تالی)
∼
P
{\displaystyle {\mathord {\sim }}P}
(۱، ۴، رفع تالی)