Построение исчисления предикатов: алфавит, формула, аксиомы. Правила вывода, опр. Вывода формулы и вывод из гипотез в ИП. Теорема Лп. Непротиворечивость ИП

1. x, y, …, z, ... – индивидные переменные;

2. ®, Ø – логические связки;

3. P₁^(k1), P₂^(k2), …, - список символов предикатов с указанием их местности;

4. $, " - кванторы;

5. (,),, - три технических символа.

II. Определение формулы такое же как в ЛП.

III. Аксиомами назовем формулы вида:

(А1): А ®(В ® А);

(А2): А ®(В ® С)®((А ® В)®(А ® С)) – закон самодистрибутивности импликации;

(А3): – закон контрапозиции.

(А4): " х А (х) ® А (t) (" – удаление)

(А5): А (t) $® х А (х) ($ - введение)

IV. Правила вывода:

1). – (MP).

2). – $ – удаление;

3) – " – введение (правило обобщения), если х не входит свободно в формулу В;

4) переименование свободной переменной, не являющейся связанной переменной этой формулы;

5) переименование связанной переменной.

V.Определение вывода формулы такое же как в ИВ, но добавляются новые правила вывода.

Определение вывода из гипотез остается в силе.

VI. Все теоремы, доказанные в (ИВ) остаются верными в (ИП).

Замечание: при доказательстве ТД следует включить еще пункты, связанные с новыми правилами вывода.