double arrow

Доказательство утверждения 1.

Доказательство ведём индукцией по числу вершин Р в дереве редукций.

Базис Р =1.

+ С помощью избавляемся от многосукцедентности.

v •

что и требовалось.

Пусть утверждение справедливо для Р<k, докажем для P=k.

Рассмотрим все возможные случаи (6 штук):

1) редукция & - справа.

+ +

+• v

По индукционному предположению доказаны секвенции, соответствующие дочерним вершинам.

Построим доказательство секвенции, соответствующей v. Для этого достаточно доказать секвенцию , и затем применить 2 раза правило сечения.

2) редукция &- слева.

+ •

+ • v

По индукционному предположению доказана секвенция, приписанная дочерней вершине. Построим доказательство секвенции, приписанной v. Она доказуема по правилу удаления &.

3) редукция v- справа.

+ •

тривиально

+ • v

4) редукция v – слева.

• •

+ +

+• v

По индукционному предположению доказываются секвенции, приписанные дочерним вершинам. Построим доказательство секвенции, приписанной v. Она доказывается по правилу удаления .

5) редукция – слева.

• •

+ +

+• v

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

Аналогично п.1 докажем сначала секвенцию ,

и применим затем 2 раза правило сечения.

6) редукция – справа (2 рода).

+

+ v

По индукционному предположению доказывается одна из секвенций, приписанных дочерним вершинам. Построим доказательство секвенции, приписанной v: .

Доказательство состоит в применении правила введения и правил введения V.

Утверждение 1 доказано.


Понравилась статья? Добавь ее в закладку (CTRL+D) и не забудь поделиться с друзьями:  



Сейчас читают про: