Язык ив

Язык (формальный) ИВ определяется следующим образом. Алфавит языка ИВ состоит из трех групп символов:

1) Символы переменных высказываний: A, B, C, ... , А₁, А₂, А₃, … (заглавные латинские буквы без индекса или с индексом).

2) Символы логических связок: ¬ (отрицания),  (конъюнкции),  (дизъюнкции), → (импликации).

3. Вспомогательные символы: левая скобка ( , правая скобка ) , запятая , .

Определение формулы носит индуктивный характер и заключается в следующем:

1. Переменное высказывание есть формула.

2. Если F, G - формулы, то ¬F, (F  G), (F  G), (F → G) - формулы.

3. Других формул, кроме указанных в пунктах 1-2, нет.

В целях сокращения записи формул договоримся:

1) опускать внешние скобки;

2) опускать скобки согласно следующему приоритету операций:

а) ¬;

б) , ;

в) →;

3) опускать скобки, если операции одинакового приоритета выполняются слева направо.

Пример. Формула (((АВ) →А) →(А→В)) записывается так: АВ →А →(А→В).

Определение. Последовательный набор символов G формулы

F, являющийся формулой, называется подформулой формулы F.

Пример. G₁=АВ→А, G₂=А→В - подформулы в формуле F=АВ→А→(А→В).

Определение. 1) Константы И, Л и переменная - формулы ранга 0.

2) Если формулы F и G имеют соответственно ранги n₁ и n₂ и n=max(n₁, n₂), то формулы ¬F, F  G, F  G, F → G имеют ранг, равный n+1.

Пример. Ранг формулы F=АВ→А→(А→В) равен 3.

Аксиомы ив

В ИВ взяты следующие 11 аксиом, разбитые для удобства их использования на четыре группы :

1

1)

2)

2

1)

2)

3)

3

1)

2)

3)

4

1)

2)

3)

Правила вывода в ИВ

Правил вывода в ИВ два:

1. Правило подстановки. Говорят, что формула F^G_A - подстановка формулы G вместо переменной А, если она получена из формулы F заменой каждого вхождения буквы А на формулу G.

Пример.

Пусть F= А→( В  А), G=AC, H=B→C. Тогда F^G_А=AC→(B (AC)),

F^G_B=A → ((AC)A), H^G_А= B→C, H^G_C= B→ (AC), H^G_B= AC→C.

2. Правило заключения. Это правило заключается в том, что из формул F и F → G мы можем получить формулу G.

Определение. Формула F называется выводимой в ИВ, если существует ее вывод, т. е. конечная последовательность формул F₁, … , F_n такая, что

1. F₁ - аксиома;

2. Формула F_i , 2≤i≤n, либо аксиома, либо получается из предыдущих формул по правилу подстановки или правилу заключения;

3. F_n=F.

Тот факт, что формула F выводима в ИВ, записывается в виде ├F. Из определения сразу следует, что ├F, если F ­­­­– аксиома.

Пример.

Покажем, ├ АВ→ В А.

F₁=(А→В)→((А→C) →(A→BC)) (аксиома 2.3);

F₂= (F₁)_A^{A^B} =(АB→В)→((АB→C) →(AB→BC));

F₃= (F₂)_C^A=(АB→В)→((АB→A) →(AB→BA);

F₄= AB→B (аксиома 2.2);

F₅=(АB→A) →(AB→BA) (правило заключения к F₄ и F₃);

F₆= AB→A (аксиома 2.1);

F₇= AB→BA (правило заключения к F₆ и F₅).

Итак, F_1, … , F₇ – вывод формулы АВ→ В А.

Следовательно, ├ АВ→ В А.

Понятие выводимости из множества гипотез Г является обобщением понятия выводимости.

Определение. Формула F выводима из множества гипотез Г, если существует конечная последовательность формул F₁, … , F_n такая, что

1. F₁-аксиома или гипотеза;

2. Формула F_i , 2≤i≤n, либо аксиома или гипотеза, либо получается подстановками из аксиомы F_к , k<i, или по правилу заключения из формул F_к и F_m , k<i, m<i;

3. F_n=F.

Тот факт, что формула F выводима из множества гипотез Г, записывается в виде Г ├ F.

Пример.

Покажем, что ¬¬F├ F для любой формулы F:

F₁= ¬¬А→А (аксиома 4.3);

F₂= ¬¬ F → F (подстановка F вместо А в F₁ );

F₃= ¬¬F – гипотеза;

F₄= F (правило заключения к F₃ и F₂ ).