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

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

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

ИНСТИТУТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ И АВТОМАТИЗИРОВАННЫХ СИСТЕМ 
УПРАВЛЕНИЯ 
 
Кафедра автоматизированных систем управления

Москва  2019

№ 3786

Е.В. Зайцева

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

Учебное пособие

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

УДК 004 
 
3-17

Р е ц е н з е н т 
канд. техн. наук, доц. Д.В. Калитин

Зайцева Е.В.
3-17  
Формальные системы : учеб. пособие / Е.В. Зайцева. – М. : 
Изд. Дом НИТУ «МИСиС», 2019. – 70 с.
ISBN 978-5-907226-02-9

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

УДК 004

 Е.В. Зайцева, 2019
ISBN 978-5-907226-02-9
 НИТУ «МИСиС», 2019

ОГЛАВЛЕНИЕ

Предисловие ..............................................................................................4
1. Формальная аксиоматическая теория .................................................6
1.1. Формализация математических теорий .......................................... 6
1.2. Общие сведения о формальных и аксиоматических системах .... 8
Контрольные вопросы  ...........................................................................11
2. Классическое исчисление высказываний .........................................12
2.1. Пропозициональные связки и основные логические операции 12
2.2. Основные логические операции  
и их логический смысл  ......................................................................... 13
2.3. Понятие формулы исчисления высказываний  ............................ 15
2.4. Доказуемые формулы исчисления высказываний....................... 18
Порядок построения доказуемых формул ...................................... 20
2.5. Правила вывода исчисления высказываний  ............................... 21
2.6. Производные правила вывода ....................................................... 25
2.7. Понятия выводимости и вывода из совокупности формул ........ 30
2.8. Основные правила выводимости .................................................. 32
2.9. Примеры доказательства некоторых логических законов ......... 43
2.10. Проблемы аксиоматического исчисления высказываний ........ 48
Контрольные вопросы  .......................................................................... 51
3. Логика предикатов ..............................................................................53
3.1. Основные понятия, связанные с предикатами............................. 53
3.2. Логические операции над предикатами ....................................... 55
Кванторные операции ....................................................................... 56
3.3. Понятие формулы предикатов ....................................................... 59
3.4. Логическое значение формулы логики предикатов .................... 60
Равносильные формулы логики предикатов ................................... 61
3.5. Предваренная нормальная форма формулы предиката .............. 64
3.6. Общезначимость и выполнимость формул .................................. 66
Контрольные вопросы ........................................................................... 68
Библиографический список ...................................................................69

ПРЕДИСЛОВИЕ

Формализация математических теорий состоит в формализации 
мыслительных процессов, процессов построения умозаключений при 
построении математической теории, т.е. в слиянии математической 
теории и математической  логики. 
Этот шаг впервые был сделан в работах Д. Гильберта и его школы, 
когда был разработан так называемый метод формализма в основаниях математики. В рамках этого направления была достигнута следующая стадия уточнения аксиоматической теории, а именно выработано 
понятие формальной аксиоматической теории или формальной системы. В результате этого уточнения оказалось возможным представлять 
сами математические теории как точные математические объекты и 
строить общую теорию, или метатеорию, таких теорий. 
Точное определение понятия доказательства, во-первых, позволяет сделать доказательство объектом математического исследования и, 
во-вторых, с точки зрения информатики позволяет алгоритмизировать 
и осуществлять с помощью компьютеров проверку и поиск доказательств. Последнее позволяет широко применять математическую 
логику в информатике, например, разрабатывать экспертные системы. 
В первой главе пособия точно определены понятия формальной 
аксиоматической теории и рассмотрена история ее развития. В этой 
главе сформулирован алгоритм формирования строгой формальной 
теории.
Вторая глава посвящена логике высказываний и исчислениям для 
нее. Определяется формальный язык для записи высказываний, называемый языком логики высказываний, и семантика этого языка – то, 
как каждой формуле этого языка сопоставляется ее истинное значение. Затем из этого языка выделяются формулы, представляющие в 
символическом виде способы рассуждений (логические законы). Вводится понятие исчисления как некоторого способа получения (или 
вывода) заключений из принятых в качестве аксиом или   ранее  установленных утверждений. 
В третьей главе изучается логика предикатов. Вводится (формальный) язык первого порядка, предназначенного для точной записи различных утверждений. Этот язык более выразителен, чем язык логики 
высказываний, потому что в языке первого порядка есть обозначения 
для объектов, для свойств упорядоченных n-объектов и для функций, 

а также можно ставить кванторы по объектам. Определяется семантика языка первого порядка – то, как каждая формула этого языка получает истинное значение. Затем из этого языка выделяются логические 
законы и изучаются механические способы их вывода: исчисление 
предикатов. 
В пособии обобщены и использованы материалы многих авторов, 
занимающихся проблемами аппроксимации формальных систем, однако впервые сделана попытка систематически изложить основные 
понятия, относящиеся к систематике формализованных логико-математических языков, к элементам теории множеств, основам классической логики, исчислениям высказываний и предикатов, в едином 
учебном пособии.

1. ФОРМАЛЬНАЯ АКСИОМАТИЧЕСКАЯ 
ТЕОРИЯ

1.1. Формализация математических теорий

Формализация математических теорий состоит в формализации 
мыслительных процессов слияния и процессов построения умозаключений, т.е. процесса слияния математической теории и математической логики. 
Истоки понятия формальной аксиоматической теории возникли на 
рубеже XYII–XYIII вв. и принадлежат великому математику Готфриду Вильгельму Лейбницу, пожелавшему заменить идеи конкретными 
вычислениями с использованием специальных символов или знаков. 
Это была эпоха расцвета аксиоматической теории древних греков, 
идущая от Аристотеля и Евклида, с методологической схемой аксиома – доказательство – теорема – определение – доказательство –
теорема – ..., выходящей за рамки геометрии и математики и оказавшей влияние на новые области философии и естествознания.
Немецкому философу и математику Г. Лейбницу принадлежит 
мысль сформулировать правила математического доказательства, чтобы избежать рассуждения о содержательном смысле математических 
выражений, т.е. создать calculus ratiocinator –исчисление, в котором 
естественные содержательные доказательства заменены формальными вычислениями с использованием символики, где представлены аксиомы, теоремы и определения математики. Такая символика 
была целью лейбницевского языка формул, знаменитой characteristica 
universalis.
Немецкий математик Д. Гильберт предложил свой путь преодоления трудностей в основаниях математики, базирующийся на применении аксиоматического метода, с помощью которого математические 
утверждения записываются в виде логических формул, некоторые из 
которых выделяются в качестве аксиом, а остальные логически из 
них выводятся. Это направление получило название формализм.
В работах Д. Гильберта и последователей его школы был разработан так называемый метод формализма в основаниях математики, 
базирующийся на применении аксиоматического метода, при использовании которого математические утверждения записываются при 
помощи особой символики в виде логических формул, причем неко

торые из этих формул выделяются в качестве аксиом, а остальные выводятся из них логическим путем.
В рамках этого направления была достигнута следующая стадия 
уточнения понятия формальной аксиоматической теории, или формальной системы, в результате чего оказалось возможным представить математические теории как точные математические объекты и 
строить общую теорию или метатеорию.
Процессы логического мышления заменяются манипуляциями 
различного рода формул по строго очерченным правилам, причем из 
уже построенных формул разрешается чисто механически по точно 
указанным схемам (рецептам) составлять новые формулы, что заменяет сознательные умозаключения, выводящие из одного предложения другое. Таким образом, математическое и логическое содержание 
представляет собой цепочки формул, изображающих математические 
и логические аксиомы, и может быть неограниченно продолжено путем механического составления новых формул.
Программа формализации была выдвинута Д. Гильбертом с целью 
доказательства непротиворечивости использования точных математических методов, предусматривающих процесс формализации доказательств, заменяя утверждение теории конечными последовательностями 
определенных знаков, а логические способы заключения – формальными правилами образования новых формально представленных высказываний из уже доказанных в рамках формальной аксиоматической теории.
Вопросы формализации аксиоматических теорий подтверждают работы Дедекинда, Кантора, Буля, Пеано, Пирса, Шредера и т.п. 
Высокой степени точности формализация математического языка в 
рамках современных логических исчислений достигла в работах математиков XX в. Рассела, Гильберта, Гёделя, Чёрча, А.А. Маркова, 
А.И. Мальцева и др. Это время бурного развития математической логики, формирования её новых разделов, таких как различные аксиоматические теории множеств, теория моделей и теория алгоритмов, 
с помощью которой были выработаны несколько формализаций понятия алгоритма. Были созданы многие новые неклассические логические системы.
Кроме того, XX в. – это период начала глубокого проникновения 
идей и методов математической логики в технику, процесс конструирования и создания ЭВМ, программирование, кибернетику, вычислительную математику, структурную лингвистику.

Мощное развитие логики и логического языка привело к созданию 
особой области математики – оснований математики, предметом изучения которой стало строение математических утверждений и математических теорий. Одной из фундаментальных идей исследований 
по основаниям математики  является идея формализации математических теорий, т.е. последовательное проведение аксиоматического 
метода построения теорий.

1.2. Общие сведения о формальных 
и аксиоматических системах
Во введении уже говорилось, что в основе любой логики лежит 
определенная система, задающая правила формирования логических 
выражений, используемых механизмов построения рассуждений и 
т.п. Системы такого рода называются формальными. Рассмотрим общие положения, которые лежат в основе построения таких систем.
Определение 1.1. Формальная система представляет собой совокупность чисто абстрактных объектов, не связанных с внешним 
миром, в которой представлены правила оперирования множеством 
символов только в синтаксической трактовке без учета смыслового 
содержания.
Всякая формальная система строится на основе формализованного языка (как средства формирования и изложения выражений, имеющих смысл в данной теории) и совокупности теорем. Так же как в 
естественном языке средством выражения мысли является предложение, построенное по определенным правилам, в математике средством выражения является формула, построенная из заданного набора символов. В формальной теории все формулы доказываются.
Под теоремой в формальной системе понимают высказывание, истинное в данной системе. Это обоснованное и строгое утверждение, 
которое строится на основе определенных логических правил и доказательства. Доказательство – это способ получения одних выражений 
из других с помощью операций над символами и построения обоснованной аргументации, следствием которой и является теорема.
При построении любой формальной теории (системы) в качестве 
исходных посылок всегда используются некоторые неопределяемые 
термины и аксиомы. Неопределяемые термины – это те термины и 
понятия, смысл и содержание которых считается уже известным, через них вводятся все новые понятия и термины. Совершенно анало

гично вводится некоторая часть постулатов (формул), которые, как 
считается в данной теории, не требуют доказательства. Обычно это 
утверждения, правильность которых не вызывает сомнения, и они 
принимаются как очевидные истины. Такие выражения (формулы) 
называют аксиомами, а системы, в основе построения которых лежит 
использование аксиом, называются аксиоматическими системами.
Формирование строгой формальной теории осуществляется в следующем порядке:
1) Задается конечное множество символов, которые образуют алфавит формальной системы.
2) Устанавливаются процедуры построения формул формальной 
системы.
3) Устанавливается множество аксиом, т.е. формул, истинность которых не требует доказательства. Обычно к ним относят те утверждения, которые полагаются очевидными по самой природе рассматриваемых понятий.
4) Устанавливается конечное множество правил вывода, которые 
позволяют получать новые формулы из некоторого множества известных формул. В общем случае эти правила могут быть представлены в 
виде 
1
2
&
&...&
→
m
H
H
H
M , что означает: из множества истинных 
формул 
1
2
m
H ,H ,...,H , указанных в левой части выражения, следует 
истинность формул правой части выражения. Говорят, что формула 
М, полученная в результате применения правила вывода, выводима в 
данной теории. Таким образом, правила вывода позволяют, последовательно применяя их, получать новые истинные формулы или теоремы из аксиом и ранее выведенных формул.
Теперь с учетом понятия правила вывода уточним понятия формального доказательства и теоремы.
Определение 1.2. Формальным доказательством или просто доказательством называется последовательность формул M1, M2, ..., 
Mn такая, что каждая формула Mi является либо аксиомой, либо выводима из предшествующих ей формул.
Определение 1.3. Формула t называется теоремой, если существует доказательство, в котором она является последней.
Задаваемые при описании формальной системы правила вывода 
называют также правилами вывода заключений, т.е. они позволяют 
определить, является ли данная формула теоремой данной формальной системы или нет.

Различают два типа правил вывода.
1) Правила, применяемые к формулам, рассматриваемым как единое целое, в этом случае их называют продукционными правилами.
Пример. x < y и 
<
→
<
y
z
x
z  – это продукция с двумя посылками.
2) Правила, которые могут применяться к любой отдельной части 
формулы, причем сами эти части являются формулами, входящими в 
состав формальной системы. В этом случае их называют правилами 
переписывания.
Пример. x – x = 0, это выражение имеет смысл при любом значении входящей в него в качестве подвыражения переменной х.
Определение 1.4. Формальная система называется разрешимой, 
если существует хорошо определенный способ действия, который за 
конечное число шагов для любой формулы формальной системы позволяет определить, выводима она в данной системе или нет. Сам способ действий, если он существует, называют процедурой разрешения.
Так как формальные системы всегда представляют собой модель 
какой-то реальности, то возникает вопрос об установлении взаимосвязи между объектами формальной системы и этой реальностью, для 
этого вводится понятие интерпретации.
Определение 1.5. Интерпретация представляет собой распространение исходных положений какой-либо формальной системы на 
реальный мир. Интерпретация придает смысл каждому символу формальной системы и устанавливает взаимно однозначное соответствие 
между символами формальной системы и реальными объектами. Теоремы формальной системы, будучи интерпретированы, становятся 
после этого утверждениями в обычном смысле слова, и в этом случае 
уже можно делать выводы об их истинности или ложности.
Следует отметить, что при интерпретации речь идет о замыкании или 
логическом завершении математического подхода, который в общем случае можно описать в виде следующей последовательности действий:
 – вначале изучается реальность и конструируется некоторое абстрактное представление о ней, т.е. некоторая формальная система;
 – затем строится доказательство теорем формальной системы. 
Вся польза и удобства формальных систем заключаются в их абстрагировании от конкретной реальности. Благодаря этому одна и та же 
формальная система может служить моделью многочисленных конкретных ситуаций;

– происходит возвращение к начальной точке всего построения и 
осуществляется интерпретация теорем, полученных при формализации.
Замечание. Изучение аксиом и теорем как абстрактных выражений, представленных в некоторой форме, называется синтаксическим изучением аксиоматических систем (АС); изучение и рассмотрение смысла этих выражений называется семантическим 
изучением АС. Отметим, что с синтаксическим аспектом АС и связано понятие формальной системы.
Формальную теорию часто называют исчислением. Под исчислением понимают формальное представление теории, которое позволяет 
оперировать с объектами без учета формального смысла выражений.
В рамках создания формальной системы, как правило, решаются 
(должны быть решены) следующие проблемы:
1) Проблема противоречивости. Логическое исчисление называется непротиворечивым, если в нем недоказуемы никакие две формулы, из которых одна является отрицанием другой;
2) Проблема полноты. Система исчисления считается полной, 
если любая теорема теории может быть доказана или опровергнута;
3) Проблема независимости аксиом. Для начала введем понятие 
независимой аксиомы. Аксиома называется независимой, если она не 
может быть выведена из других аксиом. Система аксиом исчисления 
называется независимой, если каждая аксиома в ней независима. 
4) Проблема разрешимости. Система исчисления называется разрешимой, если существует алгоритм, позволяющий по каждому утверждению выяснить, является оно истинным или ложным.
Описание всякого исчисления включает в себя описание символов 
этого исчисления (алфавита), формул, являющихся конечными конфигурациями символов, и определение выводимых формул.

Контрольные вопросы 

1. Понятие классических формальных аксиоматических систем.
2. Объекты формальной системы.
3. Язык и понятие формулы формальной аксиоматической теории.
4. Порядок формирования формальной теории.
5. Определение формального доказательства.
6. Правила вывода в формальных системах.
7. Какие проблемы решаются при создании формальных систем.