Формальные системы

Москва 2019

МИНИС ТЕРС ТВО НАУКИ И ВЫСШ ЕГО О Б РА З О ВА Н И Я РФ

ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ АВТОНОМНОЕ ОБРАЗОВАТЕЛЬНОЕ УЧРЕЖДЕНИЕ 
ВЫСШЕГО ОБРАЗОВАНИЯ 
«НАЦИОНАЛЬНЫЙ ИССЛЕДОВАТЕЛЬСКИЙ ТЕХНОЛОГИЧЕСКИЙ УНИВЕРСИТЕТ «МИСиС»

Институт информационных технологий и автоматизированных систем управления 
 
Кафедра автоматизированных систем управления

Е.В. Зайцева

ФОРМАЛЬНЫЕ СИСТЕМЫ

Практикум

Рекомендовано редакционно-издательским 
советом университета

№ 3355

УДК 004 
 
3-17

Р е ц е н з е н т 
канд. техн. наук, доц. Л.П. Волкова

Зайцева Е.В.
3-17  
Формальные системы : практикум / Е.В. Зайцева. – М. : Изд. 
Дом НИТУ «МИСиС», 2019. – 36 с.

Практикум содержит набор задач и упражнений, необходимый для закрепления и расширения лекционного материала по таким разделам, как исчисление высказываний, алгебра предикатов и исчисление предикатов, именно то, 
что входит в понятие «формальные системы».
Практикум предназначен для бакалавров, по направлению «Информатика 
и вычислительная техника».

УДК 004

 Е.В. Зайцева, 2019
 НИТУ «МИСиС», 2019

СОДЕРЖАНИЕ

Введение ....................................................................................................4

Практическое занятие 1. Исчисление высказываний ............................... 5
1.1. Теоретическая часть .......................................................................... 5
1.2. Задачи  ................................................................................................ 8

Практическое занятие 2. Предикаты и отношения ..................................11
2.1. Теоретическая часть .........................................................................11
2.2. Задачи и упражнения .......................................................................11

Практическое занятие 3. Алгебра предикатов ........................................ 15
3.1. Теоретическая часть ........................................................................ 15
3.2. Задачи ............................................................................................... 20

Практическое занятие 4. Исчисление предикатов .................................. 30
4.1. Теоретическая часть ........................................................................ 30
4.2. Задачи ............................................................................................... 32

Библиографический список ...................................................................35

ВВЕДЕНИЕ

Формальные системы в АСУ являются наукой о логических рассуждениях, использующей математические методы, при которых из 
верных исходных умозаключений путем применения законов человеческого мышления получают достоверные результаты.
Применение формальных систем позволило представить логические теории в новой совершенной форме с использованием аксиоматического метода в построении формализованных математических 
теорий.
Формальные системы для АСУ включают: исследование различных логических вычислений, таких как классическое исчисление высказываний и предикатов, и изучение взаимосвязанных синтаксических (информационных) и семантических (реальных) объектов.
Использование формальных систем позволяет проводить и исследовать аксиоматизацию классов алгебраических объектов и на основании аксиоматизации судить о свойствах самих классов, используя 
механизм логического рассуждения и доказательства.
Бурное развитие теории множеств, классического исчисления высказываний и предикатов во многом обусловлено прогрессом компьютерной техники, необходимостью создания средств обработки и 
передачи информации, а также представления математических моделей в АСУ.
В настоящем практикуме обобщены и использованы материалы 
многих авторов, занимающихся проблемами аппроксимации формальных систем, однако впервые сделана попытка систематически 
изложить основные понятия, относящиеся к систематике формализованных логико-математических языков, к элементам теории множеств, основам классической логики, исчислениям высказываний и 
предикатов в едином учебном пособии.

Практическое занятие 1

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

1.1. Теоретическая часть

Любое логическое исчисление создается как средство доказательства утверждений или вывода одних утверждений из других в некоторой предметной области знаний и задается алфавитом, правилами 
образования формул в этом алфавите, набором формул, называемых 
аксиомами, и правилами вывода одних формул из других.
Алфавит исчисления высказываний (ИВ) состоит из тех же символов, что и в алгебре высказываний (АВ), за исключением символов 
для обозначения постоянных высказываний Множество формул ИВ 
совпадает с множеством формул АВ, не содержащих постоянных высказываний.
В качестве аксиом ИВ здесь приняты следующие формулы:
1) Группа I:

 
(
)
A
B
A
→
→
; 
(1.1)

 
(
)
(
)
(
)
(
)
(
)
A
B
C
A
B
A
C
→
→
→
→
→
→
; 
(1.2)

2) Группа II:

 
AB
A
→
; 
(1.3)

 
AB
B
→
; 
(1.4)

 
(
)
(
)
(
)
(
)
A
B
A
C
a
CB
→
→
→
→
→
; 
(1.5)

3) Группа III:

 
A
A
B
→
∨
; 
(1.6)

 
B
A
B
→
∨
; 
(1.7)

 
(
)
(
)
(
)
(
)
A
C
B
C
A
B
C
→
→
→
→
∨
→
; 
(1.8)

4) Группа IV:

 
A
A
→
; 
(1.9)

A
A
→
; 
(1.10)

 
(
)
(
)
 
 
A
B
B
A
→
→
→
. 
(1.11)

Система правил вывода ИВ состоит из одного правила, называемого правилом заключения (ПЗ) (или правилом «Modus ponens») и записываемого в виде

 
,
.
A A
B
B
→
 
(1.12)

Заметим, что в аксиомах и в ПЗ под А, В, С понимаются любые 
формулы ИВ. В связи с этим их называют также схемами аксиом и 
правилами вывода.
Выводом формулы А из множества формул Т называется конечная 
последовательность формул A1, A2, ..., An, в которой An = A, и каждая 
из формул Ai, i = 1, 2, ..., n является или аксиомой, или формулой из Т, 
или получается по правилу вывода из предыдущих формул. При этом 
формула А называется выводимой из системы Т, что записывается 
в виде T├A или B1, B2, ..., BK ├A, если 
{
}
1
2
,
,...,
.
K
T
B B
B
=
 Формула 
А, выводимая из пустого множества формул, называется доказуемой 
формулой, что обозначается в виде ├А.
Если

 
1
2
,
,...,
K
B B
B ├A, 
(1.13)

то к системе правил вывода можно присоединить правило

 
1
2
,
,...,
.
K
B B
B
A
 
(1.14)

Дополнительные правила вывода, построенные по указанной схеме, будут называться вспомогательными.
Формулы ИВ называются равносильными, если любая одна из них 
выводима из другой.
В построении выводов формул и в получении вспомогательных 
правил вывода зачастую используется следующая
Теорема дедукции. Для произвольного множества формул Т и любой формулы А исчисления высказываний

 
{ }
T
A

├ B
T
⇔
├
.
A
B
→
 
(1.15)

Применив, для примера, эту теорему к аксиоме (1.1), получим 
вспомогательное правило вывода

.
A
B
A
→
 
(1.16)

Для каждого логического исчисления принципиальное значение 
имеют три проблемы.
1) Проблема полноты, то есть достаточности для доказательства 
всех истинных утверждений той предметной области, для которой 
строилось исчисление. Для ИВ такой областью является АВ. 
2) Проблема непротиворечивости, то есть невозможности доказательства некоторой формулы и ее отрицания.
3) Проблема разрешимости, то есть построения алгоритма, позволяющего для любой формулы установить, доказуема она или нет.
При решении некоторых вопросов о логических исчислениях используются их интерпретации.
Под интерпретацией произвольной системы формул Т исчисления 
высказывании понимают любую алгебру H с определенными на ней 
каким либо образом операциями 
, ,
,
∧ ∨ →
 и с 0-арной операцией е, 
удовлетворяющую следующему условию: все формулы из Т принимают значение е при произвольной замене входящих в них переменных 
элементами из Н, и таким же свойством обладают все формулы, выводимые из Т.
Для ИВ положительное решение трех указанных проблем легко 
следует из теоремы: формула ИВ доказуема тогда и только тогда, 
когда она тождественно истинна в АВ. Из этой теоремы видно, в 
частности, что АВ является интерпретацией системы аксиом ИВ. 
Пользуясь этой теоремой, вопрос о доказуемости формулы можно 
решить путем вычисления ее значений в АВ. Однако этот путь для 
формул от большого числа переменных может оказаться практически 
неосуществимым. В то же время построение доказательства формулы 
не зависит от числа переменных и в некоторых случаях быстрее приводит к цели. Поэтому логические исчисления находят применение 
на практике, и в частности при решении вопросов, связанных с защитой информации. К тому же для некоторых исчислений существуют 
программы автоматического доказательства формул.
Предлагаемые в данном параграфе упражнения нацелены на выработку навыков построения доказательств, и поэтому требуемые в них 
выводы и доказательства формул необходимо строить по их определениям, не прибегая к помощи указанной выше теоремы о доказуемости тождественно истинных формул.

1.2. Задачи 

Задача 1-01
Для произвольных формул А, В доказать утверждения:
а) ├A→A,

б) ├A
,
A
∨

в) ├
.
AA
B
→

Задача 1-02
Доказать, что система формул T противоречива (т. е. Т ├ А и T ├ 

A для некоторой формулы А) тогда и только тогда, когда Т ├ В для 
любой формулы В.

Задача 1-03
Доказать следующие вспомогательные правила вывода:
а) правило силлогизма:

,
;
A
B B
C
A
C
→
→
→

б) правило умножения заключений:

,
;
A
B A
C
A
BC
→
→
→

в) правило сложения посылок:

,
;
A
C B
C
A
B
C
→
→
∨
→

г) правило контрапозиции:

.
A
B
B
A
→
→

Задача 1-04
Доказать следующие правила монотонности логических операций 
(А, В, С, D — произвольные формулы ИВ):
а) 
,
A
B C
D
→
→
├ AC
BD
→
;
б) 
,
A
B C
D
→
→
├ A
C
B
D
∨
→
∨
;

в) 
,
A
B C
D
→
→
├ (
)
(
)
B
C
A
D
→
→
→
.

Задача 1-05
Для формул А и В исчисления высказываний символом А ~ В обозначается формула 

(
)(
)
A
B
B
A
→
→

Формулы А и В равносильны, если ├ А ~ В.
1) Доказать, что введенное бинарное отношение ~ является отношением эквивалентности на множестве формул исчисления высказываний;
2) Доказать, что все доказуемые формулы исчисления высказываний равносильны.

Задача 1-06
Доказать теорему равносильности для исчисления высказываний: если некоторую подформулу В формулы А(В) заменить равносильной ей формулой B1, и при этом получится формула А1(В1), то 
А1(В1) равносильна исходной формуле А(В).

Задача 1-07
Установить следующие равносильности:
1) ├ AB ~ BA;
2) ├ A
B
∨
~ 
;
B
A
∨

3) ├ (
)
(
)
~
AB C
A BC ;

4) ├ (
)
(
)
 ~
A
B
C
A
B
C
∨
∨
∨
∨
;

5) ├ 
(
) ~
A B
C
AB
AC
∨
∨
;

6) ├ 
(
)(
)
~
A
BC
A
B
A
C
∨
∨
∨
;

7) ├ 
(
) ~
A A
B
A
∨
;
8) ├ 
~
A
AB
A
∨
;
9) ├ 
~
AA
A;
10) ├ 
~
A
A
A
∨
;

11) ├ 
~
AB
A
B
∨
;

12) ├ 
~
A
B
A
B
∨
∧
;

13) ├ (
) (
)
~
A
B
B
A
→
→
;

14) ├ 
~
A
A ;

15) ├ (
) (
)
~
A
B
A
B
→
∨
.

Задача 1-08

Пусть H = {0,1} – алгебра с операциями 
, ,
,
∧ ∨ →
, где операция 
∧ определена соотношением x ∧ y = y, а остальные операции – как в 
алгебре высказываний.
1) Доказать, что алгебра Н является интерпретацией системы формул, полученной удалением из системы аксиом ИВ одной лишь аксиомы (1.3).
2) Пользуясь этой интерпретацией, доказать независимость аксиомы (1.3) от системы всех остальных аксиом ИВ.

Задача 1-09
Рассмотренным в задаче 1-08 методом доказать независимость 
всей системы аксиом ИВ. Указание. Взять H = {0,1} для аксиом групп 
II–IV, H = {0,1,2,3} для аксиомы (1.1), Н={0,1,2} для аксиомы (1.2). 
Для аксиомы (1.1) положить

{
}
{
}
min
,
,
max
,
,
3
,
0
x
y
x y
x
y
x y
x
x x
y
∧
=
∨
=
=
−
→
=
 

при х > у и 3 в остальных случаях. Для аксиомы (1.2) положить 

{
}
min
,
,
2
,
x
y
x y
x
x x
y
x
y
∧
=
=
−
∨
=
+
 

при 
{
}
,
0,1
x y∈
 и 2 в остальных случаях, 1→ 0 = 2 → 1 = 1, 2→ 0 = 0 и 
x→ у = 2 в остальных случаях.

Задача 1-10
Доказать, что алгебра высказываний является интерпретацией системы аксиом ИВ, и вывести отсюда непротиворечивость ИВ.

Практическое занятие 2

ПРЕДИКАТЫ И ОТНОШЕНИЯ

2.1. Теоретическая часть

Пусть М – непустое множество. Под n-местным (или n-арным) 
предикатом на множестве М понимают всякое предложение, которое 
содержит п различных переменных, принимающих значения из М, и 
превращается в высказывание при замене переменных произвольными элементами из М. Под 0-местными предикатами понимаются постоянные высказывания.
Всякое подмножество 
n
R
M
⊆
 называется n-арным отношением 
на М. По п-арному предикату р естественным образом определяется 
n-арное отношение R на М:

 
1
2
1
2
1
2
,
,...,
:(
,
,...,
)
(
,
,...,
)
n
n
n
a a
a
M
a a
a
R
p a a
a
∀
∈
∈
⇔
= И. 
(2.1)

Бинарное отношение R на множестве М называется рефлексивным, симметричным, антисимметричным, транзитивным, если соответственно выполняются условия:

 
:( , )
;
a
M
a a
R
∀ ∈
∈
 
(2.2)

 
,
:(( , )
)
(( , )
);
a b
M
a b
R
b a
R
∀
∈
∈
⇒
∈
 
(2.3)

 
,
:(( , )
)
(( , )
)
(
);
a b
M
a b
R
b a
R
a
b
∀
∈
∈
∧
∈
⇒
=
 
(2.4)

 
, ,
:(( , )
)
(( , )
)
(( , )
.
a b c
M
a b
R
b c
R
a c
R
∀
∈
∈
∧
∈
⇒
∈
 
(2.5)

Рефлексивное, транзитивное и симметричное отношение на множестве М называется отношением эквивалентности на М. Рефлексивное, транзитивное и антисимметричное отношение на множестве М 
называется отношением частичного порядка на М. Частичный порядок R на множестве М называется линейным порядком, если любые 
два элемента множества М сравнимы по R, т.е. (a, b) ∈ R или (b, a) ∈ R 
для любых (a,) ∈ M.

2.2. Задачи и упражнения

Задача 2-01
Сколько различных n-арных отношений (предикатов) можно определить на m-элементном множестве? В частности, найдите число различных бинарных отношений на множестве из 4 элементов.