خلاصة:
استنتاج طبیعی روشی صوری (Formal) برای اثبات و استنتاج قضایا در علم منطق است. یاکوفسکی و گنتزن از پیشگامان منطق جدید در سال ۱۹۳۴، مستقل از یکدیگر، این روش را به عنوان نظریه ای جایگزین برای روش اصل موضوعی پیشنهاد دادند. یاکوفسکی با ارایه دو روش گرافیکی و شرح نویسی و گنتزن با ارایه الگوی نمودار درختی، شیوه استنتاجی خود را مبتنی بر چند پیش فرض و تعدادی قاعده به اثبات رساندند که توجه منطق دانان را به خود جلب کرد و البته کواین با تیزبینی و زیرکی خاص خود، به وجود برخی کاستی ها پی برد و در نتیجه، محدودیت هایی را بر قواعد وضع شده درباره سورها ایجاد کرد. بعدها اندیشمندانی همچون کپی، فیچ و لمون، با الهام از کواین، قرایت های دیگری از استنتاج طبیعی عرضه کردند. در مقاله پیش رو، کوشیده ایم تا ضمن تبیین نظریه استنتاج طبیعی با روشی توصیفی، تاریخی و تحلیلی، مهم ترین دیدگاه های منطق دانان این حوزه را بررسی کنیم، تا با مقایسه میان این دیدگاه ها، نقاط قوت و ضعف آنها آشکار گردد.
Natural deduction is a formal method for proving and inferring the propositions in logic. In 1934, Jaskowski and Gentzen, the pioneers of modern logic, proposed this method independently of each other as an alternative to the axiomatic theory. Jaskowski by presenting graphical and annotation writing methods, and Gentzen by presenting a tree tableaus model, proved their deductive methods based on several presumptions and a number of rules that attracted the attention of logicians. However, Quine, with his special sharpness and acuteness, found out some shortcomings and put some restrictions on the rules laid down for quantifiers. Later, inspired by Quine, thinkers such as Copi, Fitch, and Lemmon offered other readings of natural deduction. Explaining the theory of natural deduction through a descriptive, historical and analytical method, this paper has examined the most important views of logicians in this field so that by comparing these views, their strengths and weaknesses are revealed.
ملخص الجهاز:
یاکوفسکی با ارائه دو روش گرافیکی و شرحنویسی و گنتزن با ارائه الگوی نمودار درختی، شیوه استنتاجی خود را مبتنی بر چند پیشفرض و تعدادی قاعده به اثبات رساندند که توجه منطقدانان را به خود جلب کرد و البته کواین با تیزبینی و زیرکی خاص خود، به وجود برخی کاستیها پی برد و در نتیجه، محدودیتهایی را بر قواعد وضع شده درباره سورها ایجاد کرد.
از ویژگیهای ممتاز این روش، آن Graphical Bookkeeping Restrictions Subproof Conditional subproof Conditional introduction Reduction ad absurdum است که قواعدی برای اعمال روی فرمولها دارد (مانند قاعده وضع مقدم 1 )، تنظیم و فرموله كردن 2 مجموعه قواعد استنتاجی، مهمترین نوآوری یاکوفسکی را نشان میدهد که همان بینیازی روش او از هر اصل موضوعه است.
روش گنتزن دارای ویژگیهای منحصر به فردی است؛ به طور مثال، برای قواعد استنتاج از حذف و معرفی، به صورت متقارن استفاده شده است.
تفاوت دیگری که کواین بین روش خود و روش گنتزن بیان میکند، در قاعده (E یا همان حذف سور وجودی است و میگوید: «گنتزن قاعدهای غیرمستقیم و انحرافی داشت و من در روش خودم به طور چشمگیری محدودیتهایی را روی قواعد وضع کردم؛ به خصوص با نشاندار کردن متغیرها از بسیاری اشکالات و ابهامات صوری و معنایی جلوگیری کردهام» (Quine, 1950b, p.
فیچ در استنتاج محمولات و قواعد حذف و معرفی سورها از متغیر آزاد، و برای حذف سور وجودی از برهانک استفاده میکند که سطر اول آن فرض است، و با ارائه محدودیتهایی از بروز ابهامات و اشکالات صوری و معنایی جلوگیری میکند.