Логические Исчисления. Исчисления высказывания (ИВ).

3.1.1  Определения.

 

Опр: Vсловом в алфавите А, называется любая конечная упорядоченная последовательность его букв.

Опр: Формативная последовательность слов – конечная последовательность слов и высказываний , если они имеют формат вида:

Логические Исчисления.  Исчисления высказывания (ИВ).

Опр: F – формулой ИВ, называется любое слово, входящее в какую-нибудь формативную последовательность.

Пример:

 

Опр: Аксиомы – специально выделенное подмножество формул. Логические Исчисления.  Исчисления высказывания (ИВ).

1)        Логические Исчисления.  Исчисления высказывания (ИВ).

2)       

3)       

4)       

5)        Логические Исчисления.  Исчисления высказывания (ИВ).

6)       

7)       

8)       

9)       

10)   

11)   

Reg – правила вывода ИВ (некоторые правила преобразования первого слова в другое).

a – символ переменной

 — произвольное слово ИВ (формула)

Отображение Логические Исчисления.  Исчисления высказывания (ИВ). действует так, что на место каждого вхождения символа а , пишется слово Логические Исчисления.  Исчисления высказывания (ИВ)..

Пример:

Правило modusponens:        

3.1.2  Формальный вывод.(простейшая модель доказательства теоремы)

Опр: Последовательность формул ИВ, называется формальным выводом, если каждая формула этой последовательности имеет следующий вид:

Опр: Выводимый формулой (теоремой) ИВ называется любая формула входящая в какой-нибудь формальный вывод.   — выводимая формула ИВ.

 

Пример: 

1)

Логические Исчисления.  Исчисления высказывания (ИВ).

2)

3)

Логические Исчисления.  Исчисления высказывания (ИВ).

4)

5)

6)

 

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

Замечание: Если формула  выводима, то выводима и

Возьмем формативную последовательность вывода   и добавим в неё , получившаяся последовательность является формальным выводом.

(Если выводима  то если  , то выводима  )

 

Теор: Если  выводимая формула , то  ( — различные символы переменных) выводима

Выберем  — символы переменных которые различны между собой и не входят не в одну из формул  , сделаем подстановку  и последовательно применим  и в новом слове делаем последовательную подстановку: Логические Исчисления.  Исчисления высказывания (ИВ)., где  — является формальным выводом.

 

3.1.3  Формальный вывод из гипотез.

Опр: Формальным выводом из гипотез (формулы), называется такая последовательность слов , каждая из которых удовлетворяет условию:

 если формулу Логические Исчисления.  Исчисления высказывания (ИВ). можно включить в некоторый формальный вывод из гипотез Логические Исчисления.  Исчисления высказывания (ИВ)..

Лемма: ; : то тогда

Напишем список:

  Логические Исчисления.  Исчисления высказывания (ИВ).   

Лемма

Док:     

 

3.1.4  Теорема Дедукции.

Если из

Логические Исчисления.  Исчисления высказывания (ИВ). 

1)                       и 2а)  Логические Исчисления.  Исчисления высказывания (ИВ)., где   по правилу m.p. Логические Исчисления.  Исчисления высказывания (ИВ)., ч.т.д.

2б)   — уже выводили , ч.т.д.

 

Базис индукции: N=1   — формальный вывод из длинного списка

 (только что доказано), осуществим переход по индукции:

 по индукции

 и по лемме 2

Пример: Логические Исчисления.  Исчисления высказывания (ИВ).

 по теореме дедукции

 

Логика - доступно для всех