стр. 1
(общее количество: 9)

ОГЛАВЛЕНИЕ

След. стр. >>

Санкт-Петербургский Государственный Институт
Точной Механики и Оптики (Технический Университет)
Факультет Информационных Технологий и Программирования
Кафедра Компьютерных технологий


М. А. Коротков Е. О. Степанов



Основы формальных
логических языков




Санкт-Петербург
2003
УДК 510.62, 510.63, 510.65, 510.675, 510.676.


Коротков М. А., Степанов Е. О. Основы формальных логических языков.
СПб: СПб ГИТМО (ТУ), 2003. 84с.


Данное учебное пособие посвящено основам формальных логических языков.
В нем дается краткое изложение языков логики первого и второго порядков, эле-
ментов теории доказательств, теории моделей и формальной теории множеств.
Пособие основано на курсе лекций, читаемом на кафедре Компьютерных тех-
нологий Санкт-Петербургского Государственного Института Точной Механики и
Оптики.


Пособие предназначено для студентов компьютерных и математических спе-
циальностей.




Утверждено к печати Ученым Советом факультета Информационных Техно-
логий и Программирования, протокол №5 от 09.01.03.

ISBN 5-7577-0122-6



c Санкт-Петербургский Государственный Институт Точной Механики и Оп-
тики (Технический Университет), 2003.

c М. А. Коротков, Е. О. Степанов, 2003.
Оглавление

1 Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2 Языки логики предикатов первого порядка . . . . . . . . . . . . . . 8
2.1 Алфавит и сигнатура . . . . . . . . . . . . . . . . . . . . . . . 8
2.2 Синтаксис языка первого порядка . . . . . . . . . . . . . . . . 9
2.3 Свободные и связанные переменные . . . . . . . . . . . . . . . 12
2.4 Семантика языков логики первого порядка . . . . . . . . . . 13
3 Языки логики второго порядка . . . . . . . . . . . . . . . . . . . . . 18
4 Логические языки с равенством . . . . . . . . . . . . . . . . . . . . . 19
5 Арифметика Пеано . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
6 Элементы теории доказательств . . . . . . . . . . . . . . . . . . . . . 30
6.1 Формальные cистемы . . . . . . . . . . . . . . . . . . . . . . . 30
6.2 Естественная дедукция . . . . . . . . . . . . . . . . . . . . . . 32
6.3 Подстановки в термах и формулах . . . . . . . . . . . . . . . 36
6.4 Корректность и полнота естественной дедукции . . . . . . . . 40
7 Основы теории моделей . . . . . . . . . . . . . . . . . . . . . . . . . . 48
8 Сравнение языков логики разных порядков . . . . . . . . . . . . . . 53
9 Формальная теория множеств . . . . . . . . . . . . . . . . . . . . . . 57
9.1 Аксиоматика Цермело-Френкеля. Основные аксиомы . . . . . 59
9.2 Отношение порядка . . . . . . . . . . . . . . . . . . . . . . . . 65
9.3 Аксиома регулярности . . . . . . . . . . . . . . . . . . . . . . 68
9.4 Аксиома бесконечности . . . . . . . . . . . . . . . . . . . . . . 69
9.5 Ординалы и стандартная модель арифметики . . . . . . . . . 71
9.6 Аксиома выбора . . . . . . . . . . . . . . . . . . . . . . . . . . 79
9.7 Теория множеств и основания математики . . . . . . . . . . . 80
4 Введение


1 Введение
Формальная логика. Дать краткое, но исчерпывающее определение той или
иной науки – задача, как правило, не простая. В особенности это относится к
таким наукам, которые, как, например, математика или физика, содержат в себе
большое число различных специальных дисциплин. В значительной мере отно-
сится это и к логике, которая фактически пронизывает всю современную матема-
тику и информатику, а также является фундаментом многочисленных естествен-
нонаучных и гуманитарных дисциплин, от “абстрактных”, таких как философия,
до “прикладных”, таких как юриспруденция. Поэтому мы попробуем подойти к
понятию о предмете современной логики, не претендуя ни на полноту, ни на точ-
ность.
Общепринятым является понимание логики как науки о правильном умоза-
ключении (“логическом рассуждении”). Чтобы понять смысл этого определения,
стоит конкретизировать, что такое умозаключение, а главное, что следует по-
нимать под правильностью. Существует только два способа, которыми человек
приобретает новые знания – в результате опыта и путем умозаключения. При
этом первым способом получена только малая часть всех используемых людь-
ми знаний. Заметим, что всякое рассуждение основывается на опытных фактах
(“посылках”), которые сами по себе могут соответствовать или не соответствовать
действительности. Однако истинность или ложность посылок никак не влияют
на правильность рассуждения.
Вот очень простой, но показательный пример. Умозаключение “страус – пти-
ца, все птицы имеют крылья, следовательно страус имеет крылья” несомненно
правильное, а все использованные посылки соответствуют действительности, по-
этому истинным является и заключение. А вот в умозаключении “кит – морская
рыба, все рыбы в море селедки, следовательно кит – селедка” обе посылки лож-
ны, заключение также ложно, но само рассуждение следует признать правиль-
ным, ибо оно ничем, кроме входящих в него опытных фактов, не отличается от
предыдущего. По сути дела, оба рассуждения – это всего лишь две разные мо-
дификации одной и той же логической конструкции “y обладает свойством P ,
все x, имеющие свойство P , имеют и свойство Q, следовательно y имеет свой-
ство Q”. Здесь уже нет никаких опытных фактов, на их месте осталась только
абстрактная конструкция, которая является общепризнанно правильной, и мы
очень часто используем ее в самых разных логических рассуждениях.
Это был, конечно, только простой пример, а на практике проверить правиль-
ность сложных умозаключений можно только сведением их к последовательно-
сти таких вот элементарных общепризнанно правильных рассуждений (в этом
и состоит процесс доказывания заключения из заданных посылок). Таким об-
разом, правильность умозаключений вводится и проверяется совершенно фор-
5


мально, без какой-либо связи с истинностью входящих в него посылок, т.е. ис-
ключительно с точки зрения структуры рассуждения. Поэтому логику, изучаю-
щую правильные умозаключения, часто называют формальной логикой (иногда
приходится встречать название логистика). С практической точки зрения самое
важное свойство такой формальной правильности рассуждений заключается в
следующем: если нам удалось доказать, пользуясь методами формальной логи-
ки, правильность рассуждения, и нам известно из опыта, что все используемые
посылки истинны, то мы можем быть уверены в истинности заключения.
Строго говоря, логика несколько шире формальной логики – например, по-
следняя не отвечает на вопросы, какие рассуждения считать “элементарными” и
почему. Для ответа на них приходится углубляться в философию и психологию.
Однако, как правило, предмет логики ограничивают все-таки именно вопросами
формальной логики, так что логика и формальная логика оказываются просто
синонимами. Некоторые базовые вопросы относят к философским основаниям
логики, хотя граница между логикой и философией весьма размыта. В дальней-
шем мы будем заниматься именно формальной логикой, хотя нам придется часто
обращаться к ее внелогическим, в т.ч. общефилософским основаниям и выводам.
Символьная и математическая логика. В конце XIX – начале XX века
логика, являющаяся одной из наиболее древних наук (по современным представ-
лениям, рождение логики связано с деятельностью софистов в Древней Греции
в 4-5 веке до н.э. – именно они создали логику как науку и активно использо-
вали ее, в частности, для обучения ведению судебных споров; к этой же эпохе
относится и деятельность первого ученого, систематизировавшего разрозненные
логические знания – “отца логики” Аристотеля) пережила невиданную по своим
масштабам и значению революцию. Вначале преобразования казались несуще-
ственными и заключались в активном использовании в логических исследовани-
ях символьной записи. Разработанная в 40-70х гг. прошлого века Дж. Булем, а
затем развитая другими учеными (в основном математиками, в т.ч. Г. Кантором)
символьная запись логических рассуждений оказалась очень удобной и быстро
завоевала популярность, превратив формальную логику в символьную логику.
Например, рассмотренное выше логическое рассуждение “y обладает свойством
P , все x, имеющие свойство P , имеют и свойство Q, следовательно y имеет свой-
ство Q”, в современной записи выглядит очень компактно

P (y), ?x(P (x) > Q(x)) Q(y).

При этом P (y) обозначает “y обладает свойством P ”, P (x) > Q(x) обознача-
ет “если x имеет свойство P , то x имеет свойство Q”, ?x(...) обозначает “для
всех x верно (...)”, а обозначает “доказывает”. “Символьная” революция в ло-
гике совпала по времени со столь же революционными преобразованиями в ма-
тематике. Основными вехами этих преобразований было появление созданной
6 Введение


Г. Кантором теории множеств, качественным повышением требований к строго-
сти доказательств, прежде всего в математическом анализе в результате работ
К. Вейерштрасса, активным поиском общих теоретикомножественных оснований
математического анализа и математики в целом. Возникшие на этом пути труд-
ности оказались принципиальными и потребовали значительной формализации
оснований математики с использованием методов символьной логики. В свою
очередь, произошедшее таким образом соприкосновение логики и математики
привело к их взаимопроникновению настолько, что считавшаяся ранее частью
философии логика оказалась пропитанной математическими методами, которые
оказались эффективными и в применении к чисто логическим задачам. В ре-
зультате современная логика полностью базируется на математических методах
и часто находит приложение в задачах математики и прикладных математиче-
ских дисциплин, включающих теоретическую информатику, и является, таким
образом, математической логикой. Однако нет никакого смысла в противопо-
ставлении “логики” и “математической логики”, так как математическая логика
представляет собой современное развитие классической логики, основы которой
заложены еще Аристотелем.
Формальные языки. Современная логика изучает формальные языки, слу-
жащие для выражения логических рассуждений. Используемые для этой цели
математические методы пригодны для изучения и значительно более широкого
класса формальных языков.
Любой язык, как естественный (русский, английский, латинский), так и фор-
мальный (языки программирования, язык шахматной записи, языки логики пре-
дикатов), служит для передачи информации. С этой точки зрения язык представ-
ляет собой совокупность знаковой системы (включающей в себя набор символов
для передачи текстов и правила написания текстов, называемые синтаксисом
языка) и набора смыслов, которые можно сопоставить текстам языка, а также
правил сопоставления смысла текстам языка, называемых семантикой языка.
Вопросы синтаксиса, как правило, существенно проще семантических вопросов
и гораздо легче поддаются формальному анализу.
Чтобы задать язык, необходимо прежде всего задать его алфавит – множе-
ство объектов (“символов”), из которых составляются тексты языка. Алфавитом
языка может, вообще говоря, служить произвольное множество. Например, ал-
фавит английского языка состоит из букв латинского алфавита, арабских цифр
и знаков пунктуации, письменный язык индейцев майя – из узелков. Также из
букв латинского алфавита, арабских цифр и некоторых специальных символов
(например, #) состоит алфавит большинства распространенных языков програм-
мирования.
Далее мы будем говорить только о формальных языках. Пусть задано множе-
ство V – алфавит языка. Элементы этого множества мы будем называть симво-
7


лами алфавита. Цепочками (string) будем называть конечные позиционные на-
боры символов алфавита с учетом порядка следования символов. В дальнейшем
мы, как правило, будем иметь дело с довольно распространенной ситуацией, ко-
гда символы алфавита представляют собой знаки, которые могут быть записа-
ны на бумаге. В этом случае цепочки символов будем записывать так, как это
принято в европейских языках – слева направо в порядке следования символов.
Пустая цепочка символов это пустое множество символов. Множество всех це-
почек, включая пустую, будем обозначать V ? . Формальный язык с алфавитом
V это просто заданное подмножество L ? V ? . Элементы этого множества могут
называться по-разному для разных языков. Например, элементы языков логики
предикатов принято называть формулами, элементы языков программирования
– программами, элементы языка шахматной записи – ходами (или записями хо-
дов), а элементы языков, в той или иной мере моделирующих естественные –
предложениями или фразами.
Задать формальный язык (т.е. правило, по которому формируется множество
L ? V ? ) можно по-разному. Чаще всего для этой цели используют формальные
грамматики. Нас будет интересовать только один весьма распространенный тип
формальной грамматики – контекстно-свободная грамматика, записываемая в
форме Бэкуса-Наура.
Язык и метаязык. Для описания синтаксиса и семантики формального язы-
ка мы, как правило, будем пользоваться естественным (в данном случае русским)
языком. Например, фраза “Ход e2–e4 состоит в передвижении пешки с поля e2
на поле e4”, является предложением русского языка, объясняющим смысл записи
e2–e4 на формальном языке шахматной записи. Использовать для этой же цели
можно было бы и другой язык, как естественный, так и формальный, специаль-
но предназначенный для описания синтаксиса и семантики данного формально-
го языка. В таком случае будем называть тот язык, который используется для
описания данного формального языка, метаязыком для последнего, а “описыва-
емый” язык предметным языком. Приставка греческого происхождения “мета”, в
прямом переводе означающая “следующий за”, имеет здесь значение “над”.
Стоит отметить, что предметный формальный язык и метаязык, как прави-
ло, отличаются друг от друга. Метаязык обычно в некотором смысле богаче,
например, его алфавит часто строго содержит алфавит предметного языка. Де-
ло в том, что многие формальные языки, в том числе и те, которые мы будем
рассматривать в дальнейшем, недостаточно богаты, чтобы использовать их в ка-
честве метаязыков для себя самих (это или просто невозможно, или по меньшей
мере весьма неудобно). При этом все естественные языки достаточно богаты,
чтобы с их помощью можно было бы описать их собственную грамматику (“син-
таксис”), а также проводить рассуждения о смысле тех или иных фраз этого
же языка (т.е. о семантике языка). Например, мы обучаемся русскому языку на
8 Языки логики предикатов первого порядка


русском (который в процессе обучения служит, таким образом, метаязыком для
самого себя. В то же время книжки по обучению формальным языкам, таким
как, например, языки программирования, написаны также на естественном (рус-
ском, английском и т.п.) языке, а не на самом изучаемом формальном языке
(представьте себе, можно ли было бы научиться программировать на C++, если
бы соответствующие учебники не были написаны на привычном русском языке).
Это, однако, не значит, что никакой формальный язык не может использоваться
в качестве метаязыка для себя самого: существуют и такие формальные языки,
которые, вовсе не будучи столь же богатыми, как и естественные, в принципе
могут быть использованы для “описания себя самих”.


2 Языки логики предикатов первого порядка
Языки логики предикатов представляют собой основной класс языков, с ко-
торыми приходится иметь дело в формальной логике. Разные языки этого класса
используются для описания различных предметных областей. Наибольшее при-
менение в силу ряда причин, которые мы рассмотрим позднее, получили язы-
ки логики предикатов первого порядка. Главная их особенность состоит в том,
что они достаточно выразительны (например, на языке логики первого порядка
можно описать всю математику) и в то же время легко поддаются формальному
анализу.

2.1 Алфавит и сигнатура
Алфавит A любого языка логики предикатов первого порядка состоит из шести
подмножеств

A = Const ? Func ? Pred ? Var ? Log ? Aux,

где
• Const – множество символов предметных констант,
• Func – множество функциональных символов,
• Pred – множество предикатных символов,
• Var – множество символов предметных переменных,
• Log := {¬, ?, ?, >, ?, ?} – множество логических символов,
• Aux := {, ()} –множество вспомогательных символов (запятая и круглые
скобки).
2.2 Синтаксис языка первого порядка 9


Объединение ? = Const ? Func ? Pred множеств символов предметных кон-
стант, функциональных и предикатных символов называется сигнатурой язы-
ка и определяется той конкретной предметной областью, для описания которой
предназначен язык. Язык логики первого порядка, таким образом, определяется
своей сигнатурой, поэтому говорят об алфавите и языке сигнатуры ? (если необ-
ходимо подчеркнуть зависимость от сигнатуры, ее указывают в верхнем индексе,
например, алфавит A? , язык L? ).
Как правило, для обозначения символов предметных констант, переменных
и функциональных символов принято использовать малые латинские буквы, а
для предикатных символов – большие латинские буквы. Кроме того, все функ-
циональные и предикатные символы делятся на унарные, бинарные, тернарные,
n-арные и т.п. (если символ n-арный, то это значит, что он используется в записи с
n аргументами). Множества n-арных функциональных и предикатных символов
будем обозначать, соответственно, Funcn и Predn .
Множество логических символов состоит из следующие элементов:

• ¬ – символ отрицания (логическое “не”),

• ? – символ конъюнкции (логическое “и”),

• ? – символ дизъюнкции (логическое “или”),

• > – символ импликации (логическое “следствие”),

• ? – квантор существования,

• ? – квантор всеобщности.

Первые четыре из перечисленных символов (символ отрицания, символ конъюнк-
ции, символ дизъюнкции и символ импликации) называются также логическими
связками, оставшиеся квантор существования и квантор всеобщности про-
сто кванторами. Иногда определяют языки логики предикатов первого порядка
с другими логическими связками, либо с меньшим числом связок – сделать так
можно без ущерба для выразительной силы языка, как мы покажем в дальней-
шем.


2.2 Синтаксис языка первого порядка
Язык L? логики предикатов первого порядка с сигнатурой ? определяется как
формальный язык с алфавитом A? , порождаемый следующей грамматикой (в
10 Языки логики предикатов первого порядка


форме Бэкуса-Наура):

< формула > ::= < атомная формула >
| (¬ < формула >)
|(< формула > ? < формула >)
|(< формула > ? < формула >)
|(< формула >>< формула >)
|(? < переменная >< формула >)
|(? < переменная >< формула >),
< атомная формула > ::= < n ? арный пред. символ > (< терм >, ...),
< терм > ::= < константа >
| < переменная >
| < n ? арный функ. символ > (< терм >, ...),

где < константа >, < переменная >, < n ? арный функциональный символ > и
< n ? арный предикатный символ > – произвольные символы из Const, Var,
Funcn и Predn , соответственно.
Элементы L? называются формулами. Согласно приведенному выше опреде-
лению, формулы бывают атомными и составными. Последние, в свою очередь,
составляются из атомных формул с помощью логических символов. Атомная
формула представляет собой предикатный символ с соответствующим количе-
ством аргументов-термов (для n-арного предикатного символа – n термов). На-
конец, терм языка L? это или предметная константа, или выражение, в которое
входит функциональный символ и соответствующее число (n для n-арного сим-
вола) термов. Это можно выразить и с помощью следующего эквивалентного
определения.

Определение 2.1 (i) Множество термов TER(L? ) языка L? определяется
по следующим правилам:

• любой символ предметной переменной или константы является тер-
мом;
• если f ? Funcn , а t1 , . . . , tn ? TER(L? ), то f (t1 , . . . , tn ) ? TER(L? );
• других термов, кроме построенных по приведенным выше правилам,
нет.

(ii) Множество формул L? определяется по следующим правилам:

• если A ? Predn , а t1 , . . . , tn ? TER(L? ), то A(t1 , . . . , tn ) – формула,
называемая в этом случае атомной формулой;
• если P, Q – формулы, то (¬P), (P ? Q), (P ? Q), (P > Q) – формулы;
2.2 Синтаксис языка первого порядка 11


• если P – формула, а x – символ предметной переменной, то ((?x)P),
((?x)P) – формулы;
• других формул, кроме построенных по приведенным выше правилам,
нет.

Пример 2.1 Пусть A1 и B 2 – унарный и бинарный предикатные символы, со-
ответственно, f – бинарный функциональный символ, а c – символ предметной
константы, а все остальные малые латинские буквы – символы предметных
переменных. Тогда цепочки символов c, x, f (c, x), f (x, f (c, f (x, x))) являются
термами, а цепочки символов

A1 (f (c, x)), B 2 (c, f (c, x)), и

(((?x)(A1 (x) ? A2 (y))) > ((?y)(B 2 (c, f (c, c)) ? A1 (x)))
являются формулами.

Упражнения.
1. Докажите, что в условиях предыдущего примера цепочки символов c(f (A1 (x) >
)), (())(c? не являются ни формулами, ни термами.
2. Докажите следующие теоремы об индукции по структуре термов и формул:

Теорема 2.1 (об индукции по структуре термов) Пусть ? такое
подмножество
TER(L? ), что

(i) ? содержит все предметные константы и переменные;

(ii) Если ? содержит t1 , . . . , tn ? TER(L? ), то ? содержит и f (t1 , t2 , . . . , tn ), где f
– произвольный n-арный функциональный символ.

Тогда ? содержит все термы.

стр. 1
(общее количество: 9)

ОГЛАВЛЕНИЕ

След. стр. >>