Повна версія

Головна arrow Природознавство arrow ІНТЕЛЕКТУАЛЬНІ СИСТЕМИ

  • Увеличить шрифт
  • Уменьшить шрифт


<<   ЗМІСТ   >>

НЕПОВНОТА ФОРМАЛЬНОЇ АРИФМЕТИКИ

Хоча для будь-якої несуперечливої теорії першого порядку Т існує несуперечливе повне її розширення Т ', це ще не означає існування алгоритму, що розпізнає по формулі, чи є вона аксіомою теорії Т' або хоча б перераховує все аксіоми цієї теорії. Гедель встановив, що будь-яка несуперечлива теорія першого порядку, для якої є алгоритм, що розпізнає її аксіоми, і до того ж включає в себе формалізацію найпростіших властивостей цілих невід'ємних чисел, обов'язково є неповною. Це твердження, відоме як теорема Геделя про неповноту формальної арифметики, часто згадується в зв'язку філософськими аспектами штучного інтелекту, і ми наведемо тут коротку схему міркувань, що лежать в основі його докази.

Перш за все, наведемо список аксіом, приєднання яких до загальних аксіомам логіки предикатів дає теорію першого порядку, звану формальної арифметикою. У цих аксіомах виділені наступні спеціальні символи: символ предметної константи, що позначається далі 0; функціональний символ арності 1, що позначається штрихом; функціональні символи арності 2, що позначаються знаками додавання і множення; предикатний символ арності 2, що позначається символом рівності. Нагадаємо, що мова логіки предикатів має рахункове безліч символів предметних констант і рахункове безліч функціональних або предикатних символів довільної арності. Аксіомами служать наступні формули:

Тут х % Х, Х 2 > Х 2 - довільні предметні змінні; Л (х) - довільна формула логіки предикатів.

Областю стандартної інтерпретації для формальної арифметики служить безліч цілих невід'ємних чисел; предметної константі 0 відповідає число 0; функціональному символу "штрих" відповідає операція додавання одиниці; додавання, множення і рівність розуміються звичайним чином. Остання з наведених вище схем аксіом є формалізацію принципу математичної індукції. Для будь-якого цілого невід'ємного числа до будемо позначати Т (к) терм, отриманий послідовним Ажратним застосуванням до 0 операції У стандартній інтерпретації значенням такого терма буде служити число к.

Ставлення R (x ... х п ), визначене на безлічі наборів цілих невід'ємних чисел, називається виразність у формальній арифметиці , якщо існує формула логіки предикатів А (х ... Х п ), така, що для будь-яких цілих невід'ємних чисел до , ..., k n :

а) Якщо R (ki ... k n ) істинно, то виведена формула

б) Якщо R (ki ... k n ) помилково, то виведена формула

Виводимість тут розуміється щодо аксіом формальної арифметики.

Функція /(xi...x n ), певна на безлічі наборів цілих невід'ємних чисел і приймаюча цілі невід'ємні значення, називається представимо у формальній арифметиці , якщо існує формула А (х i .. .x n x n + i), така, що для будь-яких цілих невід'ємних чисел до ... fc n > & n + i :

а) Якщо f (ki ... до п ) = до п + |, то виведена формула

б) що виводяться формула 3! x n + ii4 (T (A: i) ... T (fc n ) x n + i), де знак! після квантора існування - скорочена назва для формули, що виражає існування і єдиність.

Виділимо спеціальний клас арифметичних (тобто певних на множині цілих невід'ємних чисел та приймають цілі невід'ємні значення) функцій, який визначається індуктивним чином. Цей клас дає формалізацію поняття ефективно обчислюваною арифметичної функції, тобто такої функції, для обчислення значень якої існує алгоритм. Базис індукції складають наступні функції:

  • 1. Нуль-функція Z (x ), тотожно рівна 0;
  • 2. Функція додавання одиниці: N (x) = х + 1;
  • 3. Проектуючі функції: Ui > n (x .. .х п ) = х,

Операції, які породжують нові функції з раніше побудованих, такі:

1. Підстановка - отримання функції

з функцій д (у . ..2 / m ), M * i ..- х п ) 9 ... t h m (x i .. .x n );

2. Примітивна рекурсія - отримання функції

з функцій д (х 1 ... х п ), h {x ... х п + г) за допомогою співвідношень:

3. Мінімізація - отримання функції f (x .. п ) з функції д (х 1 ... x "+ i), для якої рівняння д (х ... х п у) = 0 має хоча б один корінь у при будь-якому наборі цілих невід'ємних х Значним функції f (x .. .х п ) є найменший із зазначених коренів у.

Функції, що належать заданому таким індуктивним визначенням класу, називаються рекурсивними. Якщо обмежитися лише операціями підстановки і примітивної рекурсії, то виникає власний підклас класу рекурсивних функцій, званий класом примітивно-рекурсивних функцій. Виявляється, що кожна рекурсивна функція бути подана в формальної арифметики, а кожне рекурсивне арифметичне відношення (тобто відношення на безлічі наборів цілих невід'ємних чисел, що має рекурсивну характеристическую функцію) виразність в ній. Доводяться ці твердження індукцією по визначенню класу рекурсивних функцій. Щоб за допомогою арифметичних відносин і функцій можна було визначати різні властивості кінцевих послідовностей символів в алфавіті мови логіки предикатів, вводиться спеціальна нумерація цих послідовностей. Спочатку символам s алфавіту зіставляються взаимнооднозначное їх номери N (s), після чого послідовності $ i, 52 , ... »Sk зіставляється номер .. cdotp ^ Sk Тут

Pi - просте число з номером г '; i = 1, ..., к. Легко бачити, що за своїм номером послідовність відновлюється однозначно. Тепер для таких властивостей слів в алфавіті мови логіки предикатів, як, наприклад, властивість бути термо, формулою, аксіомою, послідовністю формул, що представляє собою висновок, і т.п., можна розглядати відповідні арифметичні відносини для номерів слів. Цей прийом перекладу властивостей кінцевих послідовностей символів на арифметичний мову був запропонований Геделем і називається ге Делева нумерацією. Номер, що зіставляється слову зазначеним вище чином, називаємо гедеяевим номером цього слова.

Використовуючи твердження про виразність у формальній арифметиці будь-яких рекурсивних відносин, далі можна довести виразність у ній наступних двох відносин W (tz, v ) і W 2 {u, v):

  • 1. W {u , v) істинно тоді і тільки тоді, коли і - Геделя номер формули i4 (xi), що має вільну змінну xi (першу змінну списку предметних змінних алфавіту мови логіки предикатів), і v є Геделя номер деякого виведення в формальної арифметиці формули А {Т (і)).
  • 2. W 2 (u, v) істинно тоді і тільки тоді, коли і є Геделя номер формули i4 (xi), що має вільну змінну ii, і v є Геделя номер виводу в формальної арифметики формули - "Л (! Г (г / )).

Обидва ці властивості, вочевидь, допускають алгоритмічну перевірку, і доказ рекурсивності відносин IVi , W 2 зводиться, по суті, до звичайного програмування.

Розглянемо тепер формули U (xi, x 2 ), U 2 {xi, X 2 ), за допомогою яких виразність відносини, W 2 . Побудуємо формулу U наступного виду: V X3 {Ui (xi, x 2 ) - * Е Хз3 < х 2 & U 2 (x 1,3: 3))). Нехай п - Геделя номер цієї формули. Будуємо далі формулу V, одержувану підстановкою в U терма Т (п) замість змінної х х : V X2 (Ui (T (n), х 2 ) -> Е хз32 & U 2 (T (n) , x 3 ))).

Теорема Геделя про неповноту формальної арифметики (в так званій формі Россера, кілька підсилює початкове твердження Геделя) стверджує, що якщо формальна арифметика несуперечлива, то в ній не виводиться ні формула V, ні її заперечення, тобто вона неповна.

Сенс затвердження V досить прозорий: воно говорить, що якщо i2 є Геделя номер виведення затвердження V , то існує висновок заперечення твердження V, що має Геделя номер, що не перевищує зг 2 . Це - зручна в технічному відношенні версія затвердження, яке стверджує свою власну хибність. Як відомо, обидва припущення - про істинність або про хибність такого роду тверджень, відразу приводять до протиріччя. На цій стандартною схемою і побудовано доказ теореми. Завершальна його частина (після встановлення рекурсивності Wi, W 2 ) нескладна, і подробиці ми опустимо.

Зауважимо, що наведені міркування за аналогією можуть бути відтворені і для будь-якого розширення формальної арифметики, у якого безліч аксіом рекурсивно, тобто всі такі розширення неповні.

Звичайно, філософська інтерпретація теореми Геделя про неповноту як докази "принципової обмеженості аксіоматичного підходу" вимагає великої обережності. Ця у її доказі твердження не несе абсолютно ніякої змістовної інформації, стверджуючи лише свою власну хибність. Воно може бути сприйнято як приклад твердження абсолютно безглуздого і саме через свою безглуздість опиняється поза рамками дії аксиоматизации. З іншого боку, з математичної практики відомі конкретні приклади цілком змістовних тверджень, таких, як континуум-гіпотеза, що опинилися поза області дії загальноприйнятою аксиоматизации і таким чином виявили її неповноту. Теорема Геделя залишає відкритим питання про те, наскільки значною може виявитися неповнота Аксіоматизації, якщо обмежуватися розглядом в них лише досить осмислених і змістовних тверджень, подібних континуум-гіпотези.

З точки зору штучного інтелекту, який лише моделює логічні процеси природного інтелекту, теорема Геделя взагалі не накладає ніяких додаткових обмежень на перший, які були відсутні б для другого. Точно так же, як людина, виявивши незалежність будь-якого затвердження від наявної аксіоматики, починає розглядати дві незалежних гілки теорії або, спираючись на практику, вибирає одну з них, так і комп'ютерна модель, яка відтворює крок за кроком логіку міркувань людини, в принципі, могла б виконувати аналогічні дії.

 
<<   ЗМІСТ   >>