بخشی از مقاله
چکیده
منطق موجهات ۵S ی از مهم ترین منطق های موجهات بوده که دارای خواص بسیار خوبی از نظر نحو، معنا شناس و خواص جبری میباشد. عل رغم خواص خوب نحوی، جبری و معنا شناس ، همچنان ارائه ی یصوری سازی موفق درحساب رشته ها که دارای خاصیت حذف برش باشد با مش ل روبرو است. ی ازراهحل ها برای رسیدن به ی سیستم استنتاج که قضیه ی حذف برش در آنبرقرارباشد،حساب ابررشته ها است. در این مقاله،ضمن معرف حساب ابررشتهای برای منطق موجهات ۵S،به بررس اثبات های مختلف قضیه حذف برش در حسابهای ای ارائه شده م پردازیم.
واژه های کلیدی: منطق موجهات، حساب ابررشته ای، حذف برش.
١مقدمه
منطق موجهات ی از انواع منطق های صوری م باشد که در دهه ی ٠۶ میلادی معرف و گسترش یافته است. این منطق گسترش از منطق های گزاره ای و مرتبه اول بوده و دارایدو عمل ر وجه □ وم باشد که به ترتیب بیانگر »ضرورت« و »ام ان« در این منطق مباشند. در منطق موجهات جملات همانند»ضرورتا «p و یا »این ام ان وجود دارد که «pقابل ارائه و صوری سازی م باشند. معنا شناس منطق موجهات توسط کریپ۵۴، ارائه شد که بر پایه ی تعریف قاب۶۴، روابط دسترس پذیری٧۴ و جهان های مم ن م باشند.از منظر نظریهی برهان، نخستین صوری سازی ها در منطق موجهات بصورت سیستم اصل موضوع بودند که در واقع اصول مربوط به عمل رهای »ضرورتا« و »ام ان« به اصول موضوعه منطق گزاره ها اضافه م شدند. با توجه به اینکه چه اصول به منطق گزاره ها اضافه م شوند، نسخه های مختلف منطق موجهات به وجود م آیند.
همه ی منطقها ی موجهات در ی اصل و یقاعده مشترک م باشند که منطقهای موجهات نرمال٨۴، نامیده م شوند. ضعیف ترین منطق موجهات که به افتخار سائول کریپK نامیده م شود از اضافه کردن، قاعدهی □pp - قاعده ی گودل - و اصل توزیع K - □ - p ! q - ! - □p ! □q - - به اصول منطق گزاره ها بدست م آید. منطق K به عنوان منطق پایه ای پذیرفته م شود و با اضافه کردن اصل های دی ر به K، سیستم های دی رموجهات بدست م آیند. سیستم های مشهور در منطق موجهات بصورت زیر بهدست م آید:سیستم ۵S ی از مهمترین منطق های موجهات بوده که دارای خواص بسیار خوبی ازنظر نحو، معنا شناس و خواص جبری میباشد.در این مقاله تمرکز ما بر روی نظریه ی برهان منطق موجهات ۵S م باشد.
حساب رشتهها ٩۴ ی از سیستم های استنتاج مشهور است که اولین بار در سال ۴۳۹۱ توسط گنتسن ]٢[، ارائه گردید و به عنوان شالوده ی نظریهی برهان ساختاری٠۵ به حساب م آید. ی رشته١۵ در واقع عبارت به صورت :::; Bm ;۱:::; An ⊢ B ;۱A م باشد که معنای مورد نظرآن بهصورت B j - ۱Ai - ! - ∨j= ۱ - ∧i= م باشد.٢۵ی از مهمترین مفاهیم که در حساب رشته ها مورد بحث است قضیه ی حذف برش میباشد که اولین بار توسط گنتسن برای سیستمهای LK و LJ ارائه و اثبات گردیده است. قضیه ی حذف برش بیانگر این است که هر اثبات در حساب رشته ها که از قاعدهی برش استفاده م نماید معادل با اثبات بدون استفاده از قاعدهی برش م باشد. ارائه ی ی حساب رشته ای برای هر منطق که قضیه حذف برش در آن برقرار باشد از اهداف نظریه ی برهان م باشد و از این حقیقت منطق موجهات و به ویژه ۵S مستثن نیست. که قضیه حذف برش در به نظر م رسد بهترین راهحل ها برای رسیدن به ی سیستم استنتاج آن برقرار باشد در چارچوب حساب ابر رشتهها٣۵ بهدست م آید. ی ابررشته ۴۵ بهصورت j ___ j Gn ⊢ ∆n ۱⊢ ∆ ۱G است که به معنای برقراری از رشتههاست.
٢ حساب ابررشته ای برای منطق موجهات ۵S
مسئله ارائه ی حساب رشتهای برای ۵S که قضیه حذف برش در آن برقرار باشد دارای سابقهی طولان است. در مواجهه با این مساله دو نوع برخورد وجود داشته است؛ حساب رشته ای استاندارد و نااستاندارد.ﯾ از مش لات حساب رشته ای برای منطق موجهات، ارائه حساب رشته ای با حذف برش برای منطق ۵S م باشد. به عنوان مثال، اونیش و ماتسوموتو در سال ۷۵۹۱ ی حساب رشته ای با حذف برش برای ۵S ارائه کردند ول ایشان در مقاله بعدی خود در سال ۹۵۹۱ نشان دادند که حذف برش در این سیستم ارائه شده برقرار نیست. برای حل این مش ل، تعداد زیادی حساب رشته ای نااستاندارد ارائه شده است که هر کدام ازآنهاراهحل هایی برای اثبات قضیه حذف برش در این سیستم های نااستاندارد بدست میدهند.
علی رغم خواص خوب نحوی، جبری و معنا شناس ۵S، همچنان ارائه ی ی صوری سازی موفق در حساب رشته ها که دارای خاصیت حذف برش باشد با مش ل روبرو است و صوری سازی این منطق موجهات منجر به فرم های گسترش یافته و نا استاندارد زیادی از حساب رشته ها گردیده است. از چارچوب های مهم که به منظور صوری سازی منطق موجهات ۵S استفاده گردیده است م توان به حساب های ابر رشتهای اشاره نمود. در این مقاله، به صورت تفصیل به بررسی حساب های ابر رشته ای که تا کنون برای منطق موجهات ۵S ارائه گردیده است میپردازیم. از جمله این حساب ها م توان به حساب های ابر رشتهای
