Альтернативні системи аксіом
Система аксіом Гілберта Іакермана
Зв'язки:
,,
Вводяться наступні аксіоми:
В В В В
Система аксіом Россера
Вводяться зв'язки:
&, -, A-> B = - (A &-B)> (A & A) & B-> B
(A-> B) -> (- (B & C) -> - (C & A))
Система аксіом Мередита:
(Зв'язки: ->, -)
[((A-> B) -> (-C->-D)) -> C] -> ((C-> A) -> (D-> B ))
У всіх випадках задавалися схеми аксіом, тобто реальна кількість аксіом в кожному випадку нескінченно. Можна задати систему з кінцевим числом аксіом, кажучи, що задається не схема, а формула, але при цьому виникає необхідність введення нового правила виведення, званого правилом підстановки:
Якщо дана формула Ф (А1 ... Аn) і є деякі формули Ф1 ... Фn, то ми можемо отримати формулу Ф (Ф1 ... Фn), підставивши формули Фi замість відповідних пропозіціонних змінних.
Система аксіом Кліні.
(K1) А-> (B-A)
(K2)
(K3) A & B-> A
(K4) A & B-> B
(K5) A-> (B-> (A & B))
(K6) A-> (AB)
(K7) B-> (AB)
(K8) (A-> C) -> ((B-> C) -> ((AvB)) -> C
(K9) (A-> B) -> ((A->-B) ->-A)
(K10) - A-> A
Тут всі логічні зв'язки вводяться безпосередньо, а не розглядаються, як скорочення один одного. p> В принципі, можна показати, що обчислення висловлювань К, і ІВ L рівносильні, як формальні теорії. Основне завдання в процесі подібних доказів про равносильности аксіом і введених в них зв'язок, полягає в тому, що формули, необхідні для виведення коротшою або заданої явно логічної зв'язкою, виведені на основі еквівалентної їй формулою в іншій аксіоматиці. При цьому з формули з першої аксіоматиці, виводяться формули, з яких можна вивести формули другий аксіоматиці. p> Наприклад, розглянемо еквівалентність формул:
(A->-B) в аксіоматиці ІВ L і A & B.
На підставі схеми К5 і МР доводиться, що з формули A & B виводиться формула в аксіоматиці До формула А-> В. Далі на основі аксіом К3 і К4 бачимо що з A & B виводиться А, з A & B виводиться В.
У теорії L мається тавтологія A-> (B-> - (A->-B)) виводимість якої можна довести за допомогою теореми про повноту. Виходячи з цієї формули і МР, отримуємо, що. p> У аксіоматиці L має місце тавтології і, отже, по МР маємо і.
У підсумку можна зробити висновок (A & B).
На підставі вищевикладеного, можна зробити висновок
За аналогією можна вивести
Що стосується, то вже було доведено і.
Таким чином, ми можемо переносити аксіоми між схемами аксіом.
Теорема
Розглянемо теореми:
F1 ... Fn,
тобто тоді, коли остання формула є тавтологією.
Розглянемо доказ:
Виводимість G і безлічі F1 ... Fn означає по теоремі дедукції
F1, F2 ... Fn-1Fn-> G ...
(тут типу все через імплікації через вкладені дужки)
Виводимість даної формули по теоремі означає що вона є тавтологією. p> Уявімо імплікації через диз'юнкцію:
Звідси випливає, що виводиться т. і т.т., коли остання формула є тавтологією. p align="justify"> Приклад покажемо з використанням ModusTollens.
Покажемо, що
В
Для цього нам потрібно довести що
В
є тавтологією
Просто знаходимо таблицю істинності для всіх значень P і Q.
F1 ... Fn,
тобто є протиріччям.
Док - во. У відповідність з попередньою теоремою, ця теорема рівносильна є тавтологією, це в свою чергу рівносильне, розкриємо імплікації
,
далі за законами Де Моргана
В
Як приклад розглянемо доказ коректності ще одного правила виводу ModusTollendoTollens. Тобто покажемо, що
В
Відповідно до щойно доведеною теоремою треба вивести, що
В
за таблицею істинності видно, що це вірно. p> Теорема
F1, ..., FnГЅGГ› коли виведена формула ГЅF1 & F2 & ... & Fn В® G, тобто коли ця формула - тавтологія
Док-во:
F1, ..., Fn | - GГіпо теоремі дедукції F1, ..., Fn-1 | - FnГ G <=> F1, ..., Fn-2 | - Fn-1Г (FnГ G) <=> ... < => | - F1Г (F2Г ... Г (FnГ G) ...) <=> {по теоремі ополноте} <=> F1Г (F2Г ... Г (FnГ G) ...) - тавтологія? = p> Г№F1V (F2Г ... Г (FnГ G) ...) = ... = Г№F1VГ№F2V ... VГ№FnVG = (по з-ну Де Моргана) = Г№ (F1 & F2 & ... & Fn) VG = F1 & F2 & ... & FnГ G - тавтологія.
Теорема:
F1, ..., Fn | - G <=>
чи є формула F1 & F2 & ... & Fn & Г№G - протиріччям?
Док-во:
За попередньою теоремою: F1, ..., Fn | - G <=> F1 & F2 & ... & FnГ G - тавтологія? <=> Г™ (F1 & F2 & ... & FnГ G) - протир...
