Proof Of Calculi Equivalence In The Hol Theorem Prover

The aim of this project is to prove the equivalence of sequent calculus, natural deduction and Hilbert calculus for classical propositional logic in the HOL theorem prover. HOL is an interactive theorem prover implemented in Standard ML, which uses Higher Order Logic as an environment to formalise proofs. The task will be broken down into smaller lemmas which will combine into a proof of equivalence. I will first prove equivalence in intuitionistic logic, and then move to classical. The theorem(s) can be stated: β€œThere exists a proof of πœ‘ in calculus X if and only if there exists a proof of πœ‘ in calculus Y”, where πœ‘ is a provable formula in intuitionistic/classical logic. If time allows, I would like to also do the proofs for the first-order logic or some modal logic(s).

Alexander Cox

Australian National University

Alexander (Alex) is a theoretical computer science student at the Australian National University. He is passionate about mathematical logic and mathematical models of computation (such as lambda calculus and automata). He also studies philosophy, focusing on moral, ethical and political philosophy and philosophy of science. In his spare time he enjoys spending time with his wife and going for walks.

You may be interested in

Nicholas Garrett

Nicholas Garrett

Curve Shortening Flow and Grayson's Theorem
Michael Carr

Michael Carr

Advanced Bayesian Statistical Inference Methods for Simulation-Based Models in Cell Biology
Daniel Stratti

Daniel Stratti

Rank Embeddings for Detecting Ranking Outliers
Jonah Klowss

Jonah Klowss

Finite Transition Times for Diffusion-Decay Problems
Contact Us

We're not around right now. But you can send us an email and we'll get back to you, asap.

Not readable? Change text.