Optimality proof of Fareys sequence
Published:
Posts by Tags
Algebra
Formal logic
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:
Intuitionistic logic
A not not Brief Introduction to Kripke Semantics for Propositional Intuitionistic Logic
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.
Kripke semantics
A not not Brief Introduction to Kripke Semantics for Propositional Intuitionistic Logic
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.
Lean
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: