Download PDFOpen PDF in browserOn Expanding Standard Notions of ConstructivityEasyChair Preprint 1895 pages•Date: May 30, 2018AbstractBrouwer 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
|