II. Тип дерева редукций

а) Разметка концевых вершин дерева редукций описана выше.

б) Разметка внутренних вершин дерева редукций.

«–»и«+»приписываются всем внутренним вершинам дерева редукций по правилам:

редукции 1 рода:

+ + – – + –

+ – – + –

редукции 2 рода:

+ – – –

+ –

III. Построение доказательства или опровержения по Крипке по дереву редукций.

Утверждение 1.

Если корневая вершина дерева редукций помечена «+», то приписанная ей секвенция доказуема в КИВ.