حذف برش
حذف برش، قضیه گنتزن است که بیان میکند قاعده برش، که استفاده از لمها را رسمی میکند، میتواند از هر اثبات حساب توالی حذف شود و اثباتی را باقی بگذارد که تنها از فرمولهای مربوط به آن ساخته شده است.
Definition
حذف برش، قضیه و رویه سازندهای است که نشان میدهد هر استنتاج حساب توالی که از قاعده برش استفاده میکند، میتواند به استنتاجی تبدیل شود که از آن استفاده نمیکند، به طوری که هر توالی اثباتپذیر، اثباتی دارد که در آن تنها زیرفرمولهای توالی نهایی ظاهر میشوند.
Scope
این موضوع قاعده برش و نقش آن در حساب توالی، رویه حذف برش و خاتمه آن، خاصیت زیرفرمول اثباتهای بدون برش، نتایج حاصل از سازگاری و تصمیمپذیری، و محدودیتهای اندازه اثبات که حذف میتواند به همراه داشته باشد را پوشش میدهد.
Core questions
- قاعده برش چه چیزی را بیان میکند و چرا حذف آن مهم است؟
- رویه حذف برش چگونه خاتمه مییابد؟
- خاصیت زیرفرمول چیست و چه مفهومی برای جستجوی اثبات دارد؟
- هزینه محاسباتی حذف برش چقدر است؟
Key theories
- هاوپتساتز گنتزن
- قضیه اصلی گنتزن بیان میکند که قاعده برش در حساب توالی مجاز است، بنابراین هر اثباتی که از برشها استفاده میکند میتواند به یک اثبات بدون برش از همان توالی نهایی تبدیل شود.
- خاصیت زیرفرمول
- هر فرمولی که در یک اثبات بدون برش ظاهر میشود، زیرفرمول توالی نهایی است، که شکل اثبات را محدود میکند و مبنای رویههای تصمیمگیری و استدلالهای سازگاری است.
- سازگاری از طریق حذف برش
- از آنجا که یک اثبات بدون برش از توالی تهی غیرممکن است، حذف برش یک اثبات مستقیم ارائه میدهد که حساب، و در نتیجه نظریهای که آن را رسمی میکند، سازگار است.
Clinical relevance
حذف برش یک نتیجه بنیادی با پیامدهای گسترده است: اثباتهای سازگاری، خاصیت زیرفرمول که برای اثبات خودکار قضیه و روشهای تابلو ضروری است، قضایای درونیابی، و از طریق تطابق اثباتها به عنوان برنامهها، نرمالسازی برنامههای تایپ شده را به ارمغان میآورد.
History
گنتزن حذف برش، یا هاوپتساتز (Hauptsatz) خود را در سال ۱۹۳۴ برای منطق مرتبه اول اثبات کرد و این روش به سنگ بنای نظریه اثبات ساختاری تبدیل شد. تایت و ژیرار این تکنیک را به سیستمهای قویتر و منطق مرتبه بالاتر گسترش دادند و محدودیتهای رشد اندازه اثبات تحت حذف برش به موضوعی مستقل برای مطالعه تبدیل شد.
Key figures
- Gerhard Gentzen
- William Tait
- Jean-Yves Girard
- Gaisi Takeuti
Related topics
Seminal works
- takeuti1987
- troelstra2000
- negri2001
Frequently asked questions
- برش در یک اثبات چیست؟
- قاعده برش به فرد اجازه میدهد تا یک لم را اثبات کند و سپس از آن استفاده کند: از یک استنتاج که یک فرمول را اثبات میکند و دیگری که از آن فرمول به عنوان فرض استفاده میکند، نتیجه ترکیبی را استنتاج میکند. حذف برش نشان میدهد که چنین لمهای میانی همیشه میتوانند در اصل حذف شوند.
- چرا حذف برش میتواند اثباتها را بسیار طولانیتر کند؟
- حذف یک برش ممکن است نیاز به تکرار بخشهای بزرگی از یک استنتاج داشته باشد، و تکرار این کار میتواند اندازه اثبات را به صورت یک برج از توانها افزایش دهد. بنابراین اثباتهای بدون برش از نظر مفهومی سادهتر هستند اما میتوانند به طور قابل توجهی بزرگتر از اثباتهای اصلی با برش باشند.