Книга по математической логике, в которой используется помощник по доказательству?

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

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

РЕДАКТИРОВАТЬ

Мне нравятся ответы, опубликованные до сих пор, и я хочу оставить это открытым на некоторое время, чтобы собрать другие рекомендации в одном месте. Однако, открыв его, я также нашел следующие отличные ресурсы, связанные с этим вопросом, а именно этот список ресурсов и эту книгу/сборник заметок Джереми Авигада. Эти ресурсы кажутся теми, что я искал, и могут быть полезны другим, кто наткнется на этот пост.

РЕДАКТИРОВАТЬ 2

Одна функция, которую я действительно хотел бы видеть, которую я до сих пор не видел в предложениях, — это книга, которая также формализует свою металогику в помощнике по проверке. Например, мне бы понравилась книга, которая доказывает (например) теорему о надежности и показывает, как такое доказательство можно реализовать с помощью помощника по доказательству.

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

Будут ли учитываться тексты из Open Logic Project, где у них есть разработанный вручную веб-инструмент для формальной проверки доказательств в их системах? Или вы спрашиваете конкретно о чем-то, используя помощника по проверке доказательств общего назначения?
@DanielSchepler Меня устраивает любое конкретное программное обеспечение, если оно используется в учебных целях наряду с ресурсом для обучения математической логике. Похоже, OLP - отличный ресурс, хотя я не могу найти их веб-инструмент для проверки доказательств, о котором вы упомянули.
Чтобы намочить ноги, вы можете рассмотреть мое бесплатное программное обеспечение для проверки доказательств, которое можно загрузить с моей домашней страницы на dcproof.com с сопровождающим руководством. Он был разработан, чтобы познакомить студентов с основными методами доказательства. Он основан на упрощенной форме естественной дедукции и теории множеств, которая, по-видимому, неявно используется в большинстве учебников по математике (не в стандартных FOL или ZFC).
Относительно вашего второго редактирования: в черновике, на который я ссылаюсь, обоснованность и полнота классической пропозициональной логики показаны в конце главы о естественной дедукции. Формализация полной металогики, используемой в книге, — сложный вопрос; тогда книга явно должна провести различие между своей металогикой и объектной логикой, которую она хочет изучать. Обычно помощник доказательства (и его логика) используется в качестве металогики, в которой обсуждаются результаты. Тогда формализовать (!) все тонкости логики помощника по доказательству — это отдельная задача.
Веб-сайт Дэна бесполезен для реальной математической работы, такой как бесполезное доказательство теоремы Шредера-Бернштейна .
Для тех, кто заинтересован в Proof Assistants, есть новый предлагаемый сайт SE ProofAssistants.

Ответы (3)

Я настоятельно рекомендую «Руководство по практической логике и автоматизированному мышлению» Джона Харрисона . Примеры программирования в большей степени связаны с тем, как реализовать помощники по проверке и процедуры принятия решений, а не с тем, как использовать помощник по проверке, но я думаю, что они отвечают вашему желанию в реализации, которая разъясняет ключевые концепции. Все примеры даны на языке функционального программирования OCaml .

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

Попробуйте фундаментальные методы доказательства в информатике. Он использует Athena в качестве помощника по доказательству. Он учит как логике, так и языку.

Если вы найдете этот сложный здесь простым — https://staff.washington.edu/jon/flip/www/userguide-nd.html Он работает с Python 2.7.

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

Вот некоторые ресурсы о Coq :

На сайте Lean Community есть страница с рекомендуемыми учебными ресурсами .

И давайте не будем забывать о HoTT:

Книга по математической логике, в которой используется помощник по доказательству?
СпросиСетьПолитика конфиденциальности1y, 0v