Знаймо

Додати знання

приховати рекламу

Цей текст може містити помилки.

Формальна система



План:


Введення

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

Формальна система - це сукупність абстрактних об'єктів, не пов'язаних із зовнішнім світом, в якому представлені правила оперування безліччю символів в строго синтаксичної трактуванні без урахування смислового змісту, тобто семантики. Строго описані формальні системи з'явилися після того, як була поставлена ​​задача Гільберта. Перші ФС з'явилися після виходу книг Рассела і Уайтхеда "Формальні системи". Цим ФС були пред'явлені певні вимоги.


1. Основні визначення

Формальна теорія вважається визначеною, якщо [2] :

  1. Визнач кінцеве або рахункове безліч довільних символів. Кінцеві послідовності символів називаються виразами теорії.
  2. Є підмножина виразів, які називаються формулами.
  3. Виділено підмножина формул, які називаються аксіомами.
  4. Є кінцеве безліч відносин між формулами, які називаються правилами виводу.

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

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

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

Висновком називається всяка послідовність формул така, що будь-яка формула послідовності є або аксіома, або безпосереднє наслідок яких-небудь попередніх формул по одному з правил виводу.

Формула називається теоремою, якщо існує висновок, в якому ця формула є останньою.

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

Теорія, в якій не всі формули є теоремами, називається абсолютно несуперечливою.


2. Визначення та різновиди

Дедуктивна теорія вважається заданою, якщо:

  1. Задано алфавіт ( безліч) і правила утворення виразів ( слів) в цьому алфавіті.
  2. Задані правила освіти формул (правильно побудованих, коректних висловів).
  3. З безлічі формул деяким способом виділено підмножина T теорем (доказових формул).

3. Різновиди дедуктивних теорій

Залежно від способу побудови безлічі теорем:

3.1. Завдання аксіом і правил виводу

У безлічі формул виділяється підмножина аксіом, і задається кінцеве число правил виводу - таких правил, за допомогою яких (і тільки з допомогою їх) з аксіом і раніше виведених теорем можна утворити нові теореми. Всі аксіоми також входять до числа теорем. Іноді (наприклад в аксіоматиці Пеано) теорія містить нескінченну кількість аксіом, задаються за допомогою однієї або декількох схем аксіом. Аксіоми іноді називають "прихованими визначеннями". Таким способом задається формальна теорія (формальна аксіоматична теорія, формальне (логічне) обчислення).


3.2. Завдання тільки аксіом

Задаються тільки аксіоми, правила виведення вважаються загальновідомими.

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

3.2.1. Приклади

Геометрія

3.3. Завдання тільки правил виводу

Аксіом немає (безліч аксіом пусто), задаються тільки правила виводу.

По суті, задана таким чином теорія - окремий випадок формальної, але має власну назву: теорія природного виводу.

4. Властивості дедуктивних теорій

4.1. Суперечливість

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

4.2. Повнота

Теорія називається повною, якщо в ній для будь-якої формули F виведена або сама F , Або її заперечення \ Neg F . В іншому випадку, теорія містить недоведені твердження (твердження, які не можна ні довести, ні спростувати засобами самої теорії), і називається неповною.

4.3. Незалежність аксіом

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

4.4. Розв'язність

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

5. Найважливіші висновки

  • У 30-і рр.. XX століття Курт Гедель показав, що є цілий клас теорій першого порядку, які є неповними. Більше того, формула, яка стверджує несуперечність теорії, також невиведені засобами самої теорії (див. Теореми Геделя про неповноту). Цей висновок мав величезне значення для математики, так як формальна арифметика (а на ній базується теорія дійсних чисел, без якої не можна уявити сучасну математику) є якраз такою теорією першого порядку, а отже, формальна арифметика і всі теорії, що містять її, у тому числі теорія дійсних чисел, є неповними [ ].
  • Проблема нерозв'язності логіки предикатів. Черчем доведено, що не існує алгоритму, який для будь-якої формули логіки предикатів встановлює, логічно общезначима формула чи ні.
  • Обчислення висловлювань є несуперечливою, повної, вирішуваною теорією, причому всі три твердження доказові в рамках самої логіки висловлювань.

Примітки

  1. Кліні С. К. Введення в метаматематику - eqworld.ipmnet.ru/ru/library/books/Klini1957ru.djvu - М .: ІЛ, 1957. - С. 59-60.
  2. Мендельсон Е. Введення в математичну логіку - eqworld.ipmnet.ru/ru/library/books/Mendelson1971ru.djvu - М .: "Наука", 1971. - С. 36.

Література

Приклади формальних теорій
Формула Це заготовка статті по математиці. Ви можете допомогти проекту, виправивши або дописавши її.
Інформатика Це заготовка статті по інформатики. Ви можете допомогти проекту, виправивши або дописавши її.

Цей текст може містити помилки.

Схожі роботи | скачати

Схожі роботи:
Формальна мова
Формальна верифікація
Формальна верифікація
Формальна логіка
Формальна граматика
Формальна семантика
Система
Акустична система
© Усі права захищені
написати до нас
Рейтинг@Mail.ru