استنتاج طبیعی و حساب توالی
استنتاج طبیعی و حساب توالی دو سیستم صوری به سبک گنتزن هستند که اثباتها را از طریق قواعد معرفی و حذف برای رابطهای منطقی نشان میدهند و ماشینآلات اساسی نظریه اثبات ساختاری را تشکیل میدهند.
Definition
استنتاج طبیعی فرمولها را از مفروضات با استفاده از قواعد معرفی و حذف که منعکسکننده استدلال غیررسمی هستند، استخراج میکند، در حالی که حساب توالی، توالیها را، که ادعاهایی مبنی بر اینکه فهرستی از فرمولها مستلزم دیگری است، از طریق قواعدی که بر سمت چپ و راست یک استلزام عمل میکنند، دستکاری میکند.
Scope
این موضوع شامل قواعد استنتاج طبیعی با جفتهای معرفی و حذف آنها، ساختار حساب توالی با قواعد چپ و راست و قواعد ساختاری آن، نرمالسازی برای استنتاج طبیعی، رابطه بین دو سیستم، و انواع شهودی و کلاسیک آنها میشود.
Core questions
- چگونه قواعد معرفی و حذف به رابطهای منطقی معنا میبخشند؟
- یک توالی چیست و قواعد آن چگونه با قواعد استنتاج طبیعی تفاوت دارد؟
- نرمالسازی چگونه اثباتهای استنتاج طبیعی را ساده میکند؟
- نسخههای کلاسیک و شهودی این حسابها چگونه با هم مرتبط هستند؟
Key theories
- قواعد معرفی و حذف
- هر رابط توسط قواعدی که آن را معرفی میکنند و قواعدی که از آن بهرهبرداری میکنند، اداره میشود، و هماهنگی آنها، که حذف دقیقاً آنچه را که معرفی وارد میکند، بازیابی میکند، معنای رابط را بیان میکند.
- قضیه نرمالسازی
- پراویتز نشان داد که اثباتهای استنتاج طبیعی را میتوان به یک فرم نرمال عاری از انحرافات کاهش داد که در آن یک معرفی بلافاصله توسط یک حذف خنثی میشود، که مشابه حذف برش در استنتاج طبیعی است.
- تطابق دو حساب
- استنتاج طبیعی و حساب توالی قضایای یکسانی را اثبات میکنند و میتوانند به یکدیگر ترجمه شوند، با قواعد چپ توالی که با قواعد حذف استنتاج طبیعی مطابقت دارند.
Clinical relevance
این حسابها قالبهای استانداردی برای مطالعه ساختاری اثباتها هستند: استنتاج طبیعی از طریق تطابق اثباتها به عنوان برنامهها، زیربنای نظریه نوع و دستیاران اثبات است، در حالی که حساب توالی، با خاصیت زیرفرمول خود پس از حذف برش، اساس جستجوی اثبات خودکار و جداول تحلیلی است.
History
گنتزن هم استنتاج طبیعی و هم حساب توالی را در سالهای 1934 و 1935 معرفی کرد و حساب توالی را برای به دست آوردن قضیه حذف برش خود پس از یافتن تحلیل دشوارتر استنتاج طبیعی، ابداع کرد. پراویتز در سال 1965 استنتاج طبیعی را با یک مطالعه نرمالسازی کامل احیا کرد و این سیستمها در توسعههای بعدی اثباتها به عنوان برنامهها، محوری شدند.
Key figures
- Gerhard Gentzen
- Dag Prawitz
- Stanislaw Jaskowski
- Jan von Plato
Related topics
Seminal works
- troelstra2000
- prawitz1965
- negri2001
Frequently asked questions
- تفاوت بین استنتاج طبیعی و حساب توالی چیست؟
- استنتاج طبیعی با فرمولها در یک زمینه از مفروضات کار میکند و از قواعد حذف استفاده میکند که به شدت با اثبات غیررسمی مطابقت دارد. حساب توالی با استلزامهای صریح کار میکند و قواعد حذف را با قواعد معرفی چپ جایگزین میکند، قالبی که حذف برش و خاصیت زیرفرمول را شفاف میسازد.
- چرا نرمالسازی مهم است؟
- یک اثبات نرمال شامل هیچ انحرافی نیست و دارای خاصیت زیرفرمول است، بنابراین هر فرمول در آن یک زیرفرمول از نتیجه یا مقدمات است. این امر شکل اثباتها را محدود میکند، نتایج سازگاری را به دست میدهد، و از طریق تطابق اثباتها به عنوان برنامهها، با ارزیابی یک برنامه به یک مقدار مطابقت دارد.