تصمیم‌پذیری (منطق)

در علم منطق، یک مسئله تصمیم‌گیری درست/نادرست موقعی تصمیم‌پذیر (به انگلیسی: decidable) است که روش کارآمدی برای به‌دست‌آوردن جواب صحیح برای آن موجود باشد. سامانه‌های منطقی مثل منطق گزاره‌ای موقعی تصمیم‌پذیر هستند که عضویت در مجموعه فرمول (یا قضیه) منطقی معتبر را بتوان به صورت کارآمد تعیین نمود. یک نظریه (مجموعه جمله‌های بسته تحت پیامد منطقی) در یک سامانه ثابت موقعی تصمیم‌پذیر است که روش کارآمدی برای تعیین آنکه آیا فرمول‌های اختیاری در نظریه موجودند، موجود باشد. بسیاری از مسائل مهم، تصمیم‌ناپذیر اند، یعنی اثبات شده‌است که هیچ روش کارآمدی برای تعیین عضویت (بازگشت جواب درست بعد از بررسی همه موارد، که این موارد محدود هستند ولی احتمالاً خیلی بزرگ‌اند) برای آن‌ها بتواند موجود باشد.

تصمیم‌پذیری در منطق، ناظر بر مسئله ای است که پاسخ به آن یکی از دو حالت درست و غلط یا یکی از دو حالت بله و خیر باشد. در صورتی که جواب یک مسئلهٔ تصمیم‌گیری با یک راه مؤثر^[۱] داده شود، آن مسئله تصمیم‌پذیر است. در یک راه حل مؤثر پاسخ درست به مسئله با طی گام‌های متناهی داده می‌شود. بسیاری از مسائل مهم تصمیم‌ناپذیر‌اند. هر نظریه یا سیستم منطقی تصمیم‌پذیر را می‌توان به صورت یک راه مؤثر یا یک تابع محاسبه‌کردنی توصیف کرد که بنا بر تز چرچ‐تورینگ این دو توصیف با هم معادل هستند.

سالیان طولانی ریاضی‌دانان در پی حل سوالاتی بودند که اکنون می‌دانیم حل شدنی نیستند. دانش در مورد تصمیم‌پذیری می‌تواند از چنین تلاش‌های بیهوده جلوگیری کند.

تصمیم‌پذیری یک سیستم منطقی

یک سیستم منطقی راهی است که در آن به صورت خودکار و با قواعد بازگشتی فهرستی از تمام صحیح‌های منطقی بخشی از منطق به دست می‌آید؛ به این صورت که یک دسته اصول و یک دسته قواعد استنباط با معیارهای صوری شناسایی می‌شوند و بعد از آن قضیه‌ها می‌توانند بر اساس اصول و قواعد استنباط به دست بیایند.^[۲]

یک سیستم منطقی در صورتی تصمیم‌پذیر است که بتوان برای هر فرمولی به این مسئلهٔ تصمیم‌پذیری با یک راه حل مؤثر پاسخ داد، که آیا آن فرمول می‌تواند جزو قضیههای آن سیستم باشد یا خیر.

تصمیم‌پذیری یک نظریه

یک نظریه مجموعه‌ای از فرمول‌ها است. این مجموعه تحت استلزام منطقی بسته‌است. اگر راه مؤثری برای پاسخ به این مسئله که یک فرمول عضو یک نظریه هست یا نه وجود داشته باشد، آن نظریه تصمیم‌پذیر است.

تصمیم‌پذیری یک زبان

می‌توان مسائل مختلف را با زبان‌ها مدل کرد و پاسخ بله یا خبر به یک سؤال را معادل عضویت یا عدم عضویت ورودی در زبان در نظر گرفت. در نظریهٔ زبان‌ها یک زبان در صورتی تصمیم‌پذیر است که بتوان ماشین تورینگی ساخت که آن را تصمیم بگیرد؛ به این معنا که ماشین تورینگی وجود داشته باشد که به ازای یک رشتهٔ ورودی، عضویت یا عدم عضویت آن در آن زبان را تعیین کند. چنین ماشین تورینگی به ازای هر ورودی‌ای متوقف می‌شود.^[۳]

برخی نظریه‌های تصمیم‌پذیر

برخی نظریه‌های تصمیم‌پذیر عبارتند از:^[۴]

مجموعهٔ اعتبارات منطقی مرتبهٔ اوّل با فقط یک علامت تساوی که در سال ۱۹۱۵ توسط Leopold Löwenheim^[۵] ثابت شد.
مجموعهٔ اعتبارات منطقی مرتبهٔ اوّل با یک علامت تساوی و یک تابع یگانی که که در سال ۱۹۵۹ توسط Ehrenfeucht ثابت شد.
نظریهٔ مرتبه‌اوّل اعداد طبیعی با علامت‌های جمع و تساوی که به آن محاسبات پرس‌برگر^[۶] هم گفته می‌شود.
نظریهٔ مرتبه‌اوّل اعداد طبیعی با علامت‌های ضرب و تساوی که به آن محاسبات اسکولم^[۷] هم گفته می‌شود.
نظریهٔ مرتبه‌اوّل جبر بولی که در سال ۱۹۴۹ توسط آلفرد تارسکی ثابت شد.
نظریهٔ مرتبه‌اوّل میدان‌های از نظر جبری بسته با توجه به یک ویژگی داده شده که در سال ۱۹۴۹ توسط تارسکی ثابت شد.
نظریهٔ مرتبه‌اوّل هندسهٔ اقلیدسی که در سال ۱۹۴۹ ثابت شد.
نظریهٔ مرتبه‌اوّل هندسهٔ هذلولوی که در سال ۱۹۵۹ ثابت شد.

برخی نظریه‌های تصمیم‌ناپذیر

عموماً برای ثابت کردن تصمیم‌ناپذیری نظریه‌ها از روش تفسیرپذیری استفاده می‌شود. اگر نظریهٔ اساساً تصمیم‌ناپذیر $T$ در نظریهٔ استوار $S$ تفسیرپذیر باشد، آن گاه $S$ نیز اساساً تصمیم‌ناپذیر است. این مفهوم به مفهوم کاهش چند-یک^[۸] در نظریهٔ رایانش‌پذیری نزدیک است.

برخی نظریه‌های تصمیم‌ناپذیر عبارتند از:^[۹]

نظریهٔ مرتبه‌اوّل اعداد طبیعی با عملگرهای ضرب، جمع و تساوی.
نظریهٔ مرتبه‌اوّل اعداد گویا با عملگرهای ضرب، جمع و تساوی.
نظریهٔ مرتبه‌اوّل گروه‌ها. شایان ذکر است که نه تنها نظریهٔ عمومی گروه‌ها، بلکه چند نظریهٔ خاص دیگر هم تصمیم‌ناپذیرند؛ مانند نظریهٔ گروه‌های محدود.

زبان‌های تصمیم‌پذیر و تصمیم‌ناپذیر شاخص

یک زبان به مجموعه‌ای از رشتهها گفته می‌شود. در تعریف هر کدام از زبان‌های زیر علامت $\langle \rangle$ در کنار یک شیء نشانگر نمایش آن شیء به صورت یک رشته‌است که می‌تواند مطابق هر قراردادی باشد.

زبان‌های تصمیم‌پذیر مربوط به ماشین‌های حالت‌متناهی و زبان‌های منظم

زبان رشته‌هایی نمایشگر یک ماشین حالت متناهی و یک رشته، که ماشین حالت متناهی رشته را قبول می‌کند یک زبان تصمیم‌پذیر است.^[۱۰]به این معنی که می‌توان یک ماشین تورینگ تعریف کرد، به قسمی که به ازای یک رشتهٔ ورودی عضویت یا عدم عضویت آن در $A_{dfa}$ را تصمیم بگیرد. عضویت یک رشته در $A_{dfa}$ به معنای این است که رشتهٔ مذکور نمایشگر یک ماشین حالت متناهی است که یک رشته را قبول می‌کند. $A_{dfa}=\{\langle B,\omega \rangle \ |B\,\,is\,\,a\,\,dfa\,\,that\,\,accepts\,\,\omega \}$
زبان رشته‌هایی نمایشگر یک ماشین حالت متناهی، که زبان آن ماشین (مجموعهٔ رشته‌هایی که قبول می‌کند) تهی است، یک زبان تصمیم‌پذیر است.^[۱۱] $L_{dfa}^{\phi }=\{\langle A\rangle \ |A\,\,is\,\,a\,\,dfa\,\,and\,\,L(A)=\phi \}$
زبان رشته‌هایی نمایشگر یک عبارت منظم و یک رشته، که آن عبارت منظم آن رشته را تولید می‌کند یک زبان تصمیم‌پذیر است.^[۱۰] $A_{REX}=\{\langle R,\omega \rangle \ |R\,\,is\,\,a\,\,regex\,\,that\,\,generates\,\,\omega \}$

زبان‌های تصمیم‌پذیر مربوط به زبان‌های مستقل از متن

هر زبان مستقل از متنی تصمیم‌پذیر است.^[۱۰]
زبان رشته‌هایی نمایشگر یک گرامر مستقل از متن و یک رشته که آن گرامر آن رشته را تولید می‌کند یک زبان تصمیم‌پذیر است.^[۱۲] $A_{cfg}=\{\langle G,\omega \rangle \ |G\,\,is\,\,a\,\,cfg\,\,that\,\,generates\,\,\omega \}$
زبان رشته‌هایی نمایشگر یک گرامر مستقل از متن که زبان آن گرامر (مجموعه رشته‌هایی که تولید می‌کند) تهی است یک زبان تصمیم‌پذیر است.^[۱۰] $E_{cfg}=\{\langle G\rangle \ |G\,\,is\,\,a\,\,cfg\,\,and\,\,L(G)=\phi \}$

زبان‌های تصمیم‌ناپذیر

زبان رشته‌هایی نمایشگر یک ماشین تورینگ و یک رشته که آن ماشین تورینگ آن رشته را می‌پذیرد تصمیم‌ناپذیر است.^[۱۳] $A_{TM}=\{\langle M,\omega \rangle \ |M\,\,is\,\,a\,\,TM\,\,and\,\,M\,\,accepts\,\,\omega \}$ $A_{TM}=\{\langle M,\omega \rangle \ |M\,\,is\,\,a\,\,TM\,\,and\,\,M\,\,accepts\,\,\omega \}$ از مکمل این زبان نیز تصمیم‌ناپذیر است. از تصمیم‌ناپذیری این زبان برای اثبات تصمیم‌ناپذیری زبان‌های دیگر استفاده می‌شود. اثبات تصمیم ناپذیری این به طریق زیر است.
- در صورتی که ماشین بالا وجود داشته باشد ماشین M را به این صورت می‌سازیم: این ماشین ماشین بالا را بر روی خود و ورودیش اجرا می‌کند، اگر پذیرفته شد نمی‌پذیرد و در غیر این صورت می‌پذیرد. وجود چنین ماشینی متناقض است زیرا در صورتی که ماشین بالا به این نتیجه برسد که M ورودی را می‌پذیرد نمی‌پذیرد.
زبان رشته‌هایی نمایشگر یک ماشین تورینگ و یک رشته که آن ماشین تورینگ به ازای آن رشته به عنوان ورودی متوقف می‌شود، تصمیم‌ناپذیر است. $HALT_{TM}=\{\langle M,\omega \rangle \ |M\,\,is\,\,a\,\,TM\,\,and\,\,M\,\,halts\,\,on\,\,input\,\,\omega \}$ $HALT_{TM}=\{\langle M,\omega \rangle \ |M\,\,is\,\,a\,\,TM\,\,and\,\,M\,\,halts\,\,on\,\,input\,\,\omega \}$
- برای اثبات این مسئله از تصمیم ناپذیری مسألهٔ قبل استفاده می‌کنیم. در صورتی که ماشین این مسئله وجود داشته باشد می‌توانیم برای هر ماشینی چک کنیم که متوقف می‌شود یا نه و در صورتی که متوقف می‌شود شبیه‌سازی‌اش کنیم و به این طریق زبان بخش قبل تصمیم گرفته شده‌است.

عموماً تصمیم ناپذیری زبان‌ها و مسائل متفاوت به این صورت اثبات می‌شود که نشان داده می‌شود در صورتی که آن‌ها تصمیم گرفته شوند مسائلی که می‌دانیم تصمیم پذیر نیستند (مثلاً مسائل بالا) تصمیم گرفته می‌شوند.

نیم‌تصمیم‌پذیری

نظریه‌ها و سیستم‌های صوری مشخصه‌ای ضعیف‌تر از تصمیم‌پذیری هم دارند که نیم‌تصمیم‌پذیری است. در صورتی که برای یک نظریه راه مؤثری وجود داشته بشد که همواره به‌طور صحیح مشخص کند که آیا یک فرمول عضو یک نظریه هست یا نه، امّا امکان این باشد که در صورت عضو نبودن فرمول در نظریه پاسخی ندهد، آن نظریه نیم‌تصمیم‌پذیر است. هر نظریه در صورتی تصمیم‌پذیر است که خودش و مکملش نیم‌تصمیم‌پذیر باشند و برعکس؛ بنابراین اگر نظریه‌ای تصمیم‌ناپذیر باشد خود یا متممش نیم تصمیم پذیر نیستند.

نیم‌تصمیم‌پذیری را می‌توان مشابه با تشخیص‌پذیری در نظریهٔ ماشین‌ها دانست. هر زبان تشخیص‌پذیر در این تشبیه مانند یک نظریهٔ نیم‌تصمیم‌پذیر است؛ برای این زبان ماشین تورینگی وجود دارد که به ازای رشته‌های عضو زبان به حالت قبول می‌رود، اما این ماشین به ازای رشته‌هایی که عضو زبان نیستند الزاماً متوقف نمی‌شود. در صورتی که یک زبان و مکمل آن تشخیص‌پذیر باشند آن زبان تصمیم‌پذیر است و برعکس؛ بنابراین به ازای هر زبان تصمیم‌ناپذیر خود آن زبان یا مکمل آن تشخیص ناپذیر است.

پانویس

↑ "Effective Method" (به انگلیسی).
↑ "Logic" (به انگلیسی). Retrieved 2017-12-29.
↑ Sipser، Micheal (۱۹۹۶). Introduction to the Theory of Computation. صص. ۱۷۷.
↑ 1930-، Monk, J. Donald (James Donald), (۱۹۷۶). Mathematical logic. New York: Springer-Verlag. شابک ۹۷۸۰۳۸۷۹۰۱۷۰۱.
↑ "Leopold Löwenheim" (به انگلیسی).
↑ "Presburger Arithmetic" (به انگلیسی).
↑ "Skolem Arithmetic" (به انگلیسی).
↑ "many-one reduction" (به انگلیسی).
↑ 1930-، Monk, J. Donald (James Donald), (۱۹۷۶). Mathematical logic. New York: Springer-Verlag. صص. ۲۷۹. شابک ۹۷۸۰۳۸۷۹۰۱۷۰۱.
↑ ^۱۰٫۰ ^۱۰٫۱ ^۱۰٫۲ ^۱۰٫۳ Sipser، Micheal (۱۹۹۶). Introduction to the Theory of Computation. صص. ۱۹۴–۲۰۰.
↑ S Akshay. «CS 208: Automata Theory and Logic» (PDF).
↑ «Decidable Languages» (PDF).
↑ «ATM is Turing Undecidable» (PDF). بایگانی‌شده از اصلی (PDF) در ۱۸ نوامبر ۲۰۱۷. دریافت‌شده در ۳۱ دسامبر ۲۰۱۷.

منابع

مشارکت‌کنندگان ویکی‌پدیا. «Decidability (logic)». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۲۹ آوریل ۲۰۲۱.

[1] "Effective Method" (به انگلیسی).

[2] "Logic" (به انگلیسی). Retrieved 2017-12-29.

[3] Sipser، Micheal (۱۹۹۶). Introduction to the Theory of Computation. صص. ۱۷۷.

[4] 1930-، Monk, J. Donald (James Donald), (۱۹۷۶). Mathematical logic. New York: Springer-Verlag. شابک ۹۷۸۰۳۸۷۹۰۱۷۰۱.

[5] "Leopold Löwenheim" (به انگلیسی).

[6] "Presburger Arithmetic" (به انگلیسی).

[7] "Skolem Arithmetic" (به انگلیسی).

[8] "many-one reduction" (به انگلیسی).

[9] 1930-، Monk, J. Donald (James Donald), (۱۹۷۶). Mathematical logic. New York: Springer-Verlag. صص. ۲۷۹. شابک ۹۷۸۰۳۸۷۹۰۱۷۰۱.

[:0-10] ۱۰٫۰ ^۱۰٫۱ ^۱۰٫۲ ^۱۰٫۳ Sipser، Micheal (۱۹۹۶). Introduction to the Theory of Computation. صص. ۱۹۴–۲۰۰.

[11] S Akshay. «CS 208: Automata Theory and Logic» (PDF).

[12] «Decidable Languages» (PDF).

[13] «ATM is Turing Undecidable» (PDF). بایگانی‌شده از اصلی (PDF) در ۱۸ نوامبر ۲۰۱۷. دریافت‌شده در ۳۱ دسامبر ۲۰۱۷.

[۱]

[۲]

[۳]

[۴]

[۵]

[۶]

[۷]

[۸]

[۹]

[۱۰]

[۱۱]

[۱۲]

[۱۳]