Поможем написать любую работу на аналогичную тему
3.1.1 Определения.
Опр: V – словом в алфавите А, называется любая конечная упорядоченная последовательность его букв.
Опр: Формативная последовательность слов – конечная последовательность слов и высказываний 
, если они имеют формат вида:
Опр: F – формулой ИВ, называется любое слово, входящее в какую-нибудь формативную последовательность.
Пример: 
Опр:
Аксиомы – специально выделенное подмножество формул. 
1) 
2) 
3) 
4) 
5) 
6) 
7) 
8) 
9) 
10) 
11) 
Reg – правила вывода ИВ (некоторые правила преобразования первого слова в другое).
a – символ переменной 
- произвольное слово ИВ (формула)
Отображение 
действует так, что на место каждого вхождения символа а , пишется слово 
.
Пример: 
Правило 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
Пример: 
по теореме дедукции 