2 Introduction
Логика, грубо говоря, это наука о том, как выражать понятия и ситуации и правильно рассуждать о них. Математическая логика в основном занимается выражениями в формальных языках, тем, как приписывать значения формальным выражениям и как рассуждать с помощью формальных выражений, используя правила вывода. Математическая логика также изучает алгоритмические вопросы, включая определимость (definability), вычислимость (computability) и сложность (complexity). Кроме того, математическая логика является ключевым инструментом в изучении оснований математики.
Логика имеет множество приложений, особенно в математике и информатике. Современное развитие математической логики было мотивировано желанием установить логические основания для математики.1 С этой точки зрения, математическая логика — это раздел математики, который пытается понять и обосновать все математические рассуждения. Благодаря теоремам о корректности и полноте (Soundness and Completeness Theorems) для логики первого порядка и развитию теории множеств, математическая логика добилась огромного успеха в этом начинании и, через теорию множеств первого порядка, смогла заложить основания для всей математики. С другой стороны, теория вычислимости и теоремы Гёделя о неполноте выявили важные ограничения на использование математической логики и любых формальных систем для доказательства математических истин.
Современная формальная теория вычислимости во многом возникла из теории машин Тьюринга.[^2] Машины Тьюринга — это идеализированная модель вычислений; известный тезис Чёрча-Тьюринга (Church-Turing thesis) утверждает, что машины Тьюринга определяют очень общее и устойчивое понятие вычисления, которое соответствует интуитивному пониманию вычислений. Первоначальной мотивацией для определения машин Тьюринга было доказательство неразрешимости (undecidability) (невычислимости (noncomputability)) математических истин о целых числах. Тьюринг достиг этого, доказав неразрешимость проблемы остановки. Последующие разработки в теории информатики исследовали более ограниченные понятия вычислений, начиная от машин Тьюринга с ограниченным временем, булевых схем и заканчивая более спекулятивными перспективами квантовых вычислений, и это лишь некоторые примеры. Таким образом, теория информатики является важной частью математической логики. С тем же успехом можно сказать и обратное: математическая логика (особенно, но не только, её дискретные или конечные аспекты) является важной частью теоретической информатики.
Действительно, математическая логика имеет множество приложений в теоретической — и не только теоретической — информатике, включая теорию баз данных, верификацию аппаратного и программного обеспечения, а также компьютерное доказательство теорем. Применения компьютерного доказательства теорем варьируются от доказательства теорем о простых свойствах (например, корректности программного обеспечения с помощью SMT-решателей) до доказательства сложных математических теорем (например, с использованием систем компьютерного доказательства, таких как Mizar, Isabelle, MetaMath, Coq, Lean и др.).
При таком разнообразии приложений существует и множество формальных систем логики. Данная книга фокусируется на классической теории логики первого порядка. Первые две главы посвящены пропозициональной логике, которая интересна сама по себе и служит разминкой для разработки логики первого порядка в главах III и IV. И пропозициональная логика, и логика первого порядка имеют формальное понятие синтаксиса для формул, интуитивно понятную и прямолинейную семантику, а также системы доказательств, основанные на правилах вывода. Более того, для обеих справедливы теоремы о корректности и полноте (Soundness and Completeness Theorems). Примечательно, что логика первого порядка в некотором смысле является наиболее сильной логикой, обладающей всеми этими свойствами. Таким образом, пропозициональная логика и логика первого порядка служат эталонными системами, с которыми можно сравнивать все другие формальные системы.
Основные темы, рассматриваемые в книге, включают следующее:
2.0.1 Синтаксис и неформальная семантика
Пропозициональная логика и логика первого порядка используют формулы, построенные по точным синтаксическим правилам. В пропозициональной логике формулы строятся с помощью связок ∧ (конъюнкция, “и”), ∨ (дизъюнкция, “или”), ¬ (отрицание, “не”), → (импликация, “если-то”) и ↔︎ (эквивалентность, “тогда и только тогда”). Логика первого порядка добавляет кванторы «∀x» (универсальный, “для всех x”) и «∃x» (экзистенциальный, “существует x”), где переменная x пробегает некоторую область объектов (domain of objects). Логика первого порядка также добавляет функциональные символы и символы отношений (relation symbols).
2.0.2 Формальная семантика
Неформальные значения пропозициональных и логических формул первого порядка формализуются путем математического определения истинности или ложности формул. В общем случае истинность или ложность формулы зависит от того, как её нелогические компоненты интерпретируются в «интерпретации». Интерпретации в пропозициональной логике довольно просты: они состоят в присваивании значений T или F пропозициональным переменным. Интерпретации в логике первого порядка гораздо сложнее: они требуют выбора области объектов («универсума») для переменных и выбора значений для функциональных символов и символов отношений.
Некоторые формулы истинны при всех интерпретациях; такие формулы называются «общезначимыми».
2.0.3 Доказательства и доказуемость (Proofs and provability)
Пропозициональная логика и логика первого порядка имеют эффективные системы доказательств, в которых формулы выводятся из аксиом с помощью правил вывода. Для пропозициональной логики используется система доказательств PL, в которой модус поненс (modus ponens) является единственным правилом вывода. Наша система доказательств FO для логики первого порядка имеет два правила вывода: модус поненс и правило обобщения.
2.0.4 Корректность и полнота
Теорема о корректности утверждает, что только общезначимые формулы имеют формальные доказательства. Теорема о полноте утверждает, что все общезначимые формулы имеют формальные доказательства. И пропозициональная логика, и логика первого порядка удовлетворяют теоремам о корректности и полноте. Это удивительный факт!
Часто работают с наборами аксиом; например, аксиомами групп, аксиомами вещественно замкнутых полей, аксиомами арифметики Пеано (PA) для (неотрицательных) целых чисел или аксиомами теории множеств Цермело-Френкеля (ZF). Теоремы о корректности и полноте по-прежнему применимы и утверждают, что формула может быть доказана из аксиом тогда и только тогда, когда она является логическим следствием аксиом. Учитывая, что логика первого порядка достаточно сильна, чтобы охватить всю математику через теорию множеств первого порядка ZF, это означает, что существует формальная система первого порядка, которая может охватить практически все математические общезначимости.[^3]
2.0.5 Вычислимость и разрешимость (Computability and decidability)
Понятие вычислимости является центральным в математической логике. Интуитивное представление о вычислимости соответствует тому, что может быть выполнено идеализированным компьютером, не ограниченным ресурсами времени и пространства. Это математически точно определяется машинами Тьюринга, которые предоставляют простую, но гибкую модель вычислений, способную имитировать действие любого современного компьютера и, таким образом, в соответствии с «тезисом Чёрча-Тьюринга», дают математическое определение того, что означает вычислимость функции.
Множество или отношение называется вычислимым, или «разрешимым», если существует алгоритм (машины Тьюринга) для определения, принадлежит ли данный входной элемент множеству. Оно называется «перечислимым» (computably enumerable) или «Тьюринг-перечислимым» (Turing enumerable), если существует алгоритм, который перечисляет все элементы множества или отношения.
2.0.6 Неразрешимость (Undecidability)
Удивительно, но оказывается, что существуют простые для описания множества, которые неразрешимы; соответственно, существуют простые для описания функции, которые невычислимы. Ярким примером этого является «проблема остановки». А именно, множество (описаний) машин Тьюринга, которые не останавливаются, неразрешимо. Другими словами, не существует алгоритма, который для произвольной машины Тьюринга M корректно определял бы, остановится ли M когда-либо.
Неразрешимость проблемы остановки можно использовать для доказательства того, что множество истинных утверждений первого порядка о целых числах неразрешимо (при работе с языком, содержащим функциональные символы + и ⋅ для сложения и умножения). Более того, множество истинных утверждений первого порядка о целых числах даже не является перечислимым.
2.0.7 Неполнота (Incompleteness)
Набор аксиом называется «полным», если любая (замкнутая) формула либо доказуема, либо опровержима из аксиом.[^4] По сути, полнота означает, что аксиомы достаточны для полного описания того, что истинно или ложно.
Первая и вторая теоремы Гёделя о неполноте утверждают, что не существует полной аксиоматизации теории первого порядка для целых чисел. Теория первого порядка арифметики Пеано (PA) является наиболее распространённой аксиоматизацией целых чисел. Аксиомы PA разрешимы (decidable); отсюда следует, что теоремы PA перечислимы (computably enumerable). Это в сочетании с неразрешимостью проблемы остановки и представимостью (representability) проблемы остановки в арифметике означает, что арифметика Пеано неполна.
На первый взгляд, теоремы о полноте и неполноте могут показаться противоречащими друг другу. Но здесь нет противоречия. Теорема о полноте утверждает, например, что все формулы C, являющиеся логическими следствиями аксиом PA (арифметики Пеано), имеют доказательства из аксиом PA. То есть, если C истинна в любой модели, где выполняются аксиомы PA (т. е. в любой интерпретации PA), то C может быть доказана из аксиом PA. Теорема о неполноте подразумевает, что существуют формулы C, которые истинны для стандартных целых чисел, но не имеют доказательств из аксиом PA. Дело в том, что существуют другие интерпретации PA, называемые «нестандартными моделями PA», которые отличаются от «настоящих» целых чисел! Существуют формулы C, которые истинны в стандартных целых числах, но ложны в некоторых нестандартных моделях. Это утверждения, которые истинны для стандартных целых чисел, но не могут быть доказаны из аксиом арифметики Пеано.
2.1 Как читать эту книгу
На Рисунке 1 показаны зависимости между главами. Хотя рекомендуется читать главы по порядку, также можно пропустить главы о доказательствах в пропозициональной логике и логике первого порядка и всё равно прочитать часть глав об алгоритмах и машинах Тьюринга, а также, возможно, ещё не написанную главу о теореме Эрбрана.
Эта книга предназначена для использования в курсе по математической логике. Даже если главы изучаются по порядку, важно ввести алгоритмические понятия и идею вычислимости в начале курса. Это поможет подготовить студентов к более строгому изучению этих важных тем в главах V и VI.
Альтернативно, курс может начаться с первой части главы V, затем рассмотреть неразрешимость с использованием раздела V.6 и главы VI, а после этого изучить первые четыре главы, добавляя темы из остальной части главы V.
Для курсов, разбитых на четверти, автор старается пройти материал вплоть до теоремы о полноте в первой четверти, а затем изучить теоремы о неполноте во второй четверти. Это делает курс довольно сжатым, и обычно некоторые детали приходится опускать. Такой график был бы более спокойным для двух семестров вместо двух четвертей.
Во всех главах есть упражнения. Многие из них проверяют базовое понимание материала, но некоторые вводят новые концепции. Читателям настоятельно рекомендуется попробовать решить упражнения.
Структура работы
| 2: Это было начато в основном Фреге в 1879 году, но потребовало значительной доработки, чтобы достичь современной формы. [^2]: Машины Тьюринга были определены Тьюрингом в 1936 году. Другие эквивалентные определения вычислимости были независимо разработаны Чёрчем, Постом, а также Гёделем и Эрбраном. [^3]: Однако, как обсуждается ниже, охват всех математических общезначимостей не то же самое, что охват всех математических истин. [^4]: Здесь мы немного вольно определяем понятие «полнота». См. Определение III.98 для точного определения в логике первого порядка, применяемого к теориям. |
|---|
| title: “Chapter I” output: bookdown::gitbook |