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

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

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

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

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

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

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

عموماً برای ثابت کردن تصمیم‌ناپذیری نظریه‌ها از روش تفسیرپذیری استفاده می‌شود. اگر نظریهٔ اساساً تصمیم‌ناپذیر ${\displaystyle T}$

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

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

یک زبان به مجموعه‌ای از رشتهها اطلاق می‌شود. در تعریف هر کدام از زبان‌های زیر علامت ${\displaystyle ⟨⟩}$

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

• زبان رشته‌هایی نمایشگر یک ماشین حالت متناهی و یک رشته، که ماشین حالت متناهی رشته را قبول می‌کند یک زبان تصمیم‌پذیر است.به این معنی که می‌توان یک ماشین تورینگ تعریف کرد، به قسمی که به ازای یک رشتهٔ ورودی عضویت یا عدم عضویت آن در${\displaystyle A_{dfa}}$
  را تصمیم بگیرد. عضویت یک رشته در${\displaystyle A_{dfa}}$
  به معنای این است که رشتهٔ مذکور نمایشگر یک ماشین حالت متناهی است که یک رشته را قبول می‌کند. ${\displaystyle A_{dfa}=\{⟨B,\omega ⟩|Bisadfathataccepts\omega \}}$
• زبان رشته‌هایی نمایشگر یک ماشین حالت متناهی، که زبان آن ماشین (مجموعهٔ رشته‌هایی که قبول می‌کند) تهی است، یک زبان تصمیم‌پذیر است. ${\displaystyle L_{dfa}^{\varphi }=\{⟨A⟩|AisadfaandL(A)=\varphi \}}$
• زبان رشته‌هایی نمایشگر یک عبارت منظم و یک رشته، که آن عبارت منظم آن رشته را تولید می‌کند یک زبان تصمیم‌پذیر است. ${\displaystyle A_{REX}=\{⟨R,\omega ⟩|Risaregexthatgenerates\omega \}}$

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

• هر زبان مستقل از متنی تصمیم‌پذیر است.
• زبان رشته‌هایی نمایشگر یک گرامر مستقل از متن و یک رشته که آن گرامر آن رشته را تولید می‌کند یک زبان تصمیم‌پذیر است.${\displaystyle A_{cfg}=\{⟨G,\omega ⟩|Gisacfgthatgenerates\omega \}}$
• زبان رشته‌هایی نمایشگر یک گرامر مستقل از متن که زبان آن گرامر (مجموعه رشته‌هایی که تولید می‌کند) تهی است یک زبان تصمیم‌پذیر است.${\displaystyle E_{cfg}=\{⟨G⟩|GisacfgandL(G)=\varphi \}}$

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

• زبان رشته‌هایی نمایشگر یک ماشین تورینگ و یک رشته که آن ماشین تورینگ آن رشته را می‌پذیرد تصمیم‌ناپذیر است. ${\displaystyle A_{TM}=\{⟨M,\omega ⟩|MisaTMandMaccepts\omega \}}$
  از مکمل این زبان نیز تصمیم‌ناپذیر است. از تصمیم‌ناپذیری این زبان برای اثبات تصمیم‌ناپذیری زبان‌های دیگر استفاده می‌شود. اثبات تصمیم ناپذیری این به طریق زیر است.
  • در صورتی که ماشین بالا وجود داشته باشد ماشین M را به این صورت می‌سازیم: این ماشین ماشین بالا را بر روی خود و ورودیش اجرا می‌کند، اگر پذیرفته شد نمی‌پذیرد و در غیر این صورت می‌پذیرد. وجود چنین ماشینی متناقض است زیرا در صورتی که ماشین بالا به این نتیجه برسد که M ورودی را می‌پذیرد نمی‌پذیرد.
• زبان رشته‌هایی نمایشگر یک ماشین تورینگ و یک رشته که آن ماشین تورینگ به ازای آن رشته به عنوان ورودی متوقف می‌شود، تصمیم‌ناپذیر است. ${\displaystyle HAL{T}_{TM}=\{⟨M,\omega ⟩|MisaTMandMhaltsoninput\omega \}}$
  • برای اثبات این مسئله از تصمیم ناپذیری مسألهٔ قبل استفاده می‌کنیم. در صورتی که ماشین این مسئله وجود داشته باشد می‌توانیم برای هر ماشینی چک کنیم که متوقف می‌شود یا نه و در صورتی که متوقف می‌شود شبیه‌سازی‌اش کنیم و به این طریق زبان بخش قبل تصمیم گرفته شده‌است.

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

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

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

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