Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема



Скачать 47.45 Kb.
Дата09.10.2012
Размер47.45 Kb.
ТипДокументы

08.10.12, М.

Теорема дедукции

§ 1. Формулировка теоремы и некоторые следствия

Теорема (дедукции). Если

1, 2, …, n,  ├ ψ,

то

1, 2, …, n├ ( → ψ).

Замечания. 1. Применяя к утверждению теоремы снова несколько раз теорему де­дукции, можно, очевидно, получить новые следствия:

1, 2, …, n−1├ (n → ( → ψ));



├ (1 → … → (n−1 → (n → ( → ψ)))…).

2. На время доказательства теоремы введём такую терминологию. Будем называть список гипотез 1, 2, …, n коротким списком гипотез, а список 1, 2, …, n,  – длин­ным списком.

3. Докажем сейчас, что верна теорема, обратная к теореме дедукции, а именно: если

1, 2, …, n├ ( → ψ),

то

1, 2, …, n,  ├ ψ.

Для доказательства предположим, что

v1

v2

… (1)

vN = ( → ψ)

− формативная последовательность, являющаяся формальным выводом формулы ( → ψ) из короткого списка гипотез (в силу принципа «обрубания хвостов» можно, как обычно, предполагать, что наша формула ( → ψ) является последним словом в последо­вательности (1)).

Последовательность (1) тем более можно рассматривать как формальный вывод из длинного списка гипотез (это вытекает из определения формального вывода из гипотез). Добавим в конец последовательности (1) ещё две формулы:

v1

v2

… (2)

vN = ( → ψ)



ψ

Новая последовательность (2) снова является формальным выводом из длинного списка гипотез. В самом деле, предпоследняя формула является гипотезою, а последнюю формулу ψ можно получить по правилу modus ponens из двух предыдущих. Как видно, формула ψ выводима из длинного списка, QED1.

§ 2. Леммы к теореме дедукции

Лемма 1. Если  – выводимая формула ИВ, то результат S() применения к  од­новременной подстановки S также есть выводимая формула ИВ.

Доказательство. Пусть одновременная подстановка S заключается в том, что по­парно различные буквы a1, a2, …, ak одновременно заменяются в формуле  на формулы 1, 2, …, k.


Возьмём множество всех тех и только тех букв, которые входят в запись хотя бы одной из формул 1, 2, …, k. Их конечное число. Пусть это будут (попарно различные) буквы x1, x2, …, xn. Тогда можно записать: 1 = 1(x1, x2, …, xn), …, k = k(x1, x2, …, xn). Так как алфавит ИВ (точнее, множество символов переменных) бесконечен, то можно взять попарно различные буквы b1, b2, …, bn, каждая из которых не совпадает ни с одной из букв a1, a2, …, ak, x1, x2, …, xn и не входит в запись формулы . А теперь произведём последовательно серию обычных (однократных) подстановок: сначала в формулу  вме­сто буквы a1 подставим формулу 1(b1, b2, …, bn), затем вместо a2 в новую формулу под­ставим 2(b1, b2, …, bn) и т. д.; вместо ak – k(b1, b2, …, bn). Затем вместо букв b1, b2, …, bn последовательно подставим буквы x1, x2, …, xn. Легко видеть, что в конце мы получим S().

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

Лемма доказана.

Лемма 2. Если

1, 2, …, n├ ( → ψ)

и

1, 2, …, n├ ( → (ψ → χ)),

то

1, 2, …, n├ ( → χ)

(своеобразный modus ponens!).

Доказательство. Пусть ( → ψ) замыкает последовательность формул, являю­щуюся формальным выводом из гипотез 1, 2, …, n, а формула ( → (ψ → χ)) замыкает другую последовательность формул, также являющуюся формальным выводом из данных гипотез. Приписав вторую последовательность впритык к первой, мы получим, очевидно, новый формальный вывод из данных гипотез. Добавим к этой последовательности ещё несколько формул:



− это аксиома № 2 и, следовательно, выводимая в ИВ формула;



− результат одновременной подстановки в предыдущую формулу:  вместо A, ψ вместо B, χ вместо C. Следовательно, по лемме 1 это будет абсолютно выводимая формула;



− результат применения правила modus ponens к предыдущей формуле и к формуле ( → (ψ → χ)), содержащейся в нашей последовательности;

( → χ)

− результат применения правила modus ponens к предыдущей формуле и к формуле ( → ψ), содержащейся в нашей последовательности.

Так как построенная нами длинная последовательность является, очевидно, фор­мальным выводом из гипотез 1, 2, …, n, а формула ( → χ) в ней содержится, то лемма доказана.

§ 3. Доказательство теоремы дедукции в частных случаях

Докажем сейчас теорему дедукции в трёх важных частных случаях:

1) формула ψ выводима в ИВ;

2а) ψ совпадает с одной из гипотез 1, 2, …, n;

2б ψ = .

Впрочем, случаи 1) и 2а) можно объединить. Рассмотрим последовательность:



(ψ → ( → ψ))

ψ

( → ψ)

Утверждаю, что эта последовательность в случаях 1) и 2а) является формальным выводом из короткого списка гипотез (откуда вытекает утверждение теоремы).

В самом деле, первое слово есть аксиома № 1. Второе слово есть результат приме­нения одновременной подстановки в предыдущую формулу и, следовательно, выводимо в ИВ по лемме 1. Третье слово в случае 1) есть абсолютно выводимая формула, а в случае 2а) – гипотеза короткого списка. Наконец, последняя формула в нашей последовательно­сти есть результат применения правила modus ponens к двум предыдущим формулам.

В случае же 2б) надо вывести формулу ( → ) из короткого списка гипотез. Это делается с помощью подстановки в абсолютно выводимую формулу (AA) (доказыва­лась в моём курсе ранее) вместо буквы A формулы  (и получается даже абсолютно выво­димая формула).

§ 4. Доказательство теоремы дедукции в общем случае

Пусть

v1

v2



vN = ψ

− формальный вывод из длинного списка гипотез. Будем доказывать теорему индукцией по N.

База индукции: N = 1. Наша последовательность состоит из одной формулы ψ. Но это означает, что ψ либо абсолютно выводима, либо совпадает с одной из гипотез длин­ного списка. В обоих этих случаях теорема уже доказана (§ 3).

Пусть теперь теорема доказана для всех формул ψ, входящих во всевозможные формальные выводы из длинного списка гипотез, имеющие длину меньшую, чем N, и до­кажем её для вышеприведённого вывода длины N. Рассмотрим последнюю формулу ψ. Если она абсолютно выводима или совпадает с одной из гипотез длинного списка, то опять-таки для этих частных случаев теорема уже доказана. Остаётся случай, когда ψ = = MP (vi, vj), i, j < N. Но тогда обязательно vj = (vi → ψ). Так как оба слова vi, vj входят в формальные выводы из длинного списка гипотез длины < N, то по индуктивному предпо­ложению

1, 2, …, n├ ( → vi)

и

1, 2, …, n├ ( → (vi → ψ)).

Но тогда по лемме 2

1, 2, …, n├ ( → ψ),

QED.

1 Quod erat demonstrandum (лат.) – ‘что и требовалось доказать’.


Похожие:

Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconДифференциальная геометрия и топология
Теорема о неявных функциях (формулировка), теорема об обратном отображении, теорема "об образе"
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconПрограмма составлена кандидатом физ мат наук Барановым В. Н
Симплексы и триангуляция множеств. Нумерации и лемма Шпернера. Теорема Брауера. Теоремы о неподвижной точке в бесконечномерных пространствах....
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconОсновные теоремы о непрерывных функциях Теорема I
Теорема (I теорема Больцано-Коши). Пусть функция определена и непрерывна на и на концах принимает значения разных знаков, т е., тогда...
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconОсновные теоремы о непрерывных функциях Теорема I
Теорема (I теорема Больцано-Коши). Пусть функция определена и непрерывна на и на концах принимает значения разных знаков, т е., тогда...
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconТеория интеллектуальных систем
Язык логики высказываний, общезначимые формулы Дедуктивная система для описания класса общезначимых формул Теорема дедукции. Теорема...
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconЛекция №15 (Теорема 21), [6] Метод покоординатного спуска. Лекция №16 (Теорема 24), [2, 3]
Теория двойственности нелинейного программирования. Лекция №4 (Теорема 10, леммы 5, 6, следствия 1 и 2), Лекция №5 (следствие 3),...
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconПрограмма экзамена по курсу "Локализация аттракторов"
Трансверсальность. Формулировка теоремы о трансверсальности Абрахама (теорема 6)
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconКонспект урока геометрии в 9 классе на тему "Вписанный угол. Теорема о вписанном угле"
Определение понятия вписанного угла содержит два существенных свойства, формулировка теоремы несложная. Доказательство теоремы в...
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconПрограмма по математике для вступительного экзамена в аспирантуру на математическом факультете Омгу по специальности 01. 01. 04- «Геометрия и топология»
Основные теоремы дифференциального исчисления (теорема о средних значениях, теорема о неявных функциях, формула Тейлора). Основные...
Теорема дедукции § Формулировка теоремы и некоторые следствия Теорема iconIii. Уравнения высших степеней § Теорема Безу и её следствия Теорема
Остаток от деления многочлена Рn(х) на двучлен (х – а) равен значению данного многочлена при х =а
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org