Математическая логика и теория алгоритмов 3

Математическая логика и теория алгоритмов

Первухин Михаил Александрович

Исчисление

высказываний

Лекция 3

Определение формального исчисления

Будем говорить, что формальное исчисление определено, если выполняются четыре условия.

1.Имеется некоторое множество А символов – алфавит исчисления .

Конечные последовательности символов называются словами или выражениями исчисления . Обозначим через S множество всех слов алфавита исчисления .

2.Задано подмножество , называемое множеством формул исчисления . Элементы множества F называются формулами.

Определение формального исчисления

3.Выделено множество формул, называемых аксиомами исчисления .

4.Имеется конечное множество K отношений 1, 2, … , между

Итак, исчисление есть четверка ( , , , ).

Выводом в исчислении называется последовательность формул

1, 2, … , такая, что для любого (1 ≤ ≤ ) формула есть либо аксиома исчисления , либо непосредственное следствие каких-либо

предыдущих формул.

Формула называется теоремой исчисления , выводимой в , или

доказуемой в , если существует вывод 1, … , , , который называется

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

Если существует алгоритм, с помощью которого для произвольной формулы φ через конечное число шагов можно определить, является ли φ выводимой в исчислении или нет, то исчисление называется

разрешимым.

Исчисление называется непротиворечивым, если не все его формулы доказуемы.

Система аксиом и правил вывода

Используя понятие формального исчисления, определим исчисление высказываний (ИВ).

Алфавит ИВ состоит из букв x,y,z,u,v, возможно с индексами

(которые называются пропозициональными переменными),

логических символов (связок) ¬, , , →, а также вспомогательных

символов (, ).

Множество формул ИВ определяется индуктивно:

а) все пропозициональные переменные являются формулами ИВ;

б) если , - формулы ИВ, то ¬ , ( ), ( ), ( → ) –

формулы ИВ;

в) выражение является формулой ИВ тогда и только тогда, когда это может быть установлено с помощью пунктов "а" и "б".

Таким образом, любая формула ИВ строится из пропозициональных переменных с помощью связок ¬, , , →.

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

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

Аксиомами ИВ являются следующие формулы для любых формул

, , ИВ:

1.→ ( → );

2.( → ) → (( → ( → )) → ( → ));

3.( ) → ;

4.( ) → ;

5.( → ) → (( → ) → ( → ( )));

6.→ ( );

7.→ ( );

8.( → ) → (( → ) → (( ) → ));

9.( → ) → (( → ¬ ) → ¬ );

10.¬¬ → .