Какая парадигма автоматического доказательства теорем подходит для формализации в стиле Principia Mathematica?

У меня есть книга, которая, вдохновленная Принципами математики Рассела (PM) и логическим позитивизмом, пытается формализовать определенную область, определяя аксиомы и выводя из них теоремы. Короче говоря, он пытается сделать для своей области то, что PM пытался сделать для математики. Как и PM, он был написан до того, как стало возможным автоматическое доказательство теорем (ATP).

Я пытаюсь представить эти аксиомы в современной системе ATP и пытаюсь вывести теоремы, первоначально те, которые были выведены автором (вручную). Я не использовал систему АТФ раньше, и учитывая множество вариантов (HOL, Coq, Изабель и многие другие), каждый из которых имеет свои сильные и слабые стороны, и предполагаемые применения, трудно решить, что подходит для моего конкретного цель.

Формализм автора тесно отражает ПМ. Существуют классы (наборы?), Классы классов и т. Д. До 6 уровней иерархии. Существует логика первого порядка и, возможно, более высокого порядка. Учитывая связь с PM, я первоначально исследовал Metamath, так как несколько теорем PM были доказаны в MetaMath другими людьми. Тем не менее, Metamath, конечно, является проверяющим средством, а не системой ATP.

Просматривая описания различных систем ATP, я вижу несколько характеристик, таких как реализации теории типов Черча, конструктивных теорий типов, теорий интуиционистских типов, теории типизированных / нетипизированных множеств, естественного вывода, типов лямбда-исчислений, полиморфизма, теории рекурсивных функций и существование равенства (или нет). Короче говоря, каждая система, похоже, реализует совершенно другой язык и должна подходить для формализации разных вещей. Я предполагаю, что существующие библиотеки для формализации математики не имеют отношения к моей цели.

Буду очень признателен за любые советы относительно характеристик, которые мне следует искать при выборе АТФ, или за любые другие рекомендации, которые вы можете получить после прочтения этого вопроса. Для справки вот пример страницы из книги. К сожалению, как PM, это в примечании Пеано-Рассела.

Книга -

«Аксиоматический метод в биологии» (1937), Дж. Х. Вуджер, А. Тарский, В. Ф. Флойд

Аксиомы начинаются с простого. Например,

$x$$\alpha$$\alpha$$x$$y$$x$$z$$\alpha$$y$

$$S{ = }_{ Df }\hat { x } \hat { \alpha } \{ \alpha \subset \vec { { P }^{ ‘ } } x:.(y):yPx.\supset .(\exists z).z\in \alpha .\vec { { P }^{ ‘ } } y\cap \vec { { P }^{ ‘ } } z\neq \Lambda \}$$

Еще раз отметим, что это обозначение Пеано-Рассела (обозначение Принципов).

Более поздние аксиомы имеют биологическое содержание, например,

7.4.2 Когда гаметы двух членов менделевского класса объединяются в пары, образуя зиготы, вероятность объединения любой данной пары равна вероятности другой пары.

Насколько я понимаю, это был постулат менделевской генетики.

Я опускаю обозначения для этого, потому что это три строки длиной и основывается на ранее определенном контенте.

Пример теоремы -

Это, очевидно, несет в себе осмысленную интерпретацию в менделевской генетике, которую я, не будучи историком биологии, не понимаю. В книге это было выведено вручную.

Благодаря!

Principia Mathematica была в значительной степени ответом на различные парадоксы, обнаруженные в математической логике на рубеже 20-го века. Однако само произведение, которое часто косвенно хвалят как «нечитаемый шедевр», несколько неуклюже, и были созданы более современные основы. Чтобы описать большую часть математики, у вас есть несколько вариантов: теория категорий одна, теория типов была популярна в некоторых проектах как расширение лямбда-исчисления, но наиболее понятным и наиболее фундаментальным, вероятно, является теория множеств.

Теория множеств имеет несколько различных формулировок; Теория множеств Цермело Франкеля с аксиомой выбора является наиболее ортодоксальной, с любовью называемой энтузиастами теории множеств. Теория множеств Тарского-Гротендика - это еще одна теория, которая во многом похожа на которая включает аксиому Тарского для рассуждения о больших категориях. Они интересны для проверки, но несколько сложнее для автоматического доказательства теорем, потому что схема замены аксиом допускает бесконечное число аксиом, которые представляют собой проблему для реализации. В то время как эти основы совершенно разумны для систем проверки доказательства, таких как Мизар для теории множеств Тарского-Гротендика и Метамат для$\sf ZFC$$\sf\ ZFC$$\sf ZFC$для реальной системы доказательства теорем было бы неплохо иметь конечную аксиоматизацию.

Основой, которая, вероятно, является наиболее подходящей для этого, является теория множеств фон Неймана – Бернайса – Гёделя или , которая допускает конечную аксиоматизацию, будучи двухсортированной теорией, которая имеет онтологию как собственных классов, так и множеств. Кроме того, было доказано, что является консервативным расширением , так что любая теорема является теоремойN B G Z F C N B G Z F $\sf NBG$$\sf NBG$$\sf ZFC$$\sf NBG$$\sf ZFC$, Причина, по которой эта теория является наиболее подходящей для автоматизированного рассуждения, на мой взгляд, заключается в том, что ее можно выразить в логике первого порядка, которая допускает эффективное, надежное и полное доказательство исчисления, а конечная аксиоматизация означает, что ее можно использовать с разрешением первого порядка, которое дает нам опрятный результат: если утверждение разрешимо, в конечном итоге будет найдено доказательство.

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

Art Quaife проделал некоторую работу над этим в: Автоматизированной разработке фундаментальных математических теорий, где он реализовал в логике первого порядка в клаузальной форме, чтобы она могла использоваться проверяющим теорему на основе разрешения (Otter) и отличным справочником для решения Основой для такого рода работ является « Введение Эллиотта Мендельсона в математическую логику».$\sf NBG$

Теперь современные помощники по доказательству часто меньше заботятся об основах парадигмы « Принципов математики» и более полезны для доказательства теорем для повседневной работы, поэтому они имеют некоторую поддержку для фрагментов логики более высокого порядка, решения SAT / SMT, теорий типов и других более неформальные и менее основательные подходы. Но если вы пытаетесь сделать что-то вроде Principia Mathematica, то доказатель теоремы первого порядка с конечно-аксиоматизируемой теорией множеств первого порядка идеален.

Для некоторых примеров того, как автоматизированные теоремы доказывают проблемы атак из этих оснований, на сайте «Тысячи проблем для теорем» ( TPTP ) есть множество проблем, и вы заметите, что многие фундаментальные проблемы теории чисел основаны на теория множеств. Если у вас есть время, посмотрите NUM006-1.p на их сайте: гипотеза Гольдбаха. Вы можете попробовать запустить его, и если его можно будет решить, в конечном итоге будет найдено доказательство .$\sf NBG$

Теоремы в вашей книге почти наверняка будут теоремами если они написаны на языке теории множеств. Аксиомы генетики в этой книге почти наверняка будут представлены как определения на множестве теоретических предикатов, так же, как арифметика Пеано представлена ​​в как определения предикатов. Оттуда вы следуете процедуре разрешения в любом СПС. Выберите утверждение, которое хотите доказать, опровергните его, преобразуйте в нормальную форму Сколема, затем в клаузальную форму и следуйте резолюции. Когда вы найдете пустое предложение, вы обнаружите противоречие, подтверждающее утверждение.N B $\sf NBG$$\sf NBG$

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

∀ ∈ ↔ ∈ $\forall$ xy ( z (z x z y) x = y)$\forall$$\in$$\leftrightarrow$$\in$$\leftrightarrow$

Немного предостережения: кривая обучения для этого действительно очень крутая. Если вы намерены продолжать это, вы, возможно, окажетесь в течение нескольких лет, прежде чем поймете всю проблему, как это было в моем опыте. Возможно, вы захотите изучить теорию с менее основополагающего подхода, прежде чем взять на себя огромную задачу встраивания ее в основополагающий язык для всего. В конце концов, вам не обязательно рассуждать о бесчисленном множестве смешивающихся генов.

Несколько моментов:

1. Насколько я знаю, Principia Mathematica по существу использует формализацию теории множеств с использованием типизированной логики первого порядка. Поэтому было бы заманчиво использовать автоматическую проверку теорем первого порядка, такую ​​как Prover 9 или, возможно, ACL2, чтобы формализовать ваши утверждения. Тем не менее, я вижу несколько теоретико-множественных конструкций (таких как , ), которые обычно не очень хорошо работают с АТФ первого порядка.∩ , $\in$$\cap, \subset$

2. Любой современный интерактивный помощник по проверке наверняка сможет выразить и подтвердить ваши утверждения, как предположил Андрей. Фактически, поскольку существуют некоторые утверждения, в том числе и арифметические, было бы разумно использовать такую ​​систему, как Изабель , Coq или HOL, которая уже имеет обширные теории для обработки утверждений арифметики. Мой акцент на модернизме не случаен: со времен Automath были достигнуты большие успехи в юзабилити, и я искренне думаю, что вы окажете себе медвежью услугу, если воспользуетесь чем-то, что активно не разрабатывалось с 90-х годов (если бы вы даже могли его получить). работать!)

3. Наконец, ITP и ATP имеют довольно сложные кривые обучения, и вы не должны ожидать, что сможете ввести эти теоремы в такую ​​систему, как если бы вы писали доказательство . Ожидайте серьезное разочарование и потерянное время, особенно в первые месяцы (да, месяцы). Вам определенно нужно сначала пройтись по некоторым учебникам, прежде чем приступить к основной формализации.$\LaTeX$