Исчисление Высказываний

1. Выводимость (H={A1..An}

1.1. Правила выводимости

1.1.1. H = A / H,W = A

1.1.2. Н,C=A;H=C/H=A

1.1.3. H=C->A/H,C=A

1.1.4. H,C=A;W=C/H,W=A

1.1.5. Теорема дедукции + обобщенная - H,C=A/H=C->A

1.1.6. Закон перестановки посылок

1.1.7. Закон соединения посылок

1.1.8. Закон разъединения посылок

1.2. Всякая Ai выводима из H

1.3. Любая доказуемая формула

1.4. Если С->B то и В тоже выводима

1.5. Свойства

1.5.1. всякий начальный отрезок

1.5.2. поставить вывод между другими

1.5.3. всякий вывод - выводимая ф-ла

1.5.4. если Н часть W то выводы H тоже из W

2. Правила вывода

2.1. Производные правила вывода

2.1.1. Правило одновременной подстановки

2.1.2. Правило сложного заключения

2.1.3. Правило силлогизма

2.1.4. Правило контрапозиции

2.1.5. Правило снятия двойного отрицания

2.2. Правило подстановки

2.3. Правило заключения

3. Формула

3.1. Подформула

3.1.1. У элементарной - она сама

3.1.2. Если ¬А - она сама, А, все подформулы А

3.1.3. Если А*В - А, В, все подвормулы А и В

3.2. Всякая переменная

3.3. А, В - формулы, А*В - формула

3.4. Монотонность

3.4.1. A1->A2 = B(A1)->B(A2) => монотонно возрастает и наоборот

3.4.2. Все основные операторы монотонны по всем аргументам

3.5. Эквивалентность

3.5.1. A->B=1 & B->A=1 => эквивалентны

3.5.2. Свойства

3.5.2.1. Симметричность

3.5.2.2. Рефлексивность

3.5.2.3. Транзитивность

3.6. Доказуемая

3.6.1. Всякая аксиома

3.6.2. Формула полученная путем подстановки

3.6.3. B, если A=1 и A->B=1

4. Алфавит

4.1. Переменные высказывания - X, Y, Z

4.2. Лог.связки - ˄, ˅, → , ¬

4.3. 3я категория - (, ), ,

5. Алгебра высказываний

5.1. Теоремы связи

5.1.1. Если А доказуемая в ИВ, то она ТИ в АВ

5.1.2. Если А=1, то H=A, если А=0, то H=¬A

5.1.3. Если ТИ в АВ, то доказуемая в ИВ

6. ФОРМАЛЬНЫЕ СИСТЕМЫ

6.1. Определение

6.1.1. Алфавит

6.1.2. Процедуры построения формул

6.1.3. Аксиомы

6.1.4. Правила вывода

6.1.5. Проблемы

6.1.5.1. Противоречивость

6.1.5.2. Полнота

6.1.5.2.1. Узкий смысл в ИВ - добавление к аксиомам = противоречие

6.1.5.2.2. Широкий смысл в ИВ - ТИ = доказуемая

6.1.5.3. Независимость аксиом

6.1.5.4. Разрешенность

7. Аксиомы

7.1. Группа 1

7.1.1. 1. x -> (y -> x)

7.1.2. 2. (x->(y->z))->((x->y)->(x->z))

7.2. Группа 2

7.2.1. 1. x&y->x

7.2.2. 2.x&y->y

7.2.3. 3.(z->x)->((z->y)->(z->x&y))

7.3. Группа 3

7.3.1. 1. x-> x˅y

7.3.2. 2.y->x˅y

7.3.3. 3.(x->z)->((y->z)->(x˅y->z))

7.4. Группа 4

7.4.1. 1.(x->y)->(¬y->¬x)

7.4.2. 2.x->¬¬x

7.4.3. 3.¬¬x->x