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

Research output: Contribution to journalConference articlepeer-review

Authors

Colleges, School and Institutes

External organisations

  • Ben-Gurion University of the Negev
  • Cornell University

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.

Details

Original languageEnglish
Pages (from-to)11:1-11:23
JournalLeibniz International Proceedings in Informatics
Volume183
Publication statusPublished - 13 Jan 2021

Keywords

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