License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2021.11
URN: urn:nbn:de:0030-drops-134455
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13445/
Go to the corresponding LIPIcs Volume Portal

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

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle

pdf-format:
LIPIcs-CSL-2021-11.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{bickford_et_al:LIPIcs:2021:13445,
  author =	{Mark Bickford and Liron Cohen and Robert L. Constable and Vincent Rahli},
  title =	{{Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Christel Baier and Jean Goubault-Larrecq},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13445},
  URN =		{urn:nbn:de:0030-drops-134455},
  doi =		{10.4230/LIPIcs.CSL.2021.11},
  annote =	{Keywords: Intuitionism, Extensional type theory, Constructive Type Theory, Realizability, Choice sequences, Classical Logic, Law of Excluded Middle, Theorem proving, Coq}
}

Keywords: Intuitionism, Extensional type theory, Constructive Type Theory, Realizability, Choice sequences, Classical Logic, Law of Excluded Middle, Theorem proving, Coq
Collection: 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Issue Date: 2021
Date of publication: 13.01.2021
Supplementary Material: All the results in the paper are formalized in Coq, see https://github.com/vrahli/NuprlInCoq/tree/ls3/.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI