Реферат Аксіоматичні системи логік 1-го порядку

Реферат - Аксіоматичні системи логік 1-го порядку

Аксіоматичні системи логік 1-го порядку

Аксіоматичні системи для логік 1-го порядку називають теоріями 1-го порядку. Під теорією 1-го порядку розумітимемо формальну систему T=(L, A, P), де L - мова 1-го порядку, A - множина аксіом, яка розбита на множину логiчних аксіом та множину власних аксiом, P - множина правил виведення. Логiчнi аксiоми присутнi у всiх теоріях 1-го порядку, власнi аксiоми визначають специфiку тієї чи iншої теорії.

5.1. ТЕОРІЇ 1-го ПОРЯДКУ

Множина логiчних аксiом задається такими схемами аксiом:

Ах1) ШFЪF - пропозицiйнi аксiоми;

Ах2) Fx[t]®$xF - аксiоми пiдстановки;

Ах3) x=x - аксiоми тотожностi;

Ах4) x1=y1®...®xn=yn® fx1...xn = fy1...yn та x1=y1®...®xn = yn ® px1...xn®рy1...yn - аксiоми рiвностi.

Множина P складається з наступних правил виведення:

П1) F |-YЪF - правило розширення.

П2) FЪF |-F - правило скорочення.

П3) FЪ(YЪX) |-(FЪY)ЪX - правило асоціативності.

П4) FЪY, ШYЪX |-YЪX - правило перетину.

П5) F®Y |-$xF®Y, якщо x не вiльна в Y, - правило $-введення.

Теоремою теорії 1-го порядку T називають формулу, яка виво-диться iз аксiом за допомогою скiнченної кiлькостi застосувань правил виведення. Множину теорем теорії T позначатимемо Th(T).

Те, що формула A - теорема, будемо позначати T |-A, або |-A, якщо T мається на увазi.

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

Сигнатурою теорії 1-го порядку називають сигнатуру мови цієї теорії. Формулу мови теорії називатимемо також формулою теорії.

Теорія T’ називається розширенням теорії T, якщо кожна формула теорії T є формулою теорії T’ та Th(T) Th(T’).

В цьому випадку теорію T називають звуженням теорії T’.

Розширення (звуження) T' теорії T називають простим, якщо T та T' мають однакові мови.

Теорії 1-го порядку T1 та T2 називаються еквiвалентними, якщо в них однаковi мови та множини теорем.

Розглянемо кiлька прикладiв теорій 1-го порядку.

Приклад 1. Теорія 1-го порядку, яка не мiстить власних аксiом, називається численням предикатiв 1-го порядку (скорочено ЧП-1).

Приклад 2. Елементарною теорiєю груп називається теорія 1-го порядку Gr сигнатури {, e, =}, де e – константний символ, - бiнарний функцiональний символ. Власнi аксiоми Gr такi:

G1) x (yz)=(xy)z;

G2) x(ex=x);

G3) x$y(yx=e).

Приклад 3. Особливе мiсце серед формальних теорiй займає теорiя натуральних чисел - формальна арифметика. Таку теорію позна-чимо Ar. Мовою Ar є мова Lar. Власнi аксiоми Ar такi:

Ar1) Ш(x+1=0);

Ar2) x+1=y+1®x=y;

Ar3) x+0=x;

Ar4) x+(y+1)=(x+y)+1;

Ar5) x0=0;

Ar6) x(y+1)=xy+x;

Ar7) Ax [0] &x(A®Ax [x+1])® |-xA - аксiоми iндукцiї.

Кожна власна аксiома формальної арифметики є IАФ.

Тeорeма 5.1.1. 1) Логiчнi аксiоми є всюди iстинними формулами.

2) Висновки правил П1 - П4 - тавтологiчнi наслiдки засновкiв.

3) Висновок правила П5 - слабкий логiчний наслiдок засновку.

Наслiдок. Кожна теорема ЧП-1 є всюди iстинною формулою.

Справдi, логiчнi аксiоми всюди iстиннi, а правила виведення зберiгають властивiсть всюди iстинностi.

Приклад 4. Умова "x не вiльне в Y" iстотна для П5. Справдi, x= 0®x=0 || $x(x=0)®x=0, бо x=0®x=0 всюди iстинна, a в силу ($x(x=0)®x=0)N (1)=F маємо N | $x(x=0)®x=0.

Приклад 5. Для П5 ||= не можна посилити до |=. Справдi, маємо x=0®1=0 ||=$x(x=0)®1=0, але ((x=0®1=0)®($x(x=0)®1=0))N (1)=F, тому x=0®1=0 | $x(x=0)®1=0.

Моделлю теорії 1-го порядку T називається iнтерпретацiя мови теорії, на якiй iстиннi всi власнi аксiоми теорії T.

Приклад 6. Моделлю ЧП-1 є кожна iнтерпретацiя його мови.

Приклад 7. Моделлю елементарної теорiї груп Gr є кожна група.

Приклад 8. Моделлю елементарної теорiї полiв Fl є кожне поле.

Приклад 9. Моделлю формальної арифметики Ar є N - стандартна iнтерпретацiя Lar. Таку модель називають стандартною моделлю формальної арифметики.

Формула називається iстинною в теорії T, якщо iстинна на кожнiй моделi теорії T.

Тeорeма 5.1.2 (тeорeма iстинностi). Кожна теорема теорії 1-го порядку T iстинна в T.

Тeорeма 5.1.3 (тeорeма тавтології). Кожна тавтологiя є теоремою.

Наслiдок. Якщо {1, ..., n}¦ та |-1, ..., |-n , то |-.

Приклади використання теореми тавтології (ТТ) розглянемо в наступному розділі.

ВПРАВИ

1. Визначити, вказавши мову та власні аксіоми, теорії 1-го порядку наступних математичних структур:

1) комутативної групи;

2) кільця;

3) кільця з одиницею;

4) комутативного кільця;

5) тіла (некомутативного поля);

6) поля;

7) частково впорядкованої множини;

8) лінійно впорядкованої множини;

9) решітки;

10) булевої решітки;

11) повної групи;

12) групи без кручень;

13) алгебраїчно замкненого поля;

14) впорядкованого поля дійсних чисел.

2. Доведіть незалежність кожної схеми логічних аксіом та кожного правила виведення від інших схем аксіом та правил виведення.

5.2. ПРИКЛАДИ ВИВЕДЕНЬ В ТЕОРІЯХ 1-го ПОРЯДКУ. ПОНЯТТЯ НЕСУПЕРЕЧЛИВОСТІ ТА ПОВНОТИ

Приклад 1. |-xA®А.

(Ах2) |-ШA®$xШA, звiдси за ТТ |-Ш$xШA®A, тобто |-xA®А.

Приклад 2 (правило -ввeдeння). Якщо |-A®B та x не вiльне в A, то |-A®xB.

Приклад 3 (правилa -дистрибутивності та -дистрибутивності). Якщо |-A®B, то маємо |-$xA®$xB та |-xA®xB.

Маємо |-A®B (умова) та |-B®$xB (аксiома Ах2), звiдки за TT |-A®$xB, тому за П5 дiстаємо |-$xA®$xB.

Приклади 2 та 3 дають змогу ввести похідні правила виведення:

- правило -вв : A®B |-A®xB, якщо x не вiльне в A;

- правило $-дис : A®B |-$хA®$xB;

- правило -дис : A®B |-xA®xB.

Приклад 4 (правило уособлення). Якщо |-xA, то |-A.

За прикладом 1 |-xA®A. Звiдси та з умови |-xА за МР |-A.

Приклад 5 (правило узагальнення).

Сторінки: 1 2 3