On Expanding Standard Notions of Constructivity

EasyChair Preprint 189

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

@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}}