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

Тема II. Дедуктивные свойства СКИП.

Теорема об устранении сечения.

Теорема.

СКИП Г _{СКИП \ сечение} Г

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

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

Зафиксируем сложность правила сечения <M, N₁+N₂>, где

М - количество логических связок в формуле сечения,

N₁ - число секвенций в выводе левой посылки,

N₂ - число секвенций в выводе правой посылки.

<M¹, N₁>=p₁

<M², N₂>=p₂

<M¹, N₁ > < <M², N₂ > M¹<M² V M¹=M² & N₁<N₂

По таким парам можно вести индукцию, т.к. множество этих пар обладает свойством фундированности, т.е. любая монотонная убывающая последовательность таких пар является конечной.

Пусть р =<M, N₁+N₂> - сложность.

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

Индукционное предположение - Все секвенции со сложностью меньше р выводятся без правила сечения.

Докажем для р.

Рассмотрим случаи:

1.С неглавная в левой посылке.

2.С неглавная в правой посылке.

3.С главная в обеих посылках.

1.

1) удаление &:

р: р*:

р* < р

2) удаление Ú:

р: р*: : р**

р* < р р** < р

3) удаление :

р: р*:

р* < р

Надо сохранить чистоту переменных y. При необходимости y выбрать так, чтобы не входили ни в Г, ни в С, ни в .

4) удаление :

р: р*:

р* < р

5) удаление :

р: р*:

р* < р

2.

1)введение &:

р: р*: :р**

р* < р р** < р

2)удаление &:

р: р*:

р* < р

3) введение Ú:

р: р*:

р* < р

4) удаление Ú:

р: р*: : р**

р* < р р** < р

5) введение :

р: р*:

р* < р

6) удаление :

р: р*:

р* < р

7) введение :

р: р*:

р* < р

8) удаление :

р: р*:

р* < р

9) введение :

р: р*:

р* < р

10) удаление :

р: р*:

р* < р

3.

1)&

р: р*: :р**

р* < р р** < р

2) Ú

р: р*: р* < р

р: р**: р** < р

3) :

р: ^р* _р**

р* < р р** < р

4) :

р: р*:

р* < р

5) :

р: р*:

р* < р

Таким образом, теорема об устранении сечения доказана полностью.

Следствие1. СКИП – непротиворечивая система.

Следствие2. СКИП – конструктивная система.