close

Вход

Забыли?

вход по аккаунту

?

16 17

код для вставкиСкачать
 Система аксиом исчисления высказываний.
Содержит 11 аксиом, которые условно разбиты на 4 группы.
а) x→(y→x)
b) (x→(y→z))→((x→y)→(x→z))
a) x&y→x
b) x&y→y
c) (z→x)→((z→y)→(z→x&y))
a) x→x∨y
b) y→x∨y
c) (x→z)→((y→z)→(x∨y→z))
a) (x→y)→(y ̅→x ̅)
b) x→x ̅
c) x ̿→x
Правила вывода: правило подстановки, правило заключения.
Правило подстановки.
Пусть А - доказуемая формула исчисления высказываний, х - это некоторая переменная, В - произвольная любая формула исчисления высказываний. Тогда формула, которая получается из формулы А путем подстановки в нее вместо х формулы В доказуема. Операция замены х на формулу В символически записывается так: ∫_x^В▒〖(А)〗.
Некоторые свойства применения формулы подстановки:
Если А представляет х, то ∫_x^В▒〖(А)〗 дает в результате В.
Если А представляет собой какую-то переменную y, отличную от х, то подстановка ∫_x^В▒〖(А)〗 дает в результате А. Если А - формула, то подстановка В вместо х в отрицание А дает отрицание подстановки: ∫_x^В▒〖(А)〗 дает (∫_x^В▒〖(А)〗) ̅.
Если А1 и А2 - формулы, то подстановка ∫_x^В▒〖(А_1*А_2)〗 дает в результате ∫_x^В▒〖(А_1)〗*∫_x^В▒〖(А_2)〗*(∨, &, →).
Доказуемая формула обозначается ├А. Правило подстановки схематически записывается так: (⊢А)/(⊢∫_x^В▒〖(А)〗) . Если формула А доказуема, то доказуема формула, где вместо х В.
Правило заключения
Пусть формулы А и А→В доказуемы в исчислении высказываний, тогда формула В также доказуема.
(⊢А, ⊢А→В)/(⊢В)
Автор
lovematanfo
Документ
Категория
Без категории
Просмотров
98
Размер файла
15 Кб
Теги
билет
1/--страниц
Пожаловаться на содержимое документа