Розділ 4. МАТЕМАТИЧНА ЛОГІКА І ФОРМАЛЬНІ СИСТЕМИ
4.1. Вступ у формальні системи
Формальні системи - це системи операцій над об'єктами, що розуміються як послідовність символів (тобто як слова в зафіксованому алфавіті); самі операції також є операціями над символами. Термін "формальний" підкреслює, що об'єкти й операції над ними розглядаються чисто формально, без яких би то не було змістовних інтерпретацій символів. Передбачається, що між символами не існує ніяких зв'язків і відношень крім тих, що явно описані засобами самої формальної системи.
Якщо запропонувати читачу упорядкувати об'єкти 53, 109, 3, то, швидше за все, він без усяких додаткових питань розташує їх у порядку 3, 53,109. Інакше кажучи, цій задачі буде дана звичайна арифметична інтерпретація: послідовності цифр розглядаються як подання чисел у звичайній десятковій системі, упорядкування цих послідовностей є розташування чисел по зростанню, а правило порівняння таких зображень чисел відомо настільки добре, що звичайно про нього ніхто не замислюється.
У дійсності таке упорядкування не очевидне. Можливість неоднозначного витягу задач із тексту означає, що текст не містить формальної постановки задачі. Отже, необхідно чітко описати клас об'єктів, для яких задача розв'язується, і явно ввести для них поняття упорядкування, охарактеризувати його як систему локальних операцій над символами, з яких ці об'єкти складаються.
По суті при такому розумінні формальний опис системи означає її точний опис - усе, що істотно для розв'язання задачі. Таке уточнення задачі звичайно називають її формалізацією.
Приклади точного опису можна простежити на таких поняттях, як “алгоритм”, “дані” і т.п. У визначеному сенсі проблему точного опису деякої множини можна розглядати як проблему побудови алгоритму, що перераховує або породжує цю множину.
Так, приміром, визначення за допомогою формули - це опис множини, що перераховується, в якому використані всі істотні складові частини поняття алгоритм, крім одного - детермінованості. Відкидаючи несуттєвий тут порядок перерахування елементів множини, ми виграємо в компактності опису, що при цьому не стає менш відкритим. Такий опис, не будучи алгоритмом, являє собою формальну систему, що однозначно описує множину формул.
Історично теорія формальних систем виникла в рамках основ математики при дослідженні побудови аксіоматичних теорій і методів доказів у таких теоріях. З їхнього вивчення і починається знайомство з формальними системами.
4.2. Принципи побудови формальних теорій
Усяка точна теорія визначається, по-перше, мовою, тобто деякою множиною висловлювань, що мають зміст з погляду готової теорії, і, по-друге, сукупністю теорем - множиною мови, що складається із висловлювань, істинних у даній теорії.
Яким чином теорія одержує свої теореми?
У математиці з античних часів існував зразок систематичної побудови теорії - геометрія Евкліда, в якій усі вихідні передумови сформульовані явно, у виді аксіом, а теореми виводяться з цих аксіом за допомогою ланцюжків логічних міркувань, які називаються доказами. Проте до середини 19-го сторіччя математичні теорії, як правило, не вважали потрібним явно виділяти дійсно усі вихідні принципи. Критерії ж строгого доказу й очевидності тверджень у математиці в різні часи були різноманітні і також явно не формулювалися. Час від часу це призводило до необхідності перегляду основ тієї або іншої теорії. Відомо, наприклад, що основи диференціального й інтегрального числень, розроблених у 18-му сторіччі Ньютоном і Лейбніцем, у 19-му сторіччі піддалися серйозному перегляду. Математичний аналіз у його сучасному вигляді спирається на роботи Коші, Больцано, Вейєрштраса з теорії меж. Наприкінці 19-го сторіччя такий перегляд торкнувся загальних принципів організації математичних теорій.
Це призвело до створення нової галузі математики - основ математики, предметом якої стала саме побудова математичних теорій і тверджень і яка поклала собі за мету відповісти на запитання типу: "як повинна бути побудована теорема, щоб у ній не виникало протиріч? ”, “якими властивостями повинні володіти методи доказів, щоб вважатися достатньо строгими?”
Однією з фундаментальних ідей, на яку спираються дослідження з основ математики, є ідея формалізації теорій, тобто послідовного проведення аксіоматичного методу побудови теорій. При цьому не припускається користуватися якимись припущеннями про об'єкти теорії крім тих, що виражені явно у вигляді аксіом. Аксіоми розглядаються у вигляді формальних послідовностей символів (виразів), а докази - як методи одержання одних виразів з інших за допомогою операцій над символами. Такий підхід гарантує чіткість вихідних тверджень і однозначність висновків, проте, може скластися враження, що осмисленість і істинність в формалізованій теорії не відіграє ніякої ролі. У дійсності й аксіоми, і правила виведення прагнуть вибрати таким чином, щоб побудована з їхньою допомогою формальна теорія мала змістовний сенс.
Більш конкретно формальна теорія (або числення) будується в такий спосіб:
1. Визначається множина формул або правильно побудованих виразів, що утворять мову теорії. Ця множина задається конструктивними способами (як правило, індуктивним визначенням). Дана множина перерахована і часто розв'язувана.
2. Виділяється підмножина формул, які називаються аксіомами теорії. Підмножина може бути і нескінченною; у всякому разі, вона повинна бути розв'язувана.
3. Задаються правила виведення теорії. Правило виведення R(F1, … , Fn, σ) – це відношення, що обчислюється на множині формул. Якщо формули F1, … , Fn, σ знаходяться у відношенні R, то формула σ називається безпосередньо виведеною з F1, … , Fn за правилом R.
Часто правило R(F1, … , Fn, σ ) записується у вигляді (F1, … , Fn)/σ. Формули F1, … , Fn називаються посиланнями правила R, а σ - його наслідком або висновком. Приклади аксіом і правил виведення будуть наведені трохи пізніше. Виведенням формули В з формул A1, … , An називається така послідовність формул F1, … , Fm, що Fm = B, а будь-яка Fί (ί=1,2, … , m) є або аксіома, або одна з вихідних формул А1, … , Аn, або безпосередньо виведена з формул F1, … , Fί-1 (або якого-небудь із підмножин) по одному з правил виведення. Якщо існує виведення В з А1, …, Аn, то свідчать, що В виведена з A1, … , An. Цей факт позначається так: A1, … ,An├ B. Формули A1, … , An називаються гіпотезами або посиланнями виведення. Перехід у виведенні від Fί -1 до Fί називається і-м кроком виведення.
Доказом формули В в теорії Т називається виведення В з порожньої множини формул, тобто таке, в якому як вихідні формули використовуються тільки аксіоми. Формула В, для якої існує доказ, називається доказовою формулою в теорії Т або теоремою теорії Т; факт доказовості В позначається ├ В.
Очевидно, що приєднання формул до гіпотез не порушує вивідності. Тому якщо ├ В, то А ├ В, і якщо А1, . . ., Аn ├ В, то А1, . . ., Аn, Аn+1├ В для будь-яких А1 і Аn+1. Порядок гіпотез у списку несуттєвий.
При вивченні формальних теорій ми маємо справу з двома типами висловлювань: по-перше, із висловлюваннями самої теорії (теоремами), що розглядаються як чисто формальні об'єкти, визначені раніше, а по-друге, із висловлюваннями про теорію (про властивості її теорем, доказів і т.д.), що формулюються на мові зовнішній стосовно теорії - метамові і називаються метатеоремами. Різниця між теоремами і метатеоремами не завжди буде проводитися явно, але її обов'язково треба мати на увазі.
Наприклад, якщо вдалося побудувати виведення В з А1, . . ., Аn, то висловлювання “А1, . . . , Аn ├ В” є метатеоремою; її можна розглядати як додаткове (“довільне”) правило виведення, яке можна приєднати до вихідних і використовувати надалі.
Ясно, що загальнозначущі (тотожньо-істинні) висловлення типу А Ā або (x) (Y) мають силу загальних логічних законів і повинні входити в склад будь-якої теорії, що претендує на логічний сенс. Тому вивчення конкретних формальних теорій почнемо з числень, що породжують усі загальновідомі формули.