Skip to main content
LibreTexts - Ukrayinska

13.4: Рішення проблеми

  • Page ID
    52949
  • \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)

    Template:MathJaxZach

    Ми говоримо, що логіка першого порядку вирішується, якщо існує ефективний метод визначення того, чи є дане речення дійсним чи ні. Як виявляється, такого методу немає: проблема вирішення обґрунтованості пропозицій першого порядку нерозв'язна.

    Для того, щоб встановити цей важливий негативний результат, доведено, що завдання рішення не може бути вирішена машиною Тьюринга. Тобто ми показуємо, що немає машини Тьюринга, яка, коли вона запускається на стрічці, яка містить речення першого порядку, врешті-решт зупиняється і виводить\(1\) або\(0\) залежно від того, чи є речення дійсним чи ні. За тезою Церква-Тьюринга, кожна обчислювана функція Тьюринга обчислюється. Так що, якби ця «функція валідності» були ефективно обчислювані взагалі, це було б обчислювальним Тьюрингом. Якщо це не обчислювальний Тьюринг, то він також не може бути ефективно обчислюваним.

    Наша стратегія доведення того, що проблема вирішення нерозв'язна, полягає в тому, щоб зменшити проблему зупинки до неї. Це означає наступне: Ми довели, що функція,\(h(e,w)\) яка зупиняється з виходом,\(1\) якщо машина Тьюринга, описана\(e\) зупинками на вході\(w\) та виходах\(0\) інакше, не є обчислювальною Тьюрингом. Ми покажемо, що якщо була машина Тьюринга, яка вирішує дійсність речень першого порядку, то існує також машина Тьюринга, яка обчислює\(h\). Оскільки\(h\) не може бути обчислений машиною Тьюринга, не може бути машина Тьюринга, яка вирішує дійсність.

    Перший крок у цій стратегії полягає в тому, щоб показати, що для кожного введення\(w\) і машини Тьюринга ми можемо ефективно описати речення\(M\),\(T(M, w)\) що представляє набір інструкцій,\(M\) а також введення\(w\) і речення. \(E(M, w)\)висловлюючи «\(M\)врешті-решт зупиняє» такі, що:

    \(\Entails T(M, w) \lif E(M,w)\)iff\(M\) зупиняється для введення\(w\).

    Основна частина нашого доказу буде полягати в описі цих речень\(T(M, w)\)\(E(M, w)\) та перевірці, що\(T(M, w) \lif E(M, w)\) є дійсним, якщо\(M\) зупиняється на введенні\(w\).