ФОРМАЛЬНІ СИСТЕМИ

Загальне уявлення про формальну системі

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

Під аксіоматичним методомрозуміється такий спосіб побудови наукової теорії, при якому в основу теорії кладуться деякі вихідні положення, звані аксіомами, а всі інші твердження теорії виходять як логічні наслідки аксіом. Геометрія є історично першої і аж до XIX ст. була єдиною аксіоматичної теорією. Вона дає найбільш наочний зразок формальної системи. Саме геометрія на початку XIX ст. дала поштовх розвитку аксіоматичного методу. Н. І. Лобачевський (1926 р) і Я. Бояи (1929 г.) зробили відкриття неевклідової геометрії. Вони встановили, що, замінивши звичний і, здавалося б, єдино «об'єктивно-істинний» V постулат Евкліда про паралельних його запереченням, можна розвивати чисто логічним шляхом геометричну теорію, настільки ж струнку і багату змістом, як і геометрія Евкліда. Цей факт привернув пильну увагу математиків XIX в. до дедуктивного (від загального до конкретного) способу побудови математичних теорій, що призвело до появи нової проблематики, пов'язаної з формальними системами.

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

Аксіоматизації арифметики дозволила звести вирішення питання про несуперечності багатьох математичних теорій (евклідова геометрія, геометрія Лобачевського, геометрія Рімана, проективна геометрія) до вирішення питання про несуперечності арифметики. У цьому полягає особлива роль арифметики серед інших математичних теорій. Зауважимо, що саме Дж. Псано, аксіоматізіруя арифметику, ввів в математичну логіку позначення, які використовуються і понині.

У роботах Г. Фреге (1879 г.), Б. Рассела і А. Н. Уайхеда (1910) ставилося глобальне завдання відомості всієї математики до логіки, т. Е. До формальних систем. Д. Гільберт ставив перед собою завдання обгрунтування всієї математики (вирішення питання про її несуперечності) засобами аксіоматичних систем. Пізніше, завдяки результатам К. Геделя (1930-ті рр.), Програма повної формалізації (аксіоматизації) математики, запропонована Д. Гильбертом, зазнала краху. До такого підсумку призвели наступні доведені Геделем теореми.

Перша теорема Геделя про неповноту. Будь-яка несуперечлива формальна система, що містить мінімум арифметики (операції додавання і множення і квантори V і 3), є неповною і непополнімой.

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

Якщо до двох теорем Геделя про неповноту додати теорему Г. Генцен, доведену їм пізніше (1960-ті рр.), Про те, що формалізована арифметика несуперечлива, то це дозволить зробити два висновки. По-перше (перша теорема Геделя про неповноту), арифметику ніколи не можна аксіоматизована «до кінця», т. Е. Арифметика не повна при будь-якій системі аксіом. Це означає, що при будь-якій системі аксіом арифметики в ній міститимуться затвердження, які не можна ні довести, ні спростувати. По-друге (друга теорема Геделя про неповноту), несуперечливість арифметики не може бути доведена засобами самої арифметики. Саме на шляху побудови мета-мета -...- теорії арифметики Г. Генцен знайшов доказ несуперечності арифметики.

Завершуючи загальну характеристику поняття «формальна система», відзначимо, що воно виникло в надрах формальної математичної логіки як засіб вивчення аксіоматичного методу, вперше використаного в «Засадах» Евкліда при побудові геометрії. Сама логіка як наука про правильні міркуваннях, починаючи з робіт Аристотеля (IV ст. До н. Е.), Зародилася і розвивалася в рамках філософії. І тільки в XIX в. з розвитком методів формалізації і символізації міркувань з'являється математична логіка як окремий розділ математики, що вивчає формальні системи.

Точне визначення формальної системи буде дано після розгляду основних ідей аксіоматичного методу на прикладі геометрії.

 
Переглянути оригінал
< Попер   ЗМІСТ   ОРИГІНАЛ   Наст >