Добавил:
Upload Опубликованный материал нарушает ваши авторские права? Сообщите нам.
Вуз: Предмет: Файл:

основи мат логіки

.pdf
Скачиваний:
17
Добавлен:
07.06.2015
Размер:
522.38 Кб
Скачать

О с н о в и м а т е м а т и ч н о ї л о г і к и

1. Принципи побудови формальних теорій

Математична логіка як самостійний розділ сучасної математики сформувався відносно нещодавно - на рубежі дев’ятнадцятого і двадцятого століть. Виникнення

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

Головним предметом у дослідженнях, присвячених «ліквідуванню» кризи і «рятуванню» математики, стали принципи або правила побудови математичних тверджень і математичних теорій, зокрема, пошук відповіді на питання типу: «як повинна бути побудована теорія, щоб у ній не виникало суперечностей або антиномій?», «які властивості повинні мати методи доведення, щоб їх можна було вважати строгими?» тощо.

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

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

Укінці ХIХ століття в зв’язку з виникненням кризи в канторівській теорії множин виникла потреба перегляду загальних принципів організації математичних теорій. Це привело до створення нової галузі математики - засад математики.

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

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

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

Унайзагальнішому вигляді формальну теорію T (інший термін - числення) будують таким чином.

1

1.Означають набір основних символів - алфавіт теорії.

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

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

4.Задають правила виводу (виведення) теорії.

Правило виводу R(F1,F2,...,Fm,G) - це відношення (або операція) на множині формул.

Якщо формули F1,F2,...,Fm,G знаходяться у відношенні R, то формула G називається безпосередньо вивідною з формул F1,F2,...,Fm за правилом R.

Часто правило виводу R(F1,F2,...,Fm,G) записують у вигляді

F1,F2,...,Fm .

G

Формули F1,F2,...,Fm називають припущеннями, посилками або гіпотезами правила R, а формулу G - висновком, наслідком або вислідом.

Виведенням (виводом, вивідністю) формули B з формул A1,A2,...,An називають послідовність формул F1,F2,...,Fm таку, що Fm=B, а будь-яка формула Fi, i=1,2,...,m є:

1)або аксіомою;

2)або однією з початкових формул A1,A2,...,An;

3)або безпосередньо вивідною з формул F1,F2,...,Fi-1 (або будь-якої їх підмножини) за одним з правил виведення.

Якщо існує виведення формули B з формул A1,A2,...,An, то кажуть, що B є вивідною з A1,A2,...,An і позначають цей факт так: A1,A2,...,An B. Формули A1,A2,...,An

називають посилками або гіпотезами виведення. Перехід у виведенні від формули Fi-1 до Fi називають i-м кроком виведення.

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

Формула B, для якої існує доведення, називається формулою довідною (вивідною) у теорії T, або теоремою теорії T; факт довідності формули B позначають B.

При вивченні формальних теорій існує два типи тверджень:

1)твердження самої теорії або її теореми;

2)твердження про теорію (про властивості її теорем, властивості доведень тощо).

Перші є елементами (словами, виразами, формулами) внутрішньої мови теорії, а другі - зовнішніми і формулюються у термінах мови, зовнішньої по відношенню до теорії і званої метамовою теорії; самі ці твердження називають метатеоремами.

Наприклад, якщо побудовано виведення формули B з A1,A2,...,An, то твердження

«A1,A2,...,An B» є метатеоремою; це твердження можна розглядати, як додаткове правило виводу, яке можна додати до початкових правил і використовувати у подальших конструюваннях доведень.

2

2. Алгебра висловлень

Носієм алгебри висловлень є множина так званих простих висловлень.

Просте (елементарне) висловлення (висловлювання) - це просте твердження,

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

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

Поняття простого (елементарного) висловлення, поняття істинності і хибності належать до первинних невизначальних понять математики, тобто вони не можуть бути означені через інші більш прості терміни та об’єкти, а пояснюються на прикладах, апелюючи до нашої уяви та інтуїції. До таких понять в математиці належать поняття «число», «пряма», «точка», «площина» тощо.

Наведемо декілька прикладів елементарних висловлень:

1)Київ - столиця України.

2)Число 7 є простим.

3)Число 10 більше від числа 3.

4)Усі натуральні числа є простими.

5)Множина всіх простих чисел є скінченною.

Перші три висловлення є істинними, а два останніх - хибними.

У той же час речення «Хай живе математична логіка!» або «Уважно прочитайте весь цей розділ» не є висловленнями.

Розглядаючи висловлення, виходитимо з двох основних припущень:

1)кожне висловлення є або істинним, або хибним (закон виключення третього);

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

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

Позначатимемо елементарні висловлення малими латинськими літерами: a,b,c,... (можливо, з індексами), а значення висловлень «Iстинно» і «Хибно» - відповідно символами 1 і 0 або I і Х.

Крім того, розглядатимемо так звані змінні висловлення, які позначатимемо латинськими літерами x,y,z,... (можливо, з індексами) і називатимемо також пропозиційними змінними. Після підстановки замість пропозиційної змінної певного елементарного висловлення ця змінна набуде відповідного значення: 0 або

1.

Сигнатура алгебри висловлень традиційно складається з таких операції:

заперечення, кон’юнкція, диз’юнкція та імплікація.

У таблиці 5.1 наведені різні назви та позначення, які використовують для зазначених операцій.

3

Таблиця 5.1

Назва

Позначення

Кон’юнкція

 

 

 

Логічне множення

 

 

 

Логічне «І»

 

 

 

Диз’юнкція

 

 

 

Логічне додавання

 

 

 

Логічне «АБО»

 

 

 

Заперечення

 

 

 

Логічне «НІ»

 

 

 

Імплікація

 

 

 

Логічне слідування

 

 

 

Використовуватимемо перші з наведених назв та позначень. Нижче подано таблицю 5.2, що містить означення цих операцій.

Таблиця 5.2

 

0

1

 

 

0

1

 

 

0

1

 

 

0

1

0

0

0

 

0

0

1

 

 

1

0

 

0

1

1

1

0

1

 

1

1

1

 

 

 

 

 

1

0

1

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

Алфавіт найбільш поширеної формальної мови алгебри висловлень складається

зтрьох груп символів:

1)символи елементарних висловлень та пропозиційних змінних: a,b,c,... і x,y,z,... (можливо з індексами);

2)символи операцій: , , , ;

3)допоміжні символи - круглі дужки: ( і ).

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

1)всі пропозиційні змінні та елементарні висловлення є формулами;

2)якщо A і B - формули, то вирази (A B), (A B), ( A), (A B) також є формулами;

3)інших формул, ніж побудовані за правилами 1) і 2), немає.

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

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

4

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

Нехай p1,p2,...,pn - це всі пропозиційні змінні, що входять у формулу A; будемо позначати цей факт A(p1,p2,...,pn). Формулі A(p1,p2,...,pn) поставимо у відповідність функцію f (p1,p2,...,pn), що означена на множині Bn (B={0,1}) і приймає значення у множині B, тобто функцію типу Bn B. Значення функції f на наборі значень a1,a2,...,an її змінних p1,p2,...,pn дорівнює значенню формули A(p1,p2,...,pn) при підстановці в неї замість пропозиційних змінних p1,p2,...,pn значень a1,a2,...,an відповідно.

Зауважимо, що кількість елементів в області визначення функції f дорівнює 2n, тобто |Pr1f |=2n.

Функцію f називають функцією істинності для формули A або відповідного складеного висловлення. Для функції істинності може бути побудована так звана таблиця істинності цієї функції (див.таблицю 5.3).

Таблиця 5.3

p1 p2 ......

pn-1 pn

f (p1,p2,...,pn-1,pn)

0

0 ...

0

0

f (0,0,...,0,0)

0

0 ...

0

1

f (0,0,...,0,1)

0

0 ...

1

0

f (0,0,...,1,0)

0

0 ...

1

1

f (0,0,...,1,1)

.........................

.....................

1

1 ...

1

0

f (1,1,...,1,0)

1

1 ...

1

1

f (1,1,...,1,1)

Серед формул алгебри висловлень особливе місце займають ті формули A(p1,p2,...,pn), які на всіх наборах (a1,a2,...,an) значень своїх змінних набувають значення 1.

Формула алгебри висловлень A(p1,p2,...,pn) називається тавтологією тоді і тільки тоді, коли їй відповідає функція істинності, яка тотожно дорівнює 1.

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

Наведемо приклади деяких важливих тавтологій:

(p ( p))

(закон виключення третього),

( (p ( p)))

(закон виключення суперечності),

(p p)

(закон тотожності).

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

Формула алгебри висловлень A(p1,p2,...,pn), яка набуває значення 0 на всіх наборах (a1,a2,...,an) значень своїх пропозиційних змінних, називається

суперечністю, або тотожно хибною формулою.

5

Формулу, яка не є ні тавтологією, ні суперечністю, називають нейтральною. Множина всіх формул алгебри висловлень розбивається на тавтології,

суперечності та нейтральні формули.

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

1.Заперечення тавтології є суперечністю і навпаки.

2.Кожна тавтологія є виконуваною формулою (навпаки, взагалі кажучи, ні).

3.Кожна нейтральна формула є виконуваною, але не навпаки.

4.Заперечення виконуваної формули може бути, як виконуваною формулою, так і невиконуваною формулою.

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

допомогою знака = ( або ): записують A=B (A B або A B).

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

Наведемо приклади пар рівносильних формул:

(A B) = (( A) B), ( (A B)) = (( A) ( B)), ( (A B)) = (( A) ( B)), (A (B C)) = ((A B) (A C)), (A (B C)) = ((A B) (A C))

тощо.

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

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

Наведемо лише два міркування, які демонструють, що перше враження є обманливим.

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

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

6

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

Проблема розв’язності займає важливе місце в математичній логіці. До проблеми розв’язності зводиться багато різних задач математичної логіки.

Наприклад, до проблеми розв’язності може бути зведена обговорювана вище проблема перевірки рівносильності заданих формул A і B.

Легко довести таку теорему.

Теорема 5.1. Формули алгебри висловлень A і B рівносильні тоді і тільки тоді, коли формула ((A B) (B A)) є тавтологією.

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

Отже, останню теорему можна сформулювати так.

Формули A і B рівносильні тоді і тільки тоді, коли формула (A~B) є тотожно істинною.

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

Нехай A(p1,p2,...,pn) і B(p1,p2,...,pn) - дві формули алгебри висловлень. Будемо говорити, що формула B(p1,p2,...,pn) є логічним слідуванням формули A(p1,p2,...,pn), якщо B приймає значення 1 для всіх тих наборів значень пропозиційних змінних, для яких формула A істинна (тобто приймає значення 1); позначатимемо це A B.

Це означає, що множина наборів значень змінних, для яких істинна формула A,

єпідмножиною множини наборів значень змінних, для яких істинна формула B, що

єлогічним слідуванням формули A.

Приклад 5.1. Формула B(x,y,z)=(x z) є логічним слідуванням формули A(x,y,z)=((x y) z) , що випливає з відповідних таблиць істинності (див.табл.5.4).

Таблиця 5.4

x y z

A B

0 0 0

0

0

0 0 1

0

1

0 1 0

0

0

0 1 1

1

1

1 0 0

0

1

1 0 1

1

1

1 1 0

0

1

1 1 1

1

1

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

7

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

Проблема перевірки чи є формула B логічним слідуванням іншої заданої формули A також може бути зведена до проблеми розв’язності для певної формули алгебри висловлень.

Теорема 5.2. Формула B(p1,p2,...,pn) є логічним слідуванням формули A(p1,p2,...,pn) тоді і тільки тоді, коли тотожно істинною є формула (A B).

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

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

табличною.

Iншим методом побудови логічного числення є описаний вище формальноаксіоматичний метод. Саме за допомогою цього методу побудовано так зване числення висловлень.

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

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

1. Алфавіт числення висловлень складається з елементарних і змінних висловлень (пропозиційних змінних): a,b,c,d,...,x,y,z (можливо з індексами), знаків логічних операцій , , , і круглих дужок ( та ).

2. Поняття формули означається аналогічно алгебрі висловлень.

а) всі пропозиційні змінні та елементарні висловлення є формулами;

б) якщо A і B - формули, то вирази (слова) (A B), (A B), ( A), (A B) також є формулами;

в) інших формул, ніж побудовані за правилами а) і б) немає.

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

8

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

Зокрема, звичайно, опускають зовнішні дужки формул та замість ( A) записують

A;

3. Аксіомами числення висловлень будуть такі формули:

A1. a (b a)

A2. (a b) ((a (b c)) (a c)) A3. (a b) a

A4. (a b) b

A5. (a b) ((a c) (a (b c)))

A6. a (a b) A7. b (a b)

A8. (a c) ((b c) ((a b) c)) A9. (a b) (b a)

A10. a a

4. Правилами виведення є:

1)правило підстановки. Якщо A - вивідна формула, яка містить літеру p (позначимо цей факт A(p)), то вивідною є і формула A(B), що здобувається з A заміною всіх входжень літери p на довільну формулу B; записується

A(p) A(B)

2)правило висновку (modus ponens). Якщо A і A B - вивідні формули, то вивідною є й формула B; записується

A, A B

B

У поданому описі числення висловлень аксіоми є формулами числення (відповідними до означення формули); формули, що використовують у правилах виведення (A, A B тощо), є метаформулами, або так званими схемами формул.

Схема формул - це вираз метамови для позначення нескінченної множини всіх тих формул числення, які отримують після заміни змінних метамови (метазмінних) цієї схеми певними формулами числення.

Наприклад, для схеми формул A B, якщо замінити A на p, а B - на p q, то з даної схеми отримаємо формулу числення p (p q); якщо ж метазмінну A замінити на p q, а B - на (p q) p, то дістанемо формулу (p q) ((p q) p) тощо.

Використання схем формул можна поширити і на всі аксіоми. Наприклад, якщо в системі аксіом пропозиційні змінні a,b,c замінити метазмінними A,B,C, то отримаємо десять схем аксіом, що задають десять нескінченних множин аксіом. Таким чином приходимо до іншого способу побудови числення висловлень: з нескінченною множиною аксіом (що задається скінченним числом схем аксіом),

але без правила підстановки,

оскільки

воно неявно

міститься у поясненні

(інтерпретації) схем аксіом.

 

 

 

Перший

спосіб є більш послідовно конструктивним: всі його засоби явно

зафіксовані

і скінченні; при

введенні

числення в

ЕОМ (наприклад, для

9

автоматизації доведень теорем та побудови виведень для заданих формул) він виглядає природнішим.

З іншого боку, другий спосіб більш відповідає математичній традиції тлумачення (інтерпретації) формул: наприклад, алгебраїчна тотожність (a+b)2=a2+2ab+b2 або відомі логарифмічні чи тригонометричні тотожності тлумачаться саме як схеми тотожностей, а не конкретні тотожності, справедливі лише для конкретних літер. Правило підстановки при цьому мається на увазі і присутнє неявно. Втім, досить очевидно, що перехід від одного способу побудови числення до іншого є нескладним.

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

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

Розглянемо приклади виведення теорем ЧВ.

Приклад 5.2. Доведемо, що формула a a є теоремою ЧВ.

1) Підставляючи в аксіому A2 змінну a замість змінної c і b a замість b, матимемо вивідну формулу

(a (b a)) ((a ((b a) a)) (a a))

2) Підформула a (b a) є аксіомою A1. Тоді з вивідних формул a (b a) і (a (b a)) ((a ((b a) a)) (a a))

за правилом висновку виводимо формулу

(a ((b a) a)) (a a)).

3)Замінимо в аксіомі A1 b на (b a): a ((b a) a).

4)Знову, застосовуючи правило висновку до двох останніх формул, матимемо,

що формула a a є вивідною.

Для зручності приймемо таку форму запису виведення формул у ЧВ:

а) послідовність формул виведення писатимемо в стовпчик, нумеруючи їх у порядку слідування F1, F2,....

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

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

A(B)

висновку A, A B - у вигляді MP(A, A B) = B.

B

Тоді останнє виведення набере вигляду:

F1: Sbb,c a,a A2 = (a (b a)) ((a ((b a) a)) (a a))

F2: MP(A1,F1) = ((a ((b a) a)) (a a)) F3: Sbb a A1 = (a ((b a) a))

F4: MP(F3,F2) = (a a)

Отже, ми довели таку метатеорему числення висловлень:

S Bp A = A(B), а правило

(a a).

10