Корректор по написанию математики

Я хотел бы написать математические доказательства, используя некоторый помощник по доказательствам. Все будет написано с использованием логики первого порядка (с равенством) и естественного вывода. Фон - теория множеств (ZF). Например, как я мог написать следующее доказательство?

Аксиома: $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$

Теорема: $\forall x\forall y(\forall z(z\notin x)\land\forall z(z\notin y)\rightarrow x=y)$

То есть пустой набор уникален.

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

Спасибо.

И Кок, и Изабель могут это сделать.

[Coq] Вот статья, обсуждающая, как кодировать ZFC в CIC, на которой основан Coq.

Бенджамин Вернер: Наборы в Типах, Типы в Наборах (1997). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Изабель] Есть библиотека для ZF.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html

Перемещено из комментария по предложению Каве

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

Тогда вам нужно посвятить себя изучению корректора. Связанный документ - это учебное пособие по освоению Coq. Чтобы стать экспертом Coq, нужны годы преданности и практики, но простые теоремы могут быть доказаны во второй половине дня. Ключом к изучению Coq или любого другого помощника по доказательствам является создание доказательств, таких как те, что приведены в связанном документе. Просто чтение газеты очень мало поможет, потому что весь опыт взаимодействия с помощником по корректуре не может быть хорошо передан на бумаге.

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

Когда вам удастся доказать эти теоремы, не стесняйтесь размещать здесь свои ответы и, возможно, оставить несколько комментариев о вашем опыте.

Готовы ли вы принять вызов?

Есть много статей по математике, написанных с использованием ассистента Mizar: http://mizar.org/fm/

Дейв Кларк предлагает Coq, но на самом деле Изабель кажется гораздо лучшей идеей, поскольку у нее есть библиотека для ZF . Изабель также очень зрелая и включает в себя широкий спектр тактик и расширений.

Я лично не использовал Mizar, но это может быть хорошо.

как я мог написать следующее доказательство?

В Изабель / ZF вы можете написать что-то вроде этого

theory csthquestion imports Main

begin

theorem empty_unique:
shows "\<forall> x.\<forall>y.(\<forall>z. (z\<notin>x)) \<and> (\<forall>z.(z\<notin>y)) \<longrightarrow> x=y"
    by auto

end

Как видите, Изабель доказывает это автоматически. Конечно, вы можете написать более подробное доказательство, если вы действительно хотите.

Эта самая теорема является проработанным примером (см. Пример 11) в учебном пособии, включенном в мое программное обеспечение DC Proof 2.0. Загрузите его бесплатно на моем сайте http://www.dcproof.com