АКСІОМАТИЧНИЙ ПІДХІД

АКСІОМАТИЧНИЙ ПІДХІД

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

2 Фундаментальні властивості формальних теорій

3 Числення висловлень

4Автоматичне доведення теорем. Метод резолюцій

Формальні системиКожне числення Ф (або формальну систему) будемо будувати з використанням наступних понять:

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

Нехай а - деяка множина символів, яку називатимемо алфавітом. Найбільш типовими частинами алфавіту а будуть:

а! = {а,Ь,с,...} - пропозиційні змінні (або просто змінні);

аг = {х,у... х],у2,г,,...} - предметні змінні (або просто змінні);

«з = {/*' } - логічні зв’язки;

«4 = {<з0,а|;...} - константні символи;

а5 = {?рР"'} - предикатні символи;

а6 = } - функціональні символи;

а, - {=} - символи рівності;

«8 = - допоміжні символи (дужки).

Означення. Словами в алфавіті о: називаються скінченні впорядковані послідовності символів алфавіту. Кількість символів, що входить в слово, називається довжиною даного слова.

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

Означення. Слово В називається підсловом слова А, якщо А=СВО, де С і £> - деякі слово, можливо пусті. Якщо І - деякий символ з а і А=СЮ, то говорять про входження символу і в слово А.

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

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

Множину формул мови Ьа, що побудовані з допомогою правил Р, позначають РВа .

Будемо вважати, що серед логічних зв’язків алфавіту а обов’язково присутній символ заперечення, це вимагається для того, щоб можна було коректним чином поставити питання, що пов’язані з поняттям несуперечливості числення.

Введемо в користування метасимвол |- , який дозволить формулювати метатвердження про виведення фомул в численні Ф. Якщо Г - деяка скінченна множина формул РЬа, А - деяка формула з РЬа, то вираз виду Г|-ф А будемо в подальшому називати секвенцією. Формули з множини Г називаються гіпотезами або посилками, а формула А - наслідком даної секвенції.

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

Дуже часто задають не самі аксіоми, а схеми аксіом. Схеми аксіом - деякі схеми формул. Конкретна аксіома може бути отримана як варіант відповідної схеми аксіом заміною метасимволів, що позначають формули, конкретними формулами. Схеми аксіом будемо також називати просто аксіомами.

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

Основним логічним засобом отримання нових формул у численні є правша виведення.

Правилами виведення називаються вирази виду

Я:

(умови),

де Аи...,Ап і А - деякі формули. Метасимвол Я служить для назви або позначення даного правила. Формули А,,..., Ап називаються посилками правила Я, а формула А - безпосереднім наслідком посилок згідно даного правила Я. В дужках записуються умови при яких можна застосовувати правило Я до формул А,,..., А„. Ця частина правила може бути відсутньою, якщо жодних умов не накладається.

Для задання конкретного числення Ф виділимо деяке множину правил Я, яку будемо надалі називати правилами виведення для числення Ф.

Введемо поняття вивідності з гіпотез Г в числення Ф, де Г - деяка скінченна множина формул. Означення. Вивідністю з гіпотез Г в численні Ф, що задана аксіомами І] і правилами виведення Я, називається скінченна послідовність формул АІ,А2,...,АІІ така, що для кожного ї = 1,2,...,и формула А, є аксіомою з II або отримана з попередніх формул даної послідовності згідно з правил виведення Я (тобто є безпосереднім наслідком попередніх формул).

Означення. Говорять, що формула А вивідна з гіпотез Г в даному численні Ф і позначається через Г|-ф А, якщо існує вивідають з гіпотез Г в Ф, що закінчується даною формулою А.

Деякі загальні властивості виведення в численнях Лема (вивідність гіпотези). Г,А\-ФА Лема (перестановка гіпотез). Наступне правило

Г„А,В,Г2\-ФС

Г|,В,Д,Г2|-ФС

(Справедливе для довільного числення Ф.

Лема (скорочення гіпотез). Наступне правило

Г„Л,Л,Г2|-ФС

г„д,г2|-фс

справедливе для довільного числення Ф.

Лема (розширення гіпотез). Наступне правило

Г|-ФД Г,в|\-фА

справедливе для довільного числення Ф.

Саме числення (формальну систему) Ф(ІІ; Я), яка задана схемами аксіомам і/ і правилами виведення Я, ототожнюється з множиною всіх вивідних формул в Ф. Тобто:

А є Ф(і/ ;Я) тоді і тільки тоді, коли \-фА . < >Фундаментальні властивості формальних теорій множина А символів, які утворюють алфавіт; множина Я слів алфавіту А, які називаються формулами; гіідмножина І! формул, ІІаР, які називаються аксіомами; множина Я відношень Я на множині формул, ЯсР, ЯсЯп+ї, які називаються правилами /

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

Означення. Інтерпретація 1 називається моделлю множини формул ІУ, якщо всі формули цієї множини виконуються в інтерпретації І. Інтерпретація І називається моделлю формальної теорії З, якщо всі теореми цієї теорії виконуються в інтерпретації І (тобто всі формули що виводяться є істинними в даній інтерпретації).

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

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

Таким чином, формальна теорія підходить для опису тих множин, які є її моделями. Модель для формальної теорії 5 існує тоді й тільки тоді, коли 5 семантично несуперечлива.

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

Означення. Нехай множина М є моделлю формальної теорії 5. Формальна теорія 5 називається поєною (або адекватною), якщо кожному істинному висловленню М відповідає теорема теорії 8.

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

Означення. Якщо для множини М існує формальна повна несуперечлива теорія 8, то М називається такою, що формалізується.

Означення. Система аксіом формально несуперечливої теорії 5 називається незалежною, якщо жодна з аксіом не виводиться з решти за правилами виведення теорії 5.

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

Означення. Формальна теорія 5 називається розв ’язною, якщо існує алгоритм, який для будь-якої формули теорії визначає, чи є ця формула теоремою теорії. Формальна теорія 5 називається напіврозв'явною, якщо існує алгоритм, який для довільної формули А теорії може дати відповідь “так”, якщо А є теоремою теорії, і, можливо, не дати жодної відповіді, якщо Я не є теоремою (тобто алгоритм застосовується не до всіх формул).

Розрізняють: < >формальні теорії нульового порядку (числення висловлень ЧВ і числення секвенцій) формальні теорії першого порядку (числення предикатів ЧП і їх розширення) формальні теорії другого та вищих порядків. Числення висловлень кожна пропозиційне змінна є ПФ; такі ПФ назвемо атомарними; якщо Я та В є ПФ, то Я та Я=>В є ПФ. Я=>(Л=>Я) (Л=>(В=> С)) => ((А => В) => (А => С)) ЯлВ=>Я Ал В.=> В А=>(В=> АлВ) А => А V В (А => С) => ((В => С) => (А V В => С)) (Я=>В)=>((Я=>В)=>Я)І, Я => (Л => Я)

Г2 (Я => (Л => С)) => ((Я => 5) => (Я => С))

ІІ:ЯлЛ=>Я ІІ2ЯлЛ=>Л ІД (Я => В) => ((Я => С) => (Я => В л С))

' III 1Я=>ЯVЛ ІІІ2В=>Я^В ІІІз (Я С) => ((В => С) => (Я V Л => С))

IV: (Я => В) => (В => Я) ІУ2Я=>Я ІУ3Я=>Я.

Єдиним правилом виведення класичного числення висловлень є модус поненс (тобиз ропепз; скорочено МР) - правило, яке дозволяє з формул Я і А => В отримати формулу В. Формула В є безпосереднім наслідком формул Я і Я => В.

У відповідності з загальним визначенням, формальним доведенням в численні висловлень вважається така скінченна послідовність формул Я,,Я2,...,Я„, в якій кожна формула є аксіомою, або безпосереднім наслідком довільних двох попередніх формул. Формула Я називається теоремою в численні висловлень, якщо існує формальне доведення, що закінчується формулою Я; в даному випадку будемо писати |-А. Очевидно, що довільна аксіома доводиться в численні висловлень.

Приклад. Формально довести формулу II -> II. < >Запишемо аксіому Є2, заміна СІ, =11, =11, II2 = II -» V Запишемо аксіому Д з аналогічною заміною Застосуємо правило МР для 1,2 Запишемо аксіому Ь] із заміною II, = Д = Vп->(п->і/) (ьь о,=их=о)< >Застосуємо правішо МР для 3,4 /

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

існує скінченна послідовність формул А,,А2 А„, кожний член якої є або одним з припущень, або

теоремою числення висловлень, або випливає з попередніх членів послідовності за правилом МР.

Теорема (теорема про дедукцію). Для довільних формул А, В і множини формул Г, якщо Ги {А} |-В, то Г |-А=>В.

Метатсореми дедукції (МТГ)). Якщо Г - множина формул, V, В - формули і якщо Г|- V =» В, то

г,и\-в.

Приклад. Довести правило силогізму І], -> II2, (/2 -»• (731 £/3

Доведення. Припущення

1. (7, ->П2

г.и2-*и, < >и, ІІ2 (МР,1,3) г7,->(и2->-н3) і/, П2 ->(73 (МР.1,3) Пі (МР,2,4) cellspacing="0" width="100%"

г|-я-

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

Г,Я|-7?[endif]--

. Дане правило називається[endif]--

Г|-Л => В[endif]-- В">правил доведення. А саме, теорема про дедукцію виглядає так:

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

Г,Л|-В г, А\-В ,

вигляді такого допустимого правила: 1 г-=—1— (введення заперечення).

гМ

Правило виключення вивідної гіпотези. Правило

Г, а\- В; Г| -А Г|-В

справедливе в ЧВ.

Правила транзитивності. Правила

г|- (А => В); Г|-(В=>С) . Г,Л|-В; Г,В|-С Г|-(Л => С) 1 Г,А\-С

справедливі в ЧВ.

Правила контрапозиції. Правила

Т,А\-В . Т,в\-А

г,в|-л 1 т,а\-в

справедливі в ЧВ.

Розглянемо логічні символи, що служать для скорочення записів формул: (А а В) позначає формулу (А => В);

(А VВ) позначає формулу (А=> В).

Символи кон’юнкції і диз’юнкції використовуються як метасимволи. Теорема. В численні висловлень допустимі наступні правила виведення:

Назва правила

Запис правила дробом

Запис правила

Позначення

Правило введення диз’юнкції

Г | -А Г |-В Г|-Я V В ’ Г|-Л V В

а |-ауЬ Ь |-ачЬ

вд

Правило вилучення диз’юнкції

Г,А\-С Г,В|-С Т,А\/В\-С

а |-с

Ь \-с

то а V Ь |-с

влд

Правило введення кон’юнкції

Г - А Г -В Т\-А л В

а,Ь |-алЬ

вк

Правило вилучення кон’юнкції

Г|- А лВ Г|- А а В Г| -А ’ Г|-В

алЬ |-а алЬ |-Ь

влк

Правило силогізму

г|-А=>В Г|-В=>С Г|-Я=>С

а=>Ь Ь=> с то а => с

ПС

Правило перестановки посилок

Г|- А =>(В => С) Г|-В => (А => С)

а=>(Ь=> с) \- Ь^(а=> с)

ппе

Правило об’єднання посилок

Г|- А =>(В => С) Г|-Я а В => С

а=>(Ь=> с) |- аЬ => с

оп

Правило роз’єднання посилок

Г|-ЯлВ=>С г|-^ => (в С)

аЬ=>с\-

а=>(Ь=>с)

РП

Правило композиції

г|-л=>в г|-л=>с Г|-Я => В а с

а=>Ь а=> с І- а => Ьс

гас

Вилучення заперечення

т,а\-в г,а\-в

Т\-А

а \-Ь а (-Ь

то |-а

вз

Теорема тавтології (ТТ). Множина теорем числення висловлень співпадає з множиною тавтологій.

На практиці найчастіше використовується такий наслідок:

Наслідок. Якщо {Аі,..., А„} ^ А та |-Аі,..., |-А„, то |-А.

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

Із теореми тавтологій безпосередньо випливає: < >розв'язність числення висловлень: множина теорем числення висловлень алгоритмічно розв ’язна відносно множини всіх пропозиційних формул. несуперечливість: не існує про позиційної формули А такої, що \-А та |- А. Автоматичне доведення теорем. Метод резолюційА], Аг, ...,А„ |-В.

Даний вираз можна прочитати наступним чином: якщо посилки Я і, Аг, ...,А„ істинні, то істинний і висновок В.

Проблема виведення в логіці полягає в тому, щоб встановити чи істинна формула В, якщо формули істинні А\, Аг, ..., А„. В загальному випадку такий алгоритм неможливо побудувати, але в деяких випадках такі алгоритми існують. Доведення теореми рівносильно доведенню загальнозначущості деякої формули. Найбільш ефективне доведення загальнозначущості формул здійснюється методом резолюцій. Процедура пошуку доведення методом резолюцій фактично є процедурою пошуку спростування, тобто замість доведення загальнозначущості формули доводять, що заперечення формули суперечливе: А = 1 о А = 0.

Введемо термінологію, яка використовується при викладенні методу резолюцій.

Означення. Літерами будемо називати вирази А або А .

Означення. Літери А і А називають контрарними, а множину {А, А) - контрарною парою.

Диз ’юнкт - це диз’юнкція літер.

Означення. Диз’юнкт називається порожнім (позначається #), якщо він не містить літер. Порожній диз’юнкт завжди хибний, оскільки в ньому нема літер, які могли б бути істинними при будь-яких наборах змінних.

Правилом резолюцій називається наступне правило виведення:

А у В, АуС ВуС

Дане правило[endif]-- Розглянемо застосування методу резолюцій до числення висловлень.

єдине правило, що застосовується в методі резолюцій, що дозволяє не запам’ятовувати багато численні аксіоми і правила виведення. Його можна записати в наступному вигляді:

АуВ, АуС |- ВуС.

Приклад. Довести правило резолюцій, використавши рівносильності логіки:[endif]-- (АуВ)/\ (АуС) => (ВуС) = (АуВ)л(АуС) у(ВуС) = (А у В) у. (АуС)у (В у С) = АлВ у АлС у (В у С) = (Ау А) л (АуС)а (Ву А) л (ВуС) у (В у С) = (АуС)л (Ву А) л (ВуС) у (В у С)

-(А у С у В у С) л (В у А у В у С) л (В уС у В у С) = 1.

Отже, при істинних посилках істинний висновок. Доведено.

Означення. Диз’юнкт ВуС називається резольвентою для диз’юнктів А у В і АуС за літерою А:

ВуС= гєза(Ау В і АуС).

Якщо диз’юнкт не містить контрарних літер,-то резольвенти для них не існує. Для диз’юнктів А і А резольвентою є порожній диз’юнкт: гезЛ( А, А )= #.

Приклад. Нехай Р = А у В у С, О = А у В у О.

Тоді резольвентою

гезДР, С) = Ву Су В у О. гевц(Р, <Д)= Ау Су А у й.

ГЄ8с{Р, О) не існує.

Метод резолюцій відповідає методу доведення від супротивного. Дійсно, умова Ап (- В

рівносильна умові А1,Л2,...,Ап, В (-#.

Алгоритм побудови виведення методом резолюцій.

Крок 1. Побудувати кон’юкцію множини гіпотез А1,А2,...,Ап і заперечення висновку В; звести формулу А1 лЛ^ л...лЛп лВ доКНФ.

Крок 2. Побудувати множину 5 диз’юнктів з отриманої КНФ.

Крок 3. Замість пари диз’юнктів, що містить контрарні літери записати їх резольвенту за правилом резолюцій.

Крок 4. Продовжувати процес. Якщо він закінчується порожній диз’юнктом, то висновок обґрунтований.

Викладений алгоритм називається резолютивним висновком з 5.

Можливі три випадки: < >Серед множини диз’юнктів нема тих, що містять контрарні літери. Це означає, що формула В не виводиться з множини формул АІ,А2,..., Лп. В результаті наступного застосування правила резолюцій отриманий порожній диз’юнкт. Це означає, що формула В виводиться з множини А1,А2,...,Ап. Процес зациклюється, тобто отримуються все нові і нові резольвенти, серед яких нема порожніх. Це нічого не означає. А_ ' АуВ. В. В. (1,2) #.(3,4) /

#советы #продуктивность #таймменеджмент