Open bar - a Brouwerian intuitionistic logic with a pinch of excluded middle

Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli

Research output: Contribution to journalConference articlepeer-review

56 Downloads (Pure)


One of the differences between Brouwerian intuitionistic logic and classical logic is their treatment of time. In classical logic truth is atemporal, whereas in intuitionistic logic it is time-relative. Thus, 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 paper demonstrates that, nonetheless, the two approaches are not necessarily incompatible by introducing an intuitionistic type theory along with a Beth-like model for it that provide some middle ground. On one hand they incorporate a notion of progressing time and include evolving mathematical entities in the form of choice sequences, and on the other hand they are consistent with a variant of the classical LEM. Accordingly, this new type theory provides the basis for a more classically inclined Brouwerian intuitionistic type theory.
Original languageEnglish
Pages (from-to)11:1-11:23
JournalLeibniz International Proceedings in Informatics
Publication statusPublished - 13 Jan 2021


  • Intuitionism
  • Extensional type theory
  • Constructive Type Theory
  • Realizability
  • Choice sequences
  • Classical Logic
  • Law of Excluded Middle
  • Theorem proving
  • Coq


Dive into the research topics of 'Open bar - a Brouwerian intuitionistic logic with a pinch of excluded middle'. Together they form a unique fingerprint.

Cite this