Turner, David A. (2021) Constructive mathematics, Church's Thesis, and free choice sequences. Lecture Notes in Computer Science, . ISSN 03029743. (doi:10.1007/9783030800499_44) (KAR id:88974)
PDF
Author's Accepted Manuscript
Language: English 

Download this file (PDF/186kB) 

Request a format suitable for use with assistive technology e.g. a screenreader  
Official URL: https://doi.org/10.1007/9783030800499_44 
Abstract
We see the defining properties of constructive mathematics as being the proof interpretation of the logical connectives and the definition of function as rule or method. We sketch the development of intuitionist type theory as an alternative to set theory. We note that the axiom of choice is constructively valid for types, but not for sets. We see the theory of types, in which proofs are directly algorithmic, as a more natural setting for constructive mathematics than set theories like IZF. Church’s thesis provides an objective definition of effective computability. It cannot be proved mathematically because it is a conjecture about what kinds of mechanisms are physically possible, for which we have scientific evidence but not proof. We consider the idea of free choice sequences and argue that they do not undermine Church’s Thesis.
Item Type:  Article 

DOI/Identification number:  10.1007/9783030800499_44 
Uncontrolled keywords:  constructive type theory, Church’s Thesis, free choice sequence 
Subjects: 
Q Science > QA Mathematics (inc Computing science) > QA 21 History of mathematics Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science Q Science > QA Mathematics (inc Computing science) > QA 8 Philosophy of mathematics 
Divisions:  Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing 
Depositing User:  David Turner 
Date Deposited:  01 Jul 2021 20:49 UTC 
Last Modified:  29 Jun 2022 20:48 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/88974 (The current URI for this page, for reference purposes) 
 Link to SensusAccess
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):