Лекция № 7

Тема: ФОРМАЛЬНЫЕ СИСТЕМЫ. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Основные вопросы, рассматриваемые на лекции:

1. Определение формальной системы

2. Метод доказательства индукцией по формулам

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

4. Исчисление высказываний

Краткое содержание лекционного материала

Формальная система S определена, если:

1) Задано счетное множество символов. Конечная последовательность символов называется словом (или строкой).

2) Выделяется множество формул системы S – подмножество множества слов системы S. Обычно указывается алгоритм построения формул.

3) Выделяется множество аксиом системы S – подмножество множества формул системы S.

4) Выделяется множество правил вывода системы S – множество некоторых отношений между формулами системы S. Если P – правило вывода, (A ₁,…, A_m, B)ÎP, то формулы A ₁,…, A_m называются посылками, а формула B – заключением правила P. При этом говорят, что формула B непосредственно следует из формул A ₁,…, A_m.

Следующее определение формулы системы S ₁ является частным случаем определения пропозициональной формулы.

Слово системы S ₁ называется формулой системы S ₁, если оно построено строго по следующим правилам:

1) пропозициональные переменные – формулы системы S ₁;

2) если слово A системы S ₁ является формулой системы S ₁, то слово Ø A тоже является формулой системы S ₁;

3) если слова A и B системы S ₁ являются формулами системы S ₁, то слово (A Þ B) тоже является формулой системы S ₁.

Имеет место метод доказательства индукцией по формулам. Пусть для некоторого свойства формул P (A) доказаны следующие утверждения:

1) если p – пропозициональная переменная, то P (p) верно;

2) если P (A), то P (Ø A) тоже верно;

3) если P (A) верно и P (B) верно, то P (A Þ B) тоже верно.

Тогда свойства P (A) верно для всех формул A системы S ₁.

Следующее определение теоремы системы S ₁ является частным случаем определения логического следствия.

Выводом формулы A из множества формул G называется конечная последовательность формул A ₁,…, A_n, если:

1) A_n = A;

2) для каждого i =1,…, n формула A_i

(a) является некоторой аксиомой, или

(b) принадлежит множеству G, или

(c) непосредственно следует по некоторому правилу вывода из формул A_{i 1},…, A_im, где 1£ i ₁,…, i_m < i.

При этом говорят, что формула A следует из множества формул G (или A следствие из множества G), и пишут G|¾ A (или G|¾ _SA). Если G={ A ₁,…, A_m } – конечное множество, то пишут также A ₁,…, A_m |¾ A (или A ₁,…, A_m |¾ _SA).

Формула A системы S называется теоремой системы S, если следует из пустого множества формул. Обозначение: |¾ A, или |¾ _SA.

Исчисление высказываний – это формальная система, символами которой являются пропозициональные переменные и связки, а формулами – пропозициональные формулы. Рассмотрим исчисление высказываний S ₁ с двумя связками Ø и Þ (остальные связки можно определить в терминах Ø и Þ, например, A Ú B =Ø A Þ B и A Ù B =Ø(A ÞØ B)) и со следующими аксиомами и правилом вывода:

(A ₁) A Þ(B Þ A);

(A ₂) (A Þ(B Þ C))Þ((A Þ B)Þ(A Þ C));

(A ₃) (Ø B ÞØ A)Þ((Ø B Þ A)Þ B);

(MP) A, A Þ B |¾ B

(где A, B, C – это произвольные пропозициональные формулы, построенные из пропозициональных переменных и связок Ø и Þ).

Формула системы S называется теоремой системы S, если оно получено строго по следующим правилам:

1) аксиомы (A ₁), (A ₂), (A ₃) являются теоремами системы S;

2) если посылки A и A Þ B правила (MP) – теоремы системы S, то его заключение B – тоже теорема системы S.

Имеет место метод доказательства индукцией по теоремам (мы сформулируем этот метод для теорем системы S). Пусть для некоторого свойства формул P (A) доказаны следующие утверждения:

1) если формула A – одна из аксиом (A ₁), (A ₂), (A ₃), то P (A) верно;

2) если формула A непосредственно следует по правилу (MP) из формул B, B Þ A, P (B) верно, P (B Þ A) верно, то P (A) верно.

Тогда свойство P (A) верно для всех формул A (системы S ₁).

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