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

60 Downloads (Pure)

Abstract

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
Volume183
DOIs
Publication statusPublished - 13 Jan 2021

Bibliographical note

Publisher Copyright:
© Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli.

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this