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

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

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

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

Москва  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 в. – это период начала глубокого проникновения 
идей и методов математической логики в технику, процесс конструирования и создания ЭВМ, программирование, кибернетику, вычислительную математику, структурную лингвистику.