Formalization of \(\neg \neg (A \lor \neg A)\) in Lean
Published:
The first time I saw the following exercise was in OPLSS 2015. A proof using the axiomatization of intuitionistic logic is the following:
TODO
Jose Abel Castellanos Joo
Ph.D. in Computer Science
- Albuquerque, New Mexico, U.S.
- University of New Mexico
- Google Scholar
- ORCID
- GitHub
- X (formerly Twitter)
- YouTube
You May Also Enjoy
Optimality proof of Fareys sequence
less than 1 minute read
Published:
A not not Brief Introduction to Kripke Semantics for Propositional Intuitionistic Logic
24 minute read
Published:
In this post we motivate the study of Kripke semantics for propositional intuitionistic logic by showing fundamental properties at the proof theory level using \(n+1\)-valued logics. Some non-theorems of propositional intuitionistic logic (like the excludded middle principle) are discussed using this approach.