Схемы аксиом ИВ

1) j®(j®y)

2) (j®y)®((j®(y®c))®(j®c))

3) (jÙy)®j

4) (jÙy)®y

5) (j®y)®((j®c)®(j®(yÙc)))

6) j®(jÚy)

7) j®(yÚj)

8) (j®c)®((y®c)®((jÚy)®c))

9) (j®y)®((j® )® )

10)

Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.

Единственным правилом вывода в ИВ является правило заключений (modus ponens): если φ и φ®y - выводимые формулы, то y так же выводима. Обозначение: .

Будем говорить, что формула φ выводима из формул φ₁φ₂ …φ_n, если существует последовательность формул y₁y₂…y_к, φ в которой любая формула либо является аксиомой, либо принадлежит списку формул φ₁φ₂ …φ_n, называемых гипотезами., либо получается из предыдущих формул по правилу заключений. Обозначается: φ₁φ₂ …φ_n φ – формула φ выводима из формул φ₁φ₂ …φ_n.

Выводимость формулы φ из Ø ( φ) равносильна тому, что φ – теорема исчисления высказываний.

Всякая формула от пропозиционных переменных А₁А₂ … А_к является тождественно истиной (доказуемой), если булева функция , соответствующая формуле φ тождественно равна 1.

Для проверки значений функции используют так называемое семантическое дерево, то есть бинарное дерево, удовлетворяющее следующим условиям:

1) каждое ребро помечено литерой

2) литеры, выходящие из одной вершины являются контрарными: и

3) ребра соответствуют литере одной и той же пропозиционной переменной тогда и только тогда, когда они находятся на одинаковом расстоянии от корня дерева.

Такое семантическое дерево имеет 2^к висячих вершин и для проверки общезначимости формулы необходимо пройти 2^к маршрутов от корня до каждой из вершин.

Дата добавления: 2017-02-01