KnowledgeBase » 
PUBLICATION
» ID = 780
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020
Abstract
One the differences between intuitionistic logic and classical logic is their treatment of time. In classical logic truth is atemporal, while in intuitionistic logic truth is time-relative. Due to this difference, intuitionistic logic can derive counterexamples to standard axioms of classical logic. This is because in intuitionistic logic it is possible to acquire new knowledge as time progresses, whereas the classical Law of Excluded Middle (LEM) is essentially flattening the notion of time stating that it is possible to decide whether or not some knowledge will ever be acquired.This seems to indicate an incompatibility between classical logic and intuitionistic logic. However, this paper demonstrates that this is not necessarily so by introducing an intuitionistic type theory along with a Beth-like model for it which provide some middle ground. On one hand they incorporate a notion of time and include evolving mathematical entities in the form of choice sequences, and on the other hand they are consistent with versions of classical axioms such as LEM. Thus, this new type theory provides the basis for a more classically inclined intuitionistic type theory.