1.2.3. Свойства отношения выводимости.

Метатеорема 1(МТ1).

1. .

2. Если и , то

Доказательство

1. Для построения вывода формула из формул достаточно записать последовательно все формулы (в произвольном порядке), поместив последней формулу .

2. Заменив в данном выводе формулы С из формул формулы их данными выводами из формул .

Метатеорема 2 (МТ2).

Пусть Г – любое множество формул.

Тогда:

1. Если Г , то Г, В частности

2. Если , то

Следствие:

1. Если , то .

2. Если , то .

Метатеорема 3(МТ3).

Теорема дедукции (ТД), правило введения импликации (ВИ).

Пусть Г – любое множество формул.

Тогда:

3. Если Г, , то Г . В частности

4. Если , то .

Доказательство

По условию МТ3 вывод (1) формула B из множества формул (данный вывод).

Требуется доказать существование вывода (2) формула из формул множества Г (результирующий вывод).

Опишем алгоритм превращения данного вывода (1) в результирующей вывод (2). К каждой формуле данного вывода (1) припишем слово « ». Тогда получим последовательность формул: , (3) заканчивающуюся нужной формулой . Эта последовательность не является, вообще говоря, выводом из множества формул Г. Однако можно перед каждой формулой вставить дополнительные формулы так, чтобы превратить последовательность формул (3) в (2). Вывод дополнительных формул зависит от того, с каким обоснованием формула входит в данный вывод (1). Возможны 4 типа обоснований:

1. - посылка множества Г;

2. - посылка А;

3. - аксиома;

4. – формула, полученная по MP из двух предшествующих формул и (p,q<i).

Рассмотрим каждый из этих случаев:

1. Пусть и . В этом случае является посылкой не только в данном выводе (1), но и в результирующем выводе (2). Тогда перед формулой последовательности (3) вставим две формулы и , из которых получается по правилу MP:

l. l. посылка

l+1. l+1. AC1

l+2. l+2. MP(l, l+1)

2. Пусть . Тогда - посылка в данном выводе (1), но не является таковой в результирующем выводе (2). В последовательности (3) будет стоять формула , которая является доказуемой (пример 1). Поэтому перед вставляем первые четыре формулы из ее доказательства.

3. Пусть – аксиома. Тогда поступаем, как и в случае 1.

4. Пусть – формула, полученная по MP из формул и (p,q<i) последовательности (1). Тогда должна иметь вид (или имеет вид ). Итак, получена из и по MP. В последовательности (2) в этом случае будут формулы и с некоторыми номерами S и t(S,t<i), и нужно обосновать включение в вывод (2) формула . Но формулы и и являются частями AC2. Таким образом, перед в данном случае необходимо вставить две формулы с номерами и :

S. S

……… …

t. t

……… …

U. AC2

U+1. MP(S, U)

U+2. MP(t,

Следствия:

1. Если , то . В частности;

2. Если , то .