Minimal logic and automated proof verification. (2019)

View/ Open
Type of Content
Theses / DissertationsThesis Discipline
MathematicsDegree Name
Doctor of PhilosophyPublisher
University of CanterburyLanguage
EnglishCollections
Abstract
We implement natural deduction for first order minimal logic in Agda, and verify minimal logic proofs and natural deduction properties in the resulting proof system. We study the implications of adding the drinker paradox and other formula schemata to minimal logic. We show first that these principles are independent of the law of excluded middle and of each other, and second how these schemata relate to other well-known principles, such as Markov’s Principle of unbounded search, providing proofs and semantic models where appropriate. We show that Bishop’s constructive analysis can be adapted to minimal logic.