Download PDFOpen PDF in browser

On Expanding Standard Notions of Constructivity

EasyChair Preprint 189

5 pagesDate: May 30, 2018

Abstract

Brouwer developed the notion of mental constructions based on his view of mathematical truth as experienced truth. These constructions extend the traditional practice of constructive mathematics, and we believe they have the potential to provide a broader and deeper foundation for various constructive theories. We here illustrate mental constructions in two well-studied theories – computability theory and plane geometry – and discuss the resulting extended mathematical structures. Further, we demonstrate how these notions can be embedded in an implemented formal framework, namely the constructive type theory of the Nuprl proof assistant. Additionally, we point out several similarities in both the theory and implementation of the extended structures.

Keyphrases: Free choice sequences, Intuitionistic mathematics, Nuprl, computability, geometry, projective plane, type theory

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:189,
  author    = {Liron Cohen and Ariel Kellison},
  title     = {On Expanding Standard Notions of Constructivity},
  doi       = {10.29007/bsfx},
  howpublished = {EasyChair Preprint 189},
  year      = {EasyChair, 2018}}
Download PDFOpen PDF in browser