Математическая Логика (стр. 3 из 4)
- произвольное слово ИВ (формула)Отображение
действует так, что на место каждого вхождения символа а , пишется слово .Пример:
Правило modus ponens:
3.1.2 Формальный вывод.(простейшая модель доказательства теоремы)
Опр: Последовательность формул ИВ, называется формальным выводом, если каждая формула этой последовательности имеет следующий вид:
Опр: Выводимый формулой (теоремой) ИВ называется любая формула входящая в какой-нибудь формальный вывод.
- выводимая формула ИВ.Пример:
| 1) |  |  |
| 2) |  |  |
| 3) |  |  |
| 4) |  |  |
| 5) |  |  |
| 6) |  |  |
Правило одновременной подстановки.
Замечание: Если формула
выводима, то выводима и 
Возьмем формативную последовательность вывода
и добавим в неё 
, получившаяся последовательность является формальным выводом.(Если выводима
то если 
, то выводима 
)Теор: Если выводимая формула
, то 
( 
- различные символы переменных) выводимаВыберем
- символы переменных которые различны между собой и не входят не в одну из формул 
, сделаем подстановку 
и последовательно применим 
и в новом слове делаем последовательную подстановку: 
, где 
- является формальным выводом.3.1.3 Формальный вывод из гипотез.
Опр: Формальным выводом из гипотез
(формулы), называется такая последовательность слов 
, каждая из которых удовлетворяет условию: 
если формулу можно включить в некоторый формальный вывод из гипотез .Лемма:
; 
: то тогда 
Напишем список:
Лемма:
Док:
3.1.4Теорема Дедукции.
Если из
1) и 2а)
, где 
по правилу m.p. 
, ч.т.д.2б)
- уже выводили 
, ч.т.д.Базис индукции: N=1
- формальный вывод из длинного списка 
(только что доказано), осуществим переход по индукции: 
по индукции 
и по лемме 2 
Пример:
по теореме дедукции 
3.2 Критерий выводимости в ИВ.
3.2.1 Формулировка теоремы.
- тавтологияпри любой интерпретации алфавита (символов переменных)
3.2.2 Понятие интерпретации.
символ переменной
переменную поставим в соответствие. 
, где 
- проекция на 
. 
; 
- только символпеременных, т.к.
это заглавное слово
формативной последо-
вательности вида:
Где:
3.2.3 Доказательство теоремы.
формальныйвывод
(1)
