1. Формальна аксіоматична теорія

Формальна система (формальна аксіоматична теорія) — результат строгої формалізації теорії, що передбачає повне абстрагування від змісту слів використаної мови, причому всі умови, що регулюють використання цих слів у теорії, явно подано аксіомами і правилами виведення.

Означення 1. Формальну аксіоматичну теорію вважають визначеною, якщо справджуються такі умови:

1. Визначено деяку злічену множину символів цієї теорії. Скінченні послідовності цих символів називають виразами теорії.

2. Визначено підмножину виразів теорії, які називають формулами теорії.

3. Визначено деяку множину формул теорії, які називають аксіомами.

4. Визначено скінченну множину відношень між формулами, які називають правилами виведення. При цьому для кожного правила виведення R існує натуральне число n, при якому для довільної множини n формул і довільної формули A можна встановити, чи знаходяться дані n формул з формулою A у відношенні (правила виведення). Якщо відповідь ствердна, то формулу A називають безпосереднім наслідком даних n формул згідно з правилом R.

Аксіоми зазвичай поділяють на:

• логічні аксіоми, спільні для певного класу теорій;

• нелогічні або власні аксіоми, що визначають специфіку й зміст конкретної теорії.

Означення 2. Для визначеної формальної аксіоматичної теорії запровадимо такі поняття:

1. Виведенням у визначеній формальній аксіоматичній теорії називають будь-яку скінченну послідовність формул, у якій кожна формула:

   • або є аксіомою;

   • або є безпосереднім наслідком деяких попередніх формул згідно з одним із правил виведення.

2. Формулу A теорії називають теоремою, якщо в даній теорії існує виведення, у якому останньою формулою є дана формула. Таке виведення називають виведенням формули А.

3. Формулу А називають наслідком множини формул Н або кажуть, що з множини формул Н випливає формула А, якщо існує така скінченна послідовність формул, у якій А — остання формула, а кожна формула:

   • або є аксіомою;

   • або є елементом Н;

   • або є безпосереднім наслідком деяких попередніх формул згідно з одним із правил виведення.

   Таку послідовність формул називають виведенням А з Н. Елементи Н називають гіпотезами. Для скорочення викладу висловлювання «A є наслідком Н» і «з Н випливає А» записують так: Н┣ А.

У скороченому записі слів: «A є наслідком порожньої множини гіпотез» позначення для порожньої множини, як праволо, не використовують: ┣ A. Останній запис є також скороченим записом висловлювання «A є теоремою». Подамо кілька властивостей поняття виведення.

1. Якщо H є підмножиною G та Н┣ А, то G┣ А.

2. Н┣ А тоді й лише тоді, коли в Н існує скінченна підмножина G, при якій G┣ А.

3. Якщо Н┣А та всі елементи Н виводяться з G, то G┣ А.

Означення 3. Для визначеної формальної аксіоматичної теорії запровадимо такі поняття::

1. Теорію називають суперечливою, якщо всі її формулами є теоремами. Інакше її називають несуперечливою.

2. Теорію називають повною, якщо для довільної її формули або виводиться ця формула, або виводиться її заперечення. Інакше її називають неповною. В останньому випадку теорія містить висловлювання, які неможливо ні довести, ні спростувати в межах самої теорії.

3. Теорію називають розв'язною, якщо існує алгоритм, що для довільної формули за скінченну кількість кроків встановлює, чи існує її виведення. Інакше теорію називають нерозв'язною.

4. Окрему аксіому теорії називають незалежною, якщо її неможливо вивести з решти аксіом цієї теорії. Всю систему аксіом теорії називають незалежною, якщо кожна її аксіома є незалежною.

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

Предикат (лат. praedicatum — заявлене, згадане, сказане) — будь-яке вислов­лювання, в якому є щонайменше одна змінна.

Числення предикатів або логіка першого порядку — це формальна система математичної логіки, в якій допускають висловлювання відносно змінних, фіксованих функцій і предикатів.

2. Опис мови

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

Мову логіки першого порядку будуються на основі:

• множини функціональних символів;

• множини предикатних символів.

Наприклад, до предикатних символів теорії множин належать такі:

• ∈ — читати: «належить до (множини) (як елемент)»;

• = — читати: «дорівнює» або «збігається з».

З кожним функціональним і предикатним символом зв'язана арність (кількість агрументів). У логіці нульового порядку (численні висловлювань) функціональні та предикатні символи відсутні.

Додатково до цього використовують таке (далі сполучник «або» між символами означає, що у літературі зустрічаються усі перелічені позначення одного й того самого поняття):

• символи змінних, зазвичай a, b, c, …, x, y, z, a₁, b₁ і т.і. Передбачають зліченність символів, тобто можливість встановити взаємно однозначну відповідність між ними й підмножиною усіх натуральних чисел;

• оператор опису (дискрипції) ɩ — читати: «такий об'єкт, що ...» або «при якому». Це поняття відсутнє у численні висловлювань;

• логічні або пропозиційні зв'язки:

  • ¬ або ~ — читати: «не (справджується)»;

  • ∧ або & — читати: «i»;

  • ∨ — читати: «або»;

  • ⇒ або → або ⊃ — читати: «випливає»;

  • ⇔ або ↔ або ≡ або ~ — читати: «еквівалентно» або «(справджується) тоді й лише тоді, коли (справджується)»;

• кома, дужки ( і ) для структурування запису;

• квантори, відсутні у численні висловювань:

  • ∀ або ( ). — читати: «для всіх»;

  • ∃ або (E ). — читати: «існує», у тому числі ∃! — «існує єдиний».

Перечислені символи разом з функціональними й предикатними символами утворюють aлфавіт логіки першого порядку. Більш складні конструкції логіки першого порядку визначаються індуктивно:

• терм — це символ змінної або має вид ɩ x A чи f (x₁, x₂, …, x_n). Тут A — формула, f — функціональний символ арності n, а x₁, x₂, …, x_n — терми;

• атом має вид p (x₁, x₂, …, x_n), де p — предикатний символ арності n, а x₁, x₂, …, x_n — терми. Наприклад, якщо α і β — змінні або терми теорії множин, то (α ∈ β) і (α = β) є атомами. Зауважимо, що не всі автори виділяють атоми із сукупності формул, говорячи про атомарні формули;

• формула — це або атом, або одна з таких конструкцій: ¬A, (A ∧ B), (A ∨ B), (A ⇒ B), (A ⇔ B), ∀ x A та ∃ x A при довільних формулах A і B та змінній x.

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

У наступній таблиці істинності для двозначної логіки означено дію вже згаданих зв'язок і нових: штриха Шеффера | та стрілки Пірса ↓.

Серед логічних зв'язок можна видiлити ті, через які можна означити решту. Такі зв'язки називають елементарними. Як правило розглядають пари: (¬, ∧), (¬, ∨) чи (¬, ⇒). Однак і однією зв'язкою (штрихом Шеффера | чи стрілкою Пірса ↓) можна породити решту. Породити тут означає означити дію через дію елементарних зв'язок. Аналогічно, один з кванторів можна означити через заперечення ¬ й інший квантор. Використовують також знак, який читають: «запис ліворуч позначає те, що записано праворуч». Наприклад,

3. Аксіоми

Означення 4. Запровадимо такі поняття:

1. Змінну x називають зв'язаною у формулі F, якщо F має такий вигляд: ¬A, (A ∧ B), (A ∨ B), (A ⇒ B), (A ⇔ B), ∀ x A або ∃ x A, причому x уже зв'язана в A і B. Інакше змінну x називають незв'язаною у формулі F.

2. Формулу без незв'язаних змінних називають замкнутою формулою.

3. Теорією першого порядку називають довільну множину замкнутих формул.

Означення 5. Для довільних формул A, B, C формули (A1), (A2), (A3) є аксіомами числення висловлювань:

(A1)     (A ⇒ (B ⇒ A));
(A2)     ((A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C)));
(A3)     ((¬B ⇒ ¬A) ⇒ (¬B ⇒ A)).

Єдиним правилом виведення числення висловлювань слугує правило modus ponens: B є безпосереднім наслідком формул А і A ⇒ B. Інакше кажучи, якщо виведено формули A й A ⇒ B, то B також виведено. Традиційний запис цього правила такий:

Аксіоми числення предикатів — це вказані вже аксіоми (A1), (A2), (A3) і такі дві додаткові аксіоми:

(A4)     ∀ x A ⇒ A[t / x];
(A5)     ∀ x (A ⇒ B) ⇒ (A ⇒ ∀ x B), якщо змінна x не присутня у формулі А у незв'язному стані.

Правила виведення числення предикатів — це вже згаданий modus ponens (MP) та правило узагальнення:

В аксіомі (А4) формулу A[t / x] отримано внаслідок підстановки терму t замість змінної x у формулі A. Умови існування даної підстановки та її результат можна визначити індуктивно:

• якщо A — атом, то терм t може замінити довільну змінну x даної формули. Результат позначають A[t / x];

• якщо A має вигляд ¬B, тоді підстановка t замість x можлива тоді і лише тоді, коли така підстановка можлива для формули B. У цьому випадку A[t / x] збігається з ¬B[t / x];

• якщо A має вигляд B ⇒ C, тоді підстановка t замість x можлива тоді й лише тоді, коли така підстановка можлива для формул B і С. У цьому випадку A[t / x] збігається з B[t / x] ⇒ C[t / x]. З урахуванням того, що довільні логічні зв'язки можна означити через заперечення ¬ й імпікацію ⇒, поняття підстановки можна поширити на формули вигляду A ∧ B, A ∨ B, A ⇔ B, A | B та A ↓ B;

• якщо A має вигляд ∀ y B, тоді підстановка t замість x можлива у таких двох випадках:

  • змінна x зустрічається у формулі B лише у зв'язаному стані;

  • змінна y не зустрічається у термі t і підстановка t замість x можлива у формулі B.

  Результат визначають таким чином:

  • якщо x дорівнює y, то A[t / x] дорівнює ∀ y B;

  • якщо x не дорівнює y, то A[t / x] дорівнює ∀ y A[t / x]

  Враховуючи можливість означення одного з кванторів через заперечення й інший квантор, можемо поширити поняття підстановки на формули вигляду ∃ y B

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

4. Проблеми несуперечливості й повноти

Числення висловлювань є несуперечливою, повною, розв'язною теорією. Усі ці три твердження доводяться в рамках самої логіки висловлювань.

У 1931 році Курт Гьодель надрукував свою знамениту працю: «Про формально нерозв’язні твердження у «Принципах математики» і спорідених системах» (Godel K., Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatsh. Math. Phys., 38, 1931). У цій праці Гьодель дослідив дві найбільш відомі формальні системи математики — систему «Принципи математики» Б. Рассела і А.Н. Уайтхеда, а також аксіоматичну теорію множин Цермело — Френкеля. У них було формалізовано всі методи доведень, що використовуються в математиці, тобто доведення були зведені до сукупності деяких аксіом і правил виведення.

До публікації можна було припустити, що ці аксіоми і правила виведення достатні, щоб довести або спростувати будь-яке математичне твердження, яке можна формально виразити (записати) в цих системах. Виявилося, що таке припущення є хибним. У вказаних системах існують проблеми формальної арифметики, які є нерозв’язними, тобто які не можна ні довести, ні спростувати. І така ситуація є загальною, тобто не пов’язана зі специфікою формальних систем Рассела — Уайтхеда, Цермело — Френкеля чи інших систем.

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

Перша теорема Гьоделя стверджує: якщо формальна арифметика несуперечлива, то вона неповна.

Друга теорема Гьоделя стверджує: несуперечливість формальної арифметики не можна довести засобами самої формальної арифметики.

Отримані результати було поширено на всі найбільш відомі формально-аксіоматичні системи: Рассела — Уайтхеда, Цермело — Френкеля, Гільберта і т.і. Стало зрозуміло, що кожна достатньо багата і несуперечлива система необхідно неповна. Така неповнота має принциповий характер, бо її неможливо усунути поступовим приєднанням до системи нових аксіом. А для доведення несуперечливості системи внутрішніх її засобів недостатньо. Тому потрібно використати сильніші, зовнішні відносно системи засоби.

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