Алгоритмічні проблеми (стр. 7 из 7)

Мається точне поняття доведення твердження числення предикатів, причому твердження доводиться тоді і тільки тоді, коли воно істинно. У 1936 році Черч показав, що доведеність (і, отже, істинність) у численні предикатів нерозв'язна на відміну від більш простого пропозиціонального числення. (Гільберт вважав цей результат самим фундаментальної результатом, що стосується нерозв'язності, у всій математиці.)

Просте доведення нерозв'язності проблеми істинності можна дати з використанням МНР, хоча це вимагає деякого знайомства з численням предикатів. Читачу, що не знайомий з початками логіки предикатів, ми радимо пропустити приведений нижче зразок доведення.

5.1. Теорема.Проблема істинності числення предикатів першого порядку нерозв'язна.

Доведення. (Тим, хто не знайомий з численням предикатів, рекомендується пропустити.)

Нехай Р –деяка програма в стандартному виді, що містить команди I₁,…, I_s, і нехай u=r(P) (визначення див. § 2 р. 2). Ми будемо використовувати наступні позначення символів числення предикатів:

O – індивідний символ,

' – символ одномісної функції (значення якоїна хдорівнює х'),

R-символ (u+1) – місного відношення,

x₁, x₂,…, x_a, у – символи індивідних змінних.

Далі, для будь-якої команди I_i, можна записати твердження числення предикатів t_i, що описує результат виконання команди I_i. При цьому ми використовуємо символ Ù для позначення зв'язки «і» і символ ® для позначення імплікації. Твердження t_i, визначається в такий спосіб:

(a) якщо I_i=Z(n), тo t_i, є твердження

"x₁ … "x_u: R (x₁, …, x_n, …, x_u, i)®R (x₁, …, O, …, x_u, i ¢)

(b) якщо I_i=S(n), то t_i, є твердження

"x₁ … "x_u: R (x₁, …, x_n, …, x_u, i)®R (x₁, …, x_n¢, …, x_u, i ¢)

(c) якщо I_i=T (m, n), тo t_i, є твердження

"x₁ … "x_u: R (x₁, …, x_n, …, x_u, i)®R (x₁, …, x_m, …, x_u, i¢)

(d) якщо I_i=J (m, n, q), тo t_i, є твердження

"x₁ … "x_u: R (x₁, …, x_u, i)®((x_m = x_n®R(x₁, …, x_u, q))Ù(x_m¹ x_n ®R(x₁, …, x_u, i¢)))

Нехай тепер для будь-якого аÎ N символ

s_a позначає твердження.

(t₀Ùt₁Ù…Ùt_sÙ R (a, O,… O, 1))®$x₁ … $x_u R(x_{1, …,} x_u, s+1)

де t₀ є твердження "x"y((х'=у® x=y) Ù x¢¹O). (Це гарантує нам, що при будь-якій інтерпретації з т, n

Î N і m=n випливає, що т=п.)

Твердження R (a, O,…, О, 1) відповідає вихідному стану

а

0

0

…;

наступна командаIi

а будь-яке твердження R(x₁,…, х_u, s +1) відповідає зупинці (оскільки немає команди I_s+1). Ми покажемо, що

(*) Р (а)¯Ûs_a істинно.

Припустимо спочатку, що Р(а)¯ і що мається структура, у якій твердження t_0,…, t_s, і R (a, O,…, O, 1) виконуються. За допомогою тверджень t_0,…, t_s, ми одержуємо, що кожне з тверджень R(r₁,…. r_u, k),

що відповідають послідовним станам обчислення, також виконується. Зрештою ми приходимо до того, що для деяких b₁,…, b_uÎ N виконується твердження про зупинку R(b₁,…, b_u, s+1) і, отже, виконується твердження $x₁ …$x_u R(x₁,…, x_u, s+1). Таким чином, твердження s_a істинно.

Знову, якщо твердження s_a істинно, то воно виконується, зокрема, у структурі N, причому предикатний символ R інтерпретується як предикат R_a, для якого

R_a(a_1,…,а_u, k)ºНа деякому етапі обчислення Р (а) у регістрах містяться числа а₁, a₂,…, a_u, 0, 0,…, а наступна команда є I_k.

Тоді твердження t_0,…, t_s, і R (a, O,…, O, 1) також виконуються в цій структурі, а отже, і твердження $x₁ …$x_u R(x₁,…, x_u, s+1). Звідси Р(а)¯.

Якщо в якості Р узяти програму, що обчислює функцію y_u(x, х), то співвідношення еквівалентності (*) зводить проблему «x Î W_x» до проблеми «s істинно». Звідси випливає, що остання проблема нерозв'язна. ÿ

Математична логіка буяє результатами, що стосуються можливості розв'язання і нерозв'язності. Звичайно мова йде про задачі, у яких необхідно установити, чи буде деяке твердження істинним у всіх математичних структурах визначеного типу. Наприклад, було показано, що проблема «s є твердження, істинне для всіх груп» є нерозв'язною (s тут є твердження мовою числення предикатів першого порядку, що відповідає теорії груп), тоді як проблема «s є твердження, істинне для всіх абелевих груп» розв'язна. (При цьому прийнято говорити, що теорія груп першого порядку нерозв'язна, у той час як теорія абелевых груп першого порядку розв'язна.) Як було показано Тарським [1951], проблема «твердження s істинне в полі дійсних чисел» є розв'язної. З іншого боку, як ми побачимо в р. 8, багато проблем, зв'язаних з формалізацією арифметики натуральних чисел, нерозв'язні.

З іншими прикладами, а також з доведеннями багатьох результатів, що стосуються можливості розв'язання і нерозв'язності в математичній логіці, читач може ознайомитися в книгах Тарського, Мостовського і Робінсона [1953] чи Булоса і Джефрі [1974], а також Єршова [1981]*.