ВИЗНАЧЕННЯ ТА ВЛАСТИВОСТІ ФОРМАЛЬНОЇ СИСТЕМИ

Формальна система являє собою сукупність можливо абстрактних об'єктів (символів, позначень), взагалі кажучи, ніяк не пов'язаних із зовнішнім світом. У цій сукупності є правила оперування об'єктами (символами, позначеннями) в чисто синтаксичного трактуванні, спочатку без якого б то не було змісту (семантики) цього оперування.

Визначення . Формальною системою називається четвірка об'єктів М = <Г, Р, Л, Б>, де:

Т - кінцевий алфавіт (кінцеве безліч символів);

Р - безліч синтаксичних правил побудови формул із символів алфавіту;

А - кінцеве безліч аксіом , що представляє собою деяку підмножину безлічі формул;

В - кінцеве безліч правил виведення , які дозволяють отримувати з деякого кінцевого безлічі формул ? / ,, U 2 > ..., U p інше безліч формул lV h W 2 , ..., W n формальної системи і записуються у вигляді

Тут стрілка -> читається як «тягне» або «слід», формули t / ,, t / 2 , ..., U p називаються посилками , а кожна з формул W h W 2 , ..., W n називається висновком правила виведення.

Формальну систему іноді називають аксіоматикою , або формальної теорією.

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

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

Аксіоми формальної системи грають в ній ту ж роль, яку в геометрії грають її аксіоми, тобто використовуються в якості посилок в правилах виведення.

Правила виведення в формальної системі є аналогом логічних законів, які використовуються в геометричних міркуваннях. Результатом міркувань в геометрії є теореми. У формальній системі правила виведення використовуються для проведення доказів. Формальне доказ , або просто доказ , визначається як кінцева послідовність формул F ,, Р ь ..., /^.формальной системи, така, що кожна формула або є аксіомою, або за допомогою одного з правил виведення виведена з попередніх їй формул F l9 F 2 , F j9 де j <i. Деяка формула називається теоремою і позначається [F, якщо існує доказ F ] y F ly ..., F n в якому вона є останньою, т. Е. F = F. Звідси ясно, що будь-яка аксіома є теоремою. Докази у формальній системі є аналогами змістовних міркувань в геометрії і служать для отримання теорем. Відзначимо, що в наступному записі

{Аксіоми} е {теореми} з {формули} з {послідовності символів алфавіту}

всі включення множин є строгими.

Розрізняють два типи правил виведення:

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

є продукціям, де

S (х , у) означає, що «х є сином для у»,

F (x, у) - «х є батьком для у»,

GS (х, у) - «х є онуком для у »,

D (х, у) - «х є дочкою для у »,

В (х, у) - «х є братом для у».

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

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

дробом , залишаючи інші вирази формули без зміни. Застосування обох правил переписування, наведених вище як приклади, дозволяє спростити тригонометричну формулу cos х? tg х в два етапи:

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

Розглянемо приклад абстрактної формальної системи, для якої пізніше будуть дані дві різні інтерпретації.

Приклад. Формальна система ( JP).

  • 1. Алфавіт { а , Ь, ?}.
  • 2. Формули - це символ або будь-яка послідовність символів алфавіту.
  • 3. Одна аксіома: а ? а
  • 4. Одне правило виведення: с,? з 2 -> ЬС х ? ЬС 2

Тут символи з, і з 2 не є символами алфавіту, а грають службову роль. Символи з, і з 2 означають якісь послідовності символів а чи Ь.

З визначення даної формальної системи безпосередньо випливає, що її теоремами є тільки такі формули:

Очевидно, що, наприклад, формула baab ? abba не є теоремою.

Коли формальна система М = <Т, Р, А, В> визначена, тобто задані алфавіт Г, граматика Р, аксіоми А і правила виводу В , видається природним відповісти на наступні питання щодо системи М:

  • 1. Чи є аксіоми в А , які можуть бути виведені з інших аксіом?
  • 2. Чи є протиріччя в системі Л /, т. Е. Чи є формула У 7 , що формула У 7 і її заперечення -.У 7 обидві доказові в Ml
  • 3. Чи правда, що для будь-якої формули У 7 системи М доказовою є або сама формула У 7 , або її заперечення -.У 7 ?
  • 4. Чи існує така процедура, яка для кожної формули деїсти - ми М дозволяє встановити за кінцеве число кроків, чи є вона теоремою чи ні?
  • 5. Чи існує така інтерпретація формальної системи А /, що все її теореми стають справжніми твердженнями в цій інтерпретації?

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

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

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

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

  • 1) проглядаються зліва направо символи аналізованої формули і ведеться підрахунок символів Ь до символу а
  • 2) потім відразу за символом а повинен слідувати символ?:
  • 3) після нього повинні слідувати символи b в тій же кількості, що і на початку формули;
  • 4) за ними повинен слідувати один символ а , після якого формула закінчується.

Якщо ці чотири умови виконані, то аналізована формула теорії є теоремою. В іншому випадку вона є не-теоремою.

Нарешті, в п'ятому питанні з'ясовується, чи можна формальної теорії надати такий змістовний сенс, щоб її теореми відповідали справжнім твердженнями. Інакше кажучи, чи є модель формальної теорії. По суті змістовна модель являє собою звичайну виражену природним російською мовою наукову теорію в звичному розумінні цього слова: зі своїми об'єктами дослідження, методами і специфічними поняттями та ідеями. Не слід, правда, вважати, що моделлю обов'язково повинна бути якась відома змістовна наукова теорія. Роль моделі однієї формальної теорії цілком може виконувати інша формальна теорія або її частина. Якщо ствердно відповісти на п'яте питання, то це буде означати, що відповідної формальної теорії М зіставляється деяка інша (можливо також формальна) теорія А / ', в якій має сенс говорити про істинність і хибність її тверджень. В цьому випадку теорію М ', яка б вона не була, формальна або змістовна, називають моделлю теорії М. Так, звичайна арифметика, відома з шкільного курсу, служить моделлю для формальної арифметики. Інший цікавий приклад моделі буде розглянуто нижче. Він відноситься до змістовної інтерпретації неевклідової геометрії засобами геометрії Евкліда.

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