Математическая логика: история и современное состояние

Математическая логика: изучение формальной логики в математике. Теория моделей, доказательств, множеств и рекурсий. Основы математики и рассуждений.

27 мин чтения

100%

Источник: Mathematical logic — Wikipedia

Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.

Содержание

Введение

Раздел математики

Математическая логика — это изучение формальной логики в рамках математики. Основные подразделы включают теорию моделей, теорию доказательств, теорию множеств и теорию рекурсии (также известную как теория вычислимости). Исследования в области математической логики обычно посвящены математическим свойствам формальных логических систем, таким как их выразительная или дедуктивная сила. Однако она также может включать использование логики для характеристики корректного математического рассуждения или для установления основ математики. С момента своего возникновения математическая логика одновременно вносила вклад в изучение основ математики и была им мотивирована. Это изучение началось в конце XIX века с разработки аксиоматических систем для геометрии, арифметики и анализа. В начале XX века оно было сформировано программой Давида Гильберта по доказательству непротиворечивости фундаментальных теорий. Результаты Курта Гёделя, Герхарда Гентцена и других дали частичное решение этой программы и прояснили вопросы, связанные с доказательством непротиворечивости. Работы в теории множеств показали, что почти вся обычная математика может быть формализована в терминах множеств, хотя существуют теоремы, которые нельзя доказать в общепринятых аксиоматических системах теории множеств. Современные исследования в области основ математики часто сосредоточены на установлении того, какие части математики могут быть формализованы в конкретных формальных системах (как в обратной математике), а не на попытках найти теории, в которых может быть развита вся математика.

История

Математическая логика возникла в середине XIX века как раздел математики, отражая слияние двух традиций: формальной философской логики и математики. Математическая логика, также называемая «логистикой», «символической логикой», «алгеброй логики» и, в последнее время, просто «формальной логикой», – это совокупность логических теорий, разработанных в XIX веке с использованием искусственной нотации и строго дедуктивного метода. До этого логика изучалась посредством риторики, вычислений, с помощью силлогизмов и в рамках философии. Первая половина XX века ознаменовалась взрывом фундаментальных результатов, сопровождавшимся оживлёнными дискуссиями об основаниях математики.

Ранняя история

Теории логики разрабатывались в различных культурах на протяжении истории, включая Китай, Индию, Грецию и исламский мир. Греческие методы, в особенности аристотелевская логика (или логика терминов), представленная в «Органоне», получила широкое распространение и признание в западной науке и математике на протяжении тысячелетий. Стоики, особенно Хрисипп, начали развитие логики предикатов. В Европе XVIII века философские математики, включая Лейбница и Ламберта, предпринимали попытки представить операции формальной логики в символической или алгебраической форме, однако их работы оставались обособленными и малоизвестными.

19 век

В середине девятнадцатого века Джордж Буль, а затем Август Де Морган представили систематическое математическое изложение логики. Их работа, опираясь на труды алгебраистов, таких как Джордж Пикок, расширила традиционную аристотелевскую доктрину логики, создав достаточную основу для изучения основ математики. В 1847 году Ватрослав Бертич независимо от Буля проделал значительную работу по алгебраизации логики. Позже Чарльз Сандерс Пирс, опираясь на работу Буля, разработал логическую систему для отношений и кванторов, которую он опубликовал в ряде статей с 1870 по 1885 год. Готтлоб Фреге представил независимую разработку логики с кванторами в своей "Begriffsschrift", опубликованной в 1879 году – работа, которую обычно считают поворотным моментом в истории логики. Однако труд Фреге оставался малоизвестным, пока Бертран Рассел не начал его популяризировать в начале XX века. Двумерная нотация, разработанная Фреге, так и не получила широкого распространения и не используется в современных текстах. С 1890 по 1905 год Эрнст Шрёдер опубликовал "Vorlesungen über die Algebra der Logik" в трех томах. Эта работа обобщила и расширила труды Буля, Де Моргана и Пирса и являлась исчерпывающим справочником по символической логике, как она понималась в конце XIX века.

Основные теории

Опасения относительно того, что математика не была построена на надлежащем фундаменте, привели к разработке аксиоматических систем для фундаментальных областей математики, таких как арифметика, анализ и геометрия. В логике термин «арифметика» относится к теории натуральных чисел. Джузеппе Пеано опубликовал набор аксиом для арифметики, которые стали известны как аксиомы Пеано, используя вариацию логической системы Буля и Шредера, но добавив кванторы. В то время Пеано не знал о работах Фреге. Примерно в то же время Рихард Дедекинд показал, что натуральные числа однозначно характеризуются своими индукционными свойствами. Дедекинд предложил иную характеристику, которой не хватало формального логического характера аксиом Пеано. Однако работа Дедекинда доказала теоремы, недоступные в системе Пеано, включая единственность множества натуральных чисел (с точностью до изоморфизма) и рекурсивные определения сложения и умножения на основе функции следования и математической индукции. В середине XIX века стали известны недостатки аксиом Евклида для геометрии. Помимо независимости постулата о параллельных прямых, установленной Николаем Лобачевским в 1826 году, математики обнаружили, что некоторые теоремы, принимавшиеся Евклидом за само собой разумеющиеся, на самом деле не доказуемы из его аксиом. Среди них – теорема о том, что прямая содержит как минимум две точки, или что окружности одинакового радиуса, центры которых разделены этим радиусом, должны пересекаться. Гильберт разработал полный набор аксиом для геометрии, опираясь на предыдущие работы Паша. Успех в аксиоматизации геометрии побудил Гильберта к поиску полной аксиоматизации других областей математики, таких как натуральные числа и действительная прямая. Это стало важной областью исследований в первой половине XX века. В XIX веке произошли значительные достижения в теории вещественного анализа, включая теории сходимости функций и рядов Фурье. Математики, такие как Карл Вейерштрасс, начали конструировать функции, расширяющие интуицию, например, непрерывные функции, нигде не дифференцируемые. Предыдущие представления о функции как о правиле вычисления или гладком графике оказались недостаточными. Вейерштрасс начал выступать за арифметизацию анализа, которая стремилась аксиоматизировать анализ, используя свойства натуральных чисел. Современное (ε, δ) определение предела и непрерывных функций было разработано Болцано в 1817 году, но оставалось относительно неизвестным. Коши в 1821 году определил непрерывность в терминах бесконечно малых величин (см. Cours d'Analyse, стр. 34). В 1858 году Дедекинд предложил определение действительных чисел в терминах дедекиндовских разрезов рациональных чисел, определение, которое до сих пор используется в современных учебниках. Георг Кантор разработал фундаментальные концепции теории бесконечных множеств. Его ранние результаты развили теорию кардинальности и доказали, что действительные и натуральные числа имеют разные кардинальности. В течение следующих двадцати лет Кантор разработал теорию трансфинитных чисел в серии публикаций. В 1891 году он опубликовал новое доказательство несчётности действительных чисел, представив диагональный аргумент, и использовал этот метод для доказательства теоремы Кантора о том, что ни одно множество не может иметь ту же кардинальность, что и его множество степеней. Кантор полагал, что любое множество можно хорошо упорядочить, но не смог найти доказательство этого утверждения, оставив его открытой проблемой в 1895 году.

Concerns that mathematics had not been built on a proper foundation led to the development of axiomatic systems for fundamental areas of mathematics such as arithmetic, analysis, and geometry. In logic, the term arithmetic refers to the theory of the natural numbers. Giuseppe Peano published a set of axioms for arithmetic that came to bear his name (Peano axioms), using a variation of the logical system of Boole and Schröder but adding quantifiers. Peano was unaware of Frege's work at the time. Around the same time Richard Dedekind showed that the natural numbers are uniquely characterized by their induction properties. Dedekind proposed a different characterization, which lacked the formal logical character of Peano's axioms. Dedekind's work, however, proved theorems inaccessible in Peano's system, including the uniqueness of the set of natural numbers (up to isomorphism) and the recursive definitions of addition and multiplication from the successor function and mathematical induction. In the mid 19th century, flaws in Euclid's axioms for geometry became known. In addition to the independence of the parallel postulate, established by Nikolai Lobachevsky in 1826, mathematicians discovered that certain theorems taken for granted by Euclid were not in fact provable from his axioms. Among these is the theorem that a line contains at least two points, or that circles of the same radius whose centers are separated by that radius must intersect. Hilbert developed a complete set of axioms for geometry, building on previous work by Pasch. The success in axiomatizing geometry motivated Hilbert to seek complete axiomatizations of other areas of mathematics, such as the natural numbers and the real line. This would prove to be a major area of research in the first half of the 20th century. The 19th century saw great advances in the theory of real analysis, including theories of convergence of functions and Fourier series. Mathematicians such as Karl Weierstrass began to construct functions that stretched intuition, such as nowhere differentiable continuous functions. Previous conceptions of a function as a rule for computation, or a smooth graph, were no longer adequate. Weierstrass began to advocate the arithmetization of analysis, which sought to axiomatize analysis using properties of the natural numbers. The modern (ε, δ) definition of limit and continuous functions was already developed by Bolzano in 1817, but remained relatively unknown. Cauchy in 1821 defined continuity in terms of infinitesimals (see Cours d'Analyse, page 34). In 1858, Dedekind proposed a definition of the real numbers in terms of Dedekind cuts of rational numbers, a definition still employed in contemporary texts. Georg Cantor developed the fundamental concepts of infinite set theory. His early results developed the theory of cardinality and proved that the reals and the natural numbers have different cardinalities. Over the next twenty years, Cantor developed a theory of transfinite numbers in a series of publications. In 1891, he published a new proof of the uncountability of the real numbers that introduced the diagonal argument, and used this method to prove Cantor's theorem that no set can have the same cardinality as its powerset. Cantor believed that every set could be well ordered, but was unable to produce a proof for this result, leaving it as an open problem in 1895.

20 век

В первые десятилетия XX века основными областями исследования были теория множеств и формальная логика. Открытие парадоксов в наивной теории множеств заставило некоторых усомниться в непротиворечивости самой математики и искать доказательства её непротиворечивости. В 1900 году Гильберт сформулировал знаменитый список из 23 проблем, определяющих развитие науки на следующее столетие. Первые две из них касались решения гипотезы континуума и доказательства непротиворечивости элементарной арифметики соответственно, а десятая – разработки метода, позволяющего определить, имеет ли решение многомерное полиномиальное уравнение с целыми коэффициентами. Последующие работы, направленные на решение этих проблем, определили направление развития математической логики, равно как и усилия по решению Entscheidungsproblem, сформулированного Гильбертом в 1928 году. Эта проблема заключалась в поиске процедуры, которая, получив на вход формализованное математическое утверждение, могла бы определить, истинно оно или ложно.

Теория множеств и парадоксы

Эрнст Зермело доказал, что любое множество может быть вполне упорядочено, результат, который Георгу Кантору не удалось получить. Для доказательства Зермело ввел аксиому выбора, что вызвало оживленные дебаты и исследования среди математиков и основоположников теории множеств. Немедленная критика этого метода побудила Зермело опубликовать второе изложение своего результата, напрямую отвечая на критику его доказательства. Эта работа привела к общему принятию аксиомы выбора в математическом сообществе. Скептицизм в отношении аксиомы выбора усилился благодаря недавно обнаруженным парадоксам в наивной теории множеств. Чезаре Бурали Форти первым сформулировал парадокс: парадокс Бурали-Форти показывает, что совокупность всех ординальных чисел не может образовать множество. Вскоре после этого, в 1901 году, Бертран Рассел открыл парадокс Рассела, а Жюль Ришар – парадокс Ришара. Зермело предложил первый набор аксиом для теории множеств. Эти аксиомы, вместе с дополнительной аксиомой заменяемости, предложенной Авраамом Френкелем, теперь называются теорией множеств Цермело-Френкеля (ZF). Аксиомы Зермело включали принцип ограничения размера, чтобы избежать парадокса Рассела. В 1910 году был опубликован первый том «Principia Mathematica» Рассела и Альфреда Норта Уайтхеда. Эта основополагающая работа развивала теорию функций и кардинальности в полностью формализованной системе теории типов, которую Рассел и Уайтхед разработали в попытке избежать парадоксов. «Principia Mathematica» считается одним из самых влиятельных трудов XX века, хотя система теории типов не получила широкого распространения в качестве фундаментальной теории математики. Френкель доказал, что аксиому выбора нельзя вывести из аксиом теории множеств Зермело с уэлементами. Последующие работы Пола Коэна показали, что добавление уэлементов не требуется, и аксиома выбора недоказуема в ZF. Доказательство Коэна разработало метод принуждения, который сейчас является важным инструментом для установления результатов независимости в теории множеств.

Ernst Zermelo gave a proof that every set could be well ordered, a result Georg Cantor had been unable to obtain. To achieve the proof, Zermelo introduced the axiom of choice, which drew heated debate and research among mathematicians and the pioneers of set theory. The immediate criticism of the method led Zermelo to publish a second exposition of his result, directly addressing criticisms of his proof. This paper led to the general acceptance of the axiom of choice in the mathematics community. Skepticism about the axiom of choice was reinforced by recently discovered paradoxes in naive set theory. Cesare Burali Forti was the first to state a paradox: the Burali Forti paradox shows that the collection of all ordinal numbers cannot form a set. Very soon thereafter, Bertrand Russell discovered Russell's paradox in 1901, and Jules Richard discovered Richard's paradox. Zermelo provided the first set of axioms for set theory. These axioms, together with the additional axiom of replacement proposed by Abraham Fraenkel, are now called Zermelo–Fraenkel set theory (ZF). Zermelo's axioms incorporated the principle of limitation of size to avoid Russell's paradox. In 1910, the first volume of Principia Mathematica by Russell and Alfred North Whitehead was published. This seminal work developed the theory of functions and cardinality in a completely formal framework of type theory, which Russell and Whitehead developed in an effort to avoid the paradoxes. Principia Mathematica is considered one of the most influential works of the 20th century, although the framework of type theory did not prove popular as a foundational theory for mathematics. Fraenkel proved that the axiom of choice cannot be proved from the axioms of Zermelo's set theory with urelements. Later work by Paul Cohen showed that the addition of urelements is not needed, and the axiom of choice is unprovable in ZF. Cohen's proof developed the method of forcing, which is now an important tool for establishing independence results in set theory.

Символическая логика

Леопольд Лёвенхайм и Торальф Сколем получили теорему Лёвенхайма — Сколема, которая утверждает, что логика первого порядка не способна контролировать кардинальность бесконечных структур. Сколем осознал, что эта теорема применима к формализациям теории множеств в логике первого порядка, и что из неё следует, что любая такая формализация имеет счётную модель. Этот контринтуитивный факт стал известен как парадокс Сколема. В своей докторской диссертации Курт Гёдель доказал теорему о полноте, которая устанавливает соответствие между синтаксисом и семантикой в логике первого порядка. Гёдель использовал теорему о полноте для доказательства теоремы о компактности, демонстрируя финитарную природу логического следования в логике первого порядка. Эти результаты способствовали утверждению логики первого порядка в качестве доминирующей логики, используемой математиками. В 1931 году Гёдель опубликовал работу «О формально неразрешимых предложениях Principia Mathematica и связанных с ними систем», в которой доказал неполноту (в ином смысле этого слова) всех достаточно сильных и эффективных теорий первого порядка. Этот результат, известный как теорема о неполноте Гёделя, устанавливает серьёзные ограничения на аксиоматические основания математики, нанося серьёзный удар по программе Гильберта. Он показал невозможность получения доказательства непротиворечивости арифметики внутри какой-либо формальной теории арифметики. Однако Гильберт некоторое время не признавал значимости теоремы о неполноте. Теорема Гёделя показывает, что доказательство непротиворечивости любой достаточно сильной и эффективной аксиоматической системы не может быть получено в самой системе, если она непротиворечива, и не может быть получено ни в какой более слабой системе. Это оставляет открытой возможность доказательств непротиворечивости, которые не могут быть формализованы в рамках рассматриваемой системы. Гентцен доказал непротиворечивость арифметики, используя финитистическую систему вместе с принципом трансфинитной индукции. Результат Гентцена ввёл понятия устранения высечений и доказательно-теоретических ординалов, которые стали ключевыми инструментами в теории доказательств. Гёдель предложил другое доказательство непротиворечивости, которое сводит непротиворечивость классической арифметики к непротиворечивости интуиционистской арифметики высших типов. Первый учебник по символической логике для широкой публики был написан Льюисом Кэрроллом, автором «Приключений Алисы в Стране чудес», в 1896 году.

Leopold Löwenheim and Thoralf Skolem obtained the Löwenheim–Skolem theorem, which says that first order logic cannot control the cardinalities of infinite structures. Skolem realized that this theorem would apply to first order formalizations of set theory, and that it implies any such formalization has a countable model. This counterintuitive fact became known as Skolem's paradox. In his doctoral thesis, Kurt Gödel proved the completeness theorem, which establishes a correspondence between syntax and semantics in first order logic. Gödel used the completeness theorem to prove the compactness theorem, demonstrating the finitary nature of first order logical consequence. These results helped establish first order logic as the dominant logic used by mathematicians. In 1931, Gödel published On Formally Undecidable Propositions of Principia Mathematica and Related Systems, which proved the incompleteness (in a different meaning of the word) of all sufficiently strong, effective first order theories. This result, known as Gödel's incompleteness theorem, establishes severe limitations on axiomatic foundations for mathematics, striking a strong blow to Hilbert's program. It showed the impossibility of providing a consistency proof of arithmetic within any formal theory of arithmetic. Hilbert, however, did not acknowledge the importance of the incompleteness theorem for some time. Gödel's theorem shows that a consistency proof of any sufficiently strong, effective axiom system cannot be obtained in the system itself, if the system is consistent, nor in any weaker system. This leaves open the possibility of consistency proofs that cannot be formalized within the system they consider. Gentzen proved the consistency of arithmetic using a finitistic system together with a principle of transfinite induction. Gentzen's result introduced the ideas of cut elimination and proof theoretic ordinals, which became key tools in proof theory. Gödel gave a different consistency proof, which reduces the consistency of classical arithmetic to that of intuitionistic arithmetic in higher types. The first textbook on symbolic logic for the layman was written by Lewis Carroll, author of Alice's Adventures in Wonderland, in 1896.

Начало других отраслей

Альфред Тарски разработал основы теории моделей. Начиная с 1935 года, группа выдающихся математиков сотрудничала под псевдонимом Николя Бурбаки для публикации «Éléments de mathématique» — серии энциклопедических математических текстов. Эти тексты, написанные в строгом и аксиоматическом стиле, подчеркивали строгость изложения и основывались на теории множеств. Терминология, введенная этими текстами, такая как слова биекция, инъекция и сюржекция, а также теоретико-множественные основы, использованные в текстах, получили широкое распространение в математике. Изучение вычислимости стало известно как теория рекурсии или теория вычислимости, поскольку ранние формализации Гёделя и Клини опирались на рекурсивные определения функций. Когда было показано, что эти определения эквивалентны формализации Тьюринга с использованием машин Тьюринга, стало ясно, что было открыто новое понятие — вычислимая функция, и что это определение достаточно устойчиво, чтобы допускать множество независимых характеристик. В своей работе над теоремами о неполноте в 1931 году Гёделю не хватало строгого понятия об эффективной формальной системе; он сразу же понял, что новые определения вычислимости могут быть использованы для этой цели, что позволило ему сформулировать теоремы о неполноте в более общей форме, чем это было подразумевалось в оригинальной статье. Многочисленные результаты в теории рекурсии были получены в 1940-х годах Стивеном Коулом Клини и Эмилем Леоном Постом. Клини ввёл понятия относительной вычислимости, предвосхищенные Тьюрингом, и арифметической иерархии. Позднее Клини обобщил теорию рекурсии на функционалы высшего порядка. Клини и Георг Крайзель изучали формальные версии интуиционистской математики, особенно в контексте теории доказательств.

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

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

Логика первого порядка

Логика первого порядка — это особая формальная система логики. Её синтаксис включает только конечные выражения и корректно сформированные формулы, а её семантика характеризуется ограничением всех кванторов фиксированной областью значений. Ранние результаты формальной логики установили ограничения логики первого порядка. Теорема Лёвенхайма — Сколема (1919) показала, что если множество предложений в счетном языке первого порядка имеет бесконечную модель, то у него есть по крайней мере одна модель каждой бесконечной кардинальности. Это показывает, что невозможно с помощью множества аксиом первого порядка однозначно определить натуральные числа, действительные числа или любую другую бесконечную структуру с точностью до изоморфизма. Поскольку целью ранних фундаментальных исследований было создание аксиоматических теорий для всех разделов математики, это ограничение оказалось особенно существенным. Теорема полноты Гёделя установила эквивалентность семантических и синтаксических определений логического следования в логике первого порядка. Она показывает, что если конкретное предложение истинно во всех моделях, удовлетворяющих конкретному набору аксиом, то должно существовать конечное доказательство этого предложения из этих аксиом. Теорема компактности впервые появилась как лемма в доказательстве теоремы полноты Гёделя, и потребовались годы, прежде чем логики осознали её значимость и начали регулярно применять её. Она утверждает, что множество предложений имеет модель тогда и только тогда, когда каждое его конечное подмножество имеет модель, или, иными словами, что противоречивое множество формул должно иметь противоречивое конечное подмножество. Теоремы полноты и компактности позволяют проводить глубокий анализ логического следования в логике первого порядка и развивать теорию моделей, и они являются ключевой причиной популярности логики первого порядка в математике. Теоремы о неполноте Гёделя устанавливают дополнительные ограничения на аксиоматизацию первого порядка. Первая теорема о неполноте утверждает, что для любой непротиворечивой, эффективно заданной (определённой ниже) логической системы, способной интерпретировать арифметику, существует утверждение, которое истинно (в том смысле, что оно выполняется для натуральных чисел), но не доказуемо в этой логической системе (и которое, возможно, не выполняется в некоторых нестандартных моделях арифметики, которые могут быть непротиворечивы с этой логической системой). Например, в любой логической системе, способной выразить аксиомы Пеано, предложение Гёделя истинно для натуральных чисел, но не может быть доказано. Логическая система считается эффективно заданной, если можно определить, для любой формулы на языке этой системы, является ли она аксиомой, а система, способная выразить аксиомы Пеано, называется «достаточно сильной». Применительно к логике первого порядка, первая теорема о неполноте подразумевает, что любая достаточно сильная, непротиворечивая, эффективная теория первого порядка имеет модели, которые не элементарно эквивалентны, что является более сильным ограничением, чем то, которое установлено теоремой Лёвенхайма — Сколема. Вторая теорема о неполноте утверждает, что никакая достаточно сильная, непротиворечивая, эффективная система аксиом для арифметики не может доказать собственную непротиворечивость, что было истолковано как доказательство недостижимости программы Гильберта.

First order logic is a particular formal system of logic. Its syntax involves only finite expressions as well formed formulas, while its semantics are characterized by the limitation of all quantifiers to a fixed domain of discourse. Early results from formal logic established limitations of first order logic. The Löwenheim–Skolem theorem (1919) showed that if a set of sentences in a countable first order language has an infinite model then it has at least one model of each infinite cardinality. This shows that it is impossible for a set of first order axioms to characterize the natural numbers, the real numbers, or any other infinite structure up to isomorphism. As the goal of early foundational studies was to produce axiomatic theories for all parts of mathematics, this limitation was particularly stark. Gödel's completeness theorem established the equivalence between semantic and syntactic definitions of logical consequence in first order logic. It shows that if a particular sentence is true in every model that satisfies a particular set of axioms, then there must be a finite deduction of the sentence from the axioms. The compactness theorem first appeared as a lemma in Gödel's proof of the completeness theorem, and it took many years before logicians grasped its significance and began to apply it routinely. It says that a set of sentences has a model if and only if every finite subset has a model, or in other words that an inconsistent set of formulas must have a finite inconsistent subset. The completeness and compactness theorems allow for sophisticated analysis of logical consequence in first order logic and the development of model theory, and they are a key reason for the prominence of first order logic in mathematics. Gödel's incompleteness theorems establish additional limits on first order axiomatizations. The first incompleteness theorem states that for any consistent, effectively given (defined below) logical system that is capable of interpreting arithmetic, there exists a statement that is true (in the sense that it holds for the natural numbers) but not provable within that logical system (and which indeed may fail in some non standard models of arithmetic which may be consistent with the logical system). For example, in every logical system capable of expressing the Peano axioms, the Gödel sentence holds for the natural numbers but cannot be proved. Here a logical system is said to be effectively given if it is possible to decide, given any formula in the language of the system, whether the formula is an axiom, and one which can express the Peano axioms is called "sufficiently strong." When applied to first order logic, the first incompleteness theorem implies that any sufficiently strong, consistent, effective first order theory has models that are not elementarily equivalent, a stronger limitation than the one established by the Löwenheim–Skolem theorem. The second incompleteness theorem states that no sufficiently strong, consistent, effective axiom system for arithmetic can prove its own consistency, which has been interpreted to show that Hilbert's program cannot be reached.

Другие классические логики

Кроме логики первого порядка изучается множество других логик. К ним относятся бесконечноточные логики, которые позволяют формулам содержать бесконечное количество информации, и логики высшего порядка, которые включают часть теории множеств непосредственно в свою семантику. Наиболее изученной бесконечноточной логикой является логика, в которой кванторы могут быть вложены только на конечную глубину, как и в логике первого порядка, но формулы могут содержать конечные или счетно бесконечные конъюнкции и дизъюнкции. Таким образом, например, можно утверждать, что объект является целым числом, используя формулу вида…

Логики высшего порядка позволяют квантифицировать не только элементы области определения, но и подмножества этой области, множества таких подмножеств и другие объекты более высоких типов. Семантика определяется таким образом, что кванторы, вместо того чтобы иметь отдельную область для каждого квантора более высокого типа, охватывают все объекты соответствующего типа. Логики, изучавшиеся до развития логики первого порядка, например, логика Фреге, имели схожие теоретико-множественные аспекты. Хотя логики высшего порядка более выразительны, позволяя полные аксиоматизации структур, таких как натуральные числа, они не удовлетворяют аналогам теорем полноты и компактности из логики первого порядка и, следовательно, менее поддаются теоретико-доказательному анализу. Другой тип логик – это логики, допускающие индуктивные определения, подобные тем, что используются для примитивно рекурсивных функций. Можно формально определить расширение логики первого порядка – понятие, которое охватывает все логики, рассмотренные в этом разделе, поскольку они в определенных фундаментальных аспектах ведут себя как логика первого порядка, но не охватывает все логики в целом, например, интуиционистскую, модальную или нечеткую логику. Теорема Линдстрема утверждает, что единственным расширением логики первого порядка, удовлетворяющим одновременно теореме компактности и теореме о понижении Ловенхейма — Сколема, является сама логика первого порядка.

Неклассическая и модальная логика

Модальные логики включают дополнительные модальные операторы, такие как оператор, утверждающий, что конкретная формула истинна не только, но и необходимо истинна. Хотя модальная логика нечасто используется для аксиоматизации математики, она применялась для изучения свойств доказуемости логики первого порядка и теоретического принуждения в теории множеств. Интуиционистская логика была разработана Хейтингом для изучения программы интуиционизма Брауэра, в рамках которой сам Брауэр избегал формализации. Интуиционистская логика специально не включает закон исключённого третьего, утверждающий, что каждое высказывание либо истинно, либо его отрицание истинно. Работа Клини над теорией доказательств интуиционистской логики показала, что из интуиционистских доказательств можно извлечь конструктивную информацию. Например, любая доказуемо тотальная функция в интуиционистской арифметике вычислима; это неверно для классических теорий арифметики, таких как арифметика Пеано.

Алгебраическая логика

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

Теория множеств

Теория множеств – это изучение множеств, которые представляют собой абстрактные коллекции объектов. Многие из основных понятий, таких как ординальные и кардинальные числа, были разработаны Кантором неформально до того, как были разработаны формальные аксиоматизации теории множеств. Первая такая аксиоматизация, предложенная Зермело, была несколько расширена и стала теорией множеств Зермело–Франкеля (ZF), которая в настоящее время является наиболее широко используемой основополагающей теорией для математики. Были предложены и другие формализации теории множеств, включая теорию множеств фон Неймана – Бернайса – Гёделя (NBG), теорию множеств Морса – Келли (MK) и «Новые основания» (NF). Из них ZF, NBG и MK схожи в описании кумулятивной иерархии множеств. «Новые основания» используют иной подход: они допускают объекты, такие как множество всех множеств, но при этом вводят ограничения на аксиомы существования множеств. Система теории множеств Крипке–Платека тесно связана с обобщенной теорией рекурсии. Двумя известными утверждениями в теории множеств являются аксиома выбора и гипотеза континуума. Аксиома выбора, впервые сформулированная Зермело, была доказана Френкелем независимой от ZF, но впоследствии получила широкое признание среди математиков. Она утверждает, что для любой коллекции непустых множеств существует единственное множество C, содержащее ровно один элемент из каждого множества в этой коллекции. Говорят, что множество C «выбирает» один элемент из каждого множества в коллекции. Хотя возможность такого выбора может показаться очевидной, поскольку каждое множество в коллекции непусто, отсутствие общего, конкретного правила, по которому можно сделать этот выбор, делает аксиому неконструктивной. Стефан Банах и Альфред Тарский показали, что аксиому выбора можно использовать для разложения твердого шара на конечное число частей, которые затем можно переставить без масштабирования, чтобы получить два твердых шара исходного размера. Эта теорема, известная как парадокс Банаха–Тарского, является одним из многих контринтуитивных следствий аксиомы выбора. Гипотеза континуума, впервые предложенная Кантором как предположение, была включена Дэвидом Гильбертом в список его 23 проблем в 1900 году. Гёдель показал, что гипотезу континуума нельзя опровергнуть, исходя из аксиом теории множеств Зермело–Франкеля (с аксиомой выбора или без нее), разработав конструктивную вселенную теории множеств, в которой гипотеза континуума должна выполняться. В 1963 году Пол Коэн доказал, что гипотезу континуума нельзя доказать, исходя из аксиом теории множеств Зермело–Франкеля. Однако этот результат независимости не разрешил полностью вопрос Гильберта, поскольку возможно, что новые аксиомы теории множеств могут разрешить эту гипотезу. Недавние работы в этом направлении проводились У. Хью Вудином, хотя их значимость пока неясна. Современные исследования в теории множеств включают изучение больших кардиналов и детерминированности. Большие кардиналы – это кардинальные числа, обладающие особыми свойствами, настолько сильными, что существование таких кардиналов нельзя доказать в ZFC. Существование наименьшего большого кардинала, обычно изучаемого, недоступного кардинала, уже подразумевает непротиворечивость ZFC. Несмотря на то, что большие кардиналы имеют чрезвычайно высокую кардинальность, их существование имеет множество последствий для структуры вещественной прямой. Детерминированность относится к возможному существованию выигрышных стратегий для определенных двухместных игр (игры называются детерминированными). Существование этих стратегий подразумевает структурные свойства вещественной прямой и других польских пространств.

Set theory is the study of sets, which are abstract collections of objects. Many of the basic notions, such as ordinal and cardinal numbers, were developed informally by Cantor before formal axiomatizations of set theory were developed. The first such axiomatization, due to Zermelo, was extended slightly to become Zermelo–Fraenkel set theory (ZF), which is now the most widely used foundational theory for mathematics. Other formalizations of set theory have been proposed, including von Neumann–Bernays–Gödel set theory (NBG), Morse–Kelley set theory (MK), and New Foundations (NF). Of these, ZF, NBG, and MK are similar in describing a cumulative hierarchy of sets. New Foundations takes a different approach; it allows objects such as the set of all sets at the cost of restrictions on its set existence axioms. The system of Kripke–Platek set theory is closely related to generalized recursion theory. Two famous statements in set theory are the axiom of choice and the continuum hypothesis. The axiom of choice, first stated by Zermelo, was proved independent of ZF by Fraenkel, but has come to be widely accepted by mathematicians. It states that given a collection of nonempty sets there is a single set C that contains exactly one element from each set in the collection. The set C is said to "choose" one element from each set in the collection. While the ability to make such a choice is considered obvious by some, since each set in the collection is nonempty, the lack of a general, concrete rule by which the choice can be made renders the axiom nonconstructive. Stefan Banach and Alfred Tarski showed that the axiom of choice can be used to decompose a solid ball into a finite number of pieces which can then be rearranged, with no scaling, to make two solid balls of the original size. This theorem, known as the Banach–Tarski paradox, is one of many counterintuitive results of the axiom of choice. The continuum hypothesis, first proposed as a conjecture by Cantor, was listed by David Hilbert as one of his 23 problems in 1900. Gödel showed that the continuum hypothesis cannot be disproven from the axioms of Zermelo–Fraenkel set theory (with or without the axiom of choice), by developing the constructible universe of set theory in which the continuum hypothesis must hold. In 1963, Paul Cohen showed that the continuum hypothesis cannot be proven from the axioms of Zermelo–Fraenkel set theory. This independence result did not completely settle Hilbert's question, however, as it is possible that new axioms for set theory could resolve the hypothesis. Recent work along these lines has been conducted by W. Hugh Woodin, although its importance is not yet clear. Contemporary research in set theory includes the study of large cardinals and determinacy. Large cardinals are cardinal numbers with particular properties so strong that the existence of such cardinals cannot be proved in ZFC. The existence of the smallest large cardinal typically studied, an inaccessible cardinal, already implies the consistency of ZFC. Despite the fact that large cardinals have extremely high cardinality, their existence has many ramifications for the structure of the real line. Determinacy refers to the possible existence of winning strategies for certain two player games (the games are said to be determined). The existence of these strategies implies structural properties of the real line and other Polish spaces.

Теория моделей

Теория моделей изучает модели различных формальных теорий. Здесь под теорией понимается множество формул в конкретной формальной логике и сигнатуре, а модель – это структура, дающая конкретную интерпретацию теории. Теория моделей тесно связана с универсальной алгеброй и алгебраической геометрией, хотя методы теории моделей больше ориентированы на логические аспекты, чем эти области. Множество всех моделей конкретной теории называется элементарным классом; классическая теория моделей стремится определить свойства моделей в заданном элементарном классе или установить, образуют ли определенные классы структур элементарные классы. Метод устранения кванторов может быть использован для доказательства того, что определяемые множества в конкретных теориях не могут быть слишком сложными. Тарский установил устранение кванторов для вещественно замкнутых полей, результат, который также показывает, что теория поля вещественных чисел является разрешимой. Он также отметил, что его методы в равной степени применимы к алгебраически замкнутым полям произвольной характеристики. Современное направление, развивающееся из этого, посвящено o-минимальным структурам. Теорема категоричности Морли, доказанная Майклом Д. Морли, утверждает, что если теория первого порядка на счетном языке категорична в некоторой несчётной кардинальности, то есть все модели этой кардинальности изоморфны, то она категорична во всех несчётных кардинальностях. Непосредственным следствием гипотезы континуума является то, что полная теория с числом неизоморфных счётных моделей, меньшим континуума, может иметь только счётное число моделей. Гипотеза Вотта, названная в честь Роберта Лоусона Вотта, утверждает, что это верно даже независимо от гипотезы континуума. Многие частные случаи этой гипотезы были установлены.

Теория рекурсии

Теория рекурсии, также называемая теорией вычислимости, изучает свойства вычислимых функций и степеней Тьюринга, которые разделяют невычислимые функции на множества с одинаковой степенью невычислимости. Теория рекурсии также включает изучение обобщенной вычислимости и определимости. Теория рекурсии берет начало в работах Розы Петера, Алонзо Черча и Алана Тьюринга 1930-х годов, которые были значительно расширены Клини и Постом в 1940-х годах. Классическая теория рекурсии фокусируется на вычислимости функций от натуральных чисел к натуральным числам. Фундаментальные результаты устанавливают устойчивый, канонический класс вычислимых функций с многочисленными независимыми и эквивалентными характеристиками, использующими машины Тьюринга, λ-исчисление и другие системы. Более сложные результаты касаются структуры степеней Тьюринга и решетки рекурсивно перечислимых множеств. Обобщенная теория рекурсии распространяет идеи теории рекурсии на вычисления, которые не обязательно являются конечными. Она включает изучение вычислимости высших типов, а также такие области, как гиперарифметическая теория и α-рекурсия. Современные исследования в теории рекурсии включают изучение приложений, таких как алгоритмическая случайность, теория вычислимых моделей и обратная математика, а также новые результаты в самой теории рекурсии.

Алгоритмически неразрешимые проблемы

Важным подполем теории рекурсии является изучение алгоритмической неразрешимости; задача о решении или функциональная задача считается алгоритмически неразрешимой, если не существует вычислимого алгоритма, который бы возвращал правильный ответ для всех допустимых входных данных. Первые результаты о неразрешимости, полученные независимо друг от друга Церкью и Тьюрингом в 1936 году, показали, что проблема решения (Entscheidungsproblem) алгоритмически неразрешима. Тьюринг доказал это, установив неразрешимость проблемы останова, результат, имеющий далеко идущие последствия как для теории рекурсии, так и для информатики. Существует множество известных примеров неразрешимых задач из обычной математики. Алгоритмическая неразрешимость задачи о слове для групп была доказана Петром Новиковым в 1955 году и независимо от него У. Буном в 1959 году. Другой хорошо известный пример – задача о занятом бобре, разработанная Тибором Радо в 1962 году. Десятая проблема Гильберта заключалась в поиске алгоритма для определения, имеет ли многомерное полиномиальное уравнение с целыми коэффициентами решение в целых числах. Частичный прогресс был достигнут Джулией Робинсон, Мартином Дэвисом и Хилари Путнам. Алгоритмическая неразрешимость этой проблемы была доказана Юрием Матьясевичем в 1970 году.

Теория доказательств и конструктивная математика

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

Приложения

Математическая логика успешно применяется не только к математике и ее основам (Г. Фреге, Б. Рассел, Д. Гильберт, П. Бернейс, Х. Шолц, Р. Карнап, С. Лесневский, Т. Сколем), но и к физике (Р. Карнап, А. Диттрих, Б. Рассел, С. Э. Шеннон, А. Н. Уайтхед, Х. Рейхенбах, П. Февриер), к биологии (Дж. Х. Вудджер, А. Тарский), к психологии (Ф. Б. Фитч, К. Г. Хемпель), к юриспруденции и морали (К. Менгер, У. Клюг, П. Оппенгейм), к экономике (Дж. Нейман, О. Моргенштерн), к практическим вопросам (Э. С. Беркли, Э. Штамм) и даже к метафизике (Дж. [Ян] Саламуха, Х. Шолц, Дж. М. Бохенский). Ее применение в истории логики оказалось чрезвычайно плодотворным (Я. Лукасевич, Х. Шолц, Б. Мейтс, А. Беккер, Э. Муди, Дж. Саламуха, К. Дюрр, З. Йордан, П. Бёнер, Дж. М. Бохенский, С. [Станислав] Т. Шайер, Д. Ингаллс). Также применялась к теологии (Ф. Древновский, Дж. Саламуха, И. Томас).

Связи с информатикой

Изучение теории вычислимости в информатике тесно связано с изучением вычислимости в математической логике. Однако существует разница в акцентах. Специалисты в области информатики часто сосредотачиваются на конкретных языках программирования и практически реализуемой вычислимости, в то время как исследователи в математической логике чаще рассматривают вычислимость как теоретическое понятие и невычислимость. Теория семантики языков программирования связана с теорией моделей, как и верификация программ (в частности, проверка моделей). Соответствие Карри — Ховарда между доказательствами и программами относится к теории доказательств, особенно к интуиционистской логике. Формальные исчисления, такие как лямбда-исчисление и комбинаторная логика, теперь изучаются как идеализированные языки программирования. Информатика также вносит вклад в математику, разрабатывая методы автоматической проверки или даже поиска доказательств, такие как автоматическое доказательство теорем и логическое программирование. Теория описательной сложности связывает логики с вычислительной сложностью. Первым значительным результатом в этой области стала теорема Фагина (1974), установившая, что NP — это точно множество языков, выразимых предложениями экзистенциальной логики второго порядка.

Основы математики

В XIX веке математики осознали наличие логических пробелов и противоречий в своей области. Было показано, что аксиомы Евклида для геометрии, которые на протяжении веков преподавали как пример аксиоматического метода, были неполными. Использование бесконечно малых и само определение функции подверглись критике в анализе, поскольку были обнаружены патологические примеры, такие как нигде недифференцируемая непрерывная функция Вейерштрасса. Исследование Кантором произвольных бесконечных множеств также вызвало критику. Леопольд Кронекер, как известно, заявил: «Бог создал целые числа; все остальное – дело рук человеческих», поддерживая возвращение к изучению конечных, конкретных объектов в математике. Хотя аргумент Кронекера был подхвачен конструктивистами в XX веке, математическое сообщество в целом отвергло их. Давид Гильберт выступал в защиту изучения бесконечного, говоря: «Никто не изгонит нас из Рая, который создал Кантор». Математики начали искать системы аксиом, которые можно было бы использовать для формализации больших частей математики. Помимо устранения неоднозначности из ранее наивных терминов, таких как функция, надеялись, что эта аксиоматизация позволит доказать непротиворечивость. В XIX веке основным методом доказательства непротиворечивости набора аксиом было приведение модели для него. Так, например, непротиворечивость неевклидовой геометрии можно доказать, определив точку как точку на фиксированной сфере, а прямую – как большую окружность на сфере. Полученная структура, модель эллиптической геометрии, удовлетворяет аксиомам планиметрии, за исключением постулата о параллельных прямых. С развитием формальной логики Гильберт задался вопросом, возможно ли доказать непротиворечивость системы аксиом, анализируя структуру возможных доказательств в системе и показывая посредством этого анализа, что невозможно доказать противоречие. Эта идея привела к изучению теории доказательств. Более того, Гильберт предложил, чтобы анализ был полностью конкретным, используя термин «финитарный» для обозначения методов, которые он допускал бы, но не определяя их точно. Этот проект, известный как программа Гильберта, был серьезно подорван теоремами о неполноте Гёделя, которые показали, что непротиворечивость формальных теорий арифметики нельзя установить, используя методы, формализуемые в этих теориях. Гентцен показал, что возможно построить доказательство непротиворечивости арифметики в финитарной системе, дополненной аксиомами трансфинитной индукции, и разработанные им методы стали основополагающими в теории доказательств. Другая линия в истории основ математики связана с неклассическими логиками и конструктивной математикой. Изучение конструктивной математики включает в себя множество различных программ с различными определениями конструктивности. В наиболее широком смысле доказательства в теории множеств ZF, которые не используют аксиому выбора, многими математиками считаются конструктивными. Более ограниченные версии конструктивизма ограничиваются натуральными числами, арифметическими функциями и множествами натуральных чисел (которые можно использовать для представления действительных чисел, облегчая изучение математического анализа). Общая идея заключается в том, что конкретный способ вычисления значений функции должен быть известен, прежде чем можно будет сказать, что сама функция существует. В начале XX века Люциен Эгбертус Ян Брауэр основал интуиционизм как часть философии математики. Эта философия, поначалу плохо понятая, утверждала, что для того, чтобы математическое утверждение было истинным для математика, этот человек должен быть способен интуитивно постичь это утверждение, не только верить в его истинность, но и понимать причину его истинности. Следствием этого определения истины было отвержение закона исключенного третьего, поскольку есть утверждения, которые, по мнению Брауэра, нельзя было считать истинными, а их отрицания также нельзя было считать истинными. Философия Брауэра оказала влияние и стала причиной ожесточенных споров среди видных математиков. Позже Клини и Крайзель изучали формализованные версии интуиционистской логики (Брауэр отвергал формализацию и представлял свою работу на неформализованном естественном языке). С появлением BHK-интерпретации и моделей Крипке интуиционизм стало легче согласовать с классической математикой.

In the 19th century, mathematicians became aware of logical gaps and inconsistencies in their field. It was shown that Euclid's axioms for geometry, which had been taught for centuries as an example of the axiomatic method, were incomplete. The use of infinitesimals, and the very definition of function, came into question in analysis, as pathological examples such as Weierstrass' nowhere differentiable continuous function were discovered. Cantor's study of arbitrary infinite sets also drew criticism. Leopold Kronecker famously stated "God made the integers; all else is the work of man," endorsing a return to the study of finite, concrete objects in mathematics. Although Kronecker's argument was carried forward by constructivists in the 20th century, the mathematical community as a whole rejected them. David Hilbert argued in favor of the study of the infinite, saying "No one shall expel us from the Paradise that Cantor has created." Mathematicians began to search for axiom systems that could be used to formalize large parts of mathematics. In addition to removing ambiguity from previously naive terms such as function, it was hoped that this axiomatization would allow for consistency proofs. In the 19th century, the main method of proving the consistency of a set of axioms was to provide a model for it. Thus, for example, non Euclidean geometry can be proved consistent by defining point to mean a point on a fixed sphere and line to mean a great circle on the sphere. The resulting structure, a model of elliptic geometry, satisfies the axioms of plane geometry except the parallel postulate. With the development of formal logic, Hilbert asked whether it would be possible to prove that an axiom system is consistent by analyzing the structure of possible proofs in the system, and showing through this analysis that it is impossible to prove a contradiction. This idea led to the study of proof theory. Moreover, Hilbert proposed that the analysis should be entirely concrete, using the term finitary to refer to the methods he would allow but not precisely defining them. This project, known as Hilbert's program, was seriously affected by Gödel's incompleteness theorems, which show that the consistency of formal theories of arithmetic cannot be established using methods formalizable in those theories. Gentzen showed that it is possible to produce a proof of the consistency of arithmetic in a finitary system augmented with axioms of transfinite induction, and the techniques he developed to do so were seminal in proof theory. A second thread in the history of foundations of mathematics involves nonclassical logics and constructive mathematics. The study of constructive mathematics includes many different programs with various definitions of constructive. At the most accommodating end, proofs in ZF set theory that do not use the axiom of choice are called constructive by many mathematicians. More limited versions of constructivism limit themselves to natural numbers, number theoretic functions, and sets of natural numbers (which can be used to represent real numbers, facilitating the study of mathematical analysis). A common idea is that a concrete means of computing the values of the function must be known before the function itself can be said to exist. In the early 20th century, Luitzen Egbertus Jan Brouwer founded intuitionism as a part of philosophy of mathematics This philosophy, poorly understood at first, stated that in order for a mathematical statement to be true to a mathematician, that person must be able to intuit the statement, to not only believe its truth but understand the reason for its truth. A consequence of this definition of truth was the rejection of the law of the excluded middle, for there are statements that, according to Brouwer, could not be claimed to be true while their negations also could not be claimed true. Brouwer's philosophy was influential, and the cause of bitter disputes among prominent mathematicians. Later, Kleene and Kreisel would study formalized versions of intuitionistic logic (Brouwer rejected formalization, and presented his work in unformalized natural language). With the advent of the BHK interpretation and Kripke models, intuitionism became easier to reconcile with classical mathematics.

Тексты для студентов

Шон Хедман, Первый курс по логике: введение в теорию моделей, теорию доказательств, вычислимость и сложность, Oxford University Press, 2004, Охватывает логики в тесной связи с теорией вычислимости и теорией сложности.

Тексты выпускников

Клин, Стивен Коул. (1952), Введение в метаматематику. Нью-Йорк: Ван Ностранд. (Иши Пресс: переиздание 2009 года). Клин, Стивен Коул. (1967), Математическая логика. Джон Уайли. Переиздание Dover, 2002.