Certified Soundness of Simplest Known Formulation of First-Order Logic

John Bruntse Larsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

51 Downloads (Pure)


In 1965, Donald Monk published a paper about an axiomatic system for first-order predicate logic that he described as “the simplest known formulation of ordinary logic”. In this paper we show work in progress on certifying soundness of this system in the interactive proof assistant Isabelle. Through this work we demonstrate the usefulness of using proof assistants for validating mathematical results. This work also establishes an outline for future work such as a certified completeness proof of the axiomatic system in Isabelle.
Original languageEnglish
Title of host publicationProceedings of the ESSLLI 2017 Student Session
Publication date2017
Publication statusPublished - 2017
Event29th European Summer School in Logic, Language & Information - Toulouse, France
Duration: 17 Jul 201728 Jul 2017
Conference number: 29


Conference29th European Summer School in Logic, Language & Information

Cite this