This HTML5 document contains 25 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n6doi:10.1007/
dctermshttp://purl.org/dc/terms/
n18https://kar.kent.ac.uk/id/eprint/88974#
n22https://kar.kent.ac.uk/88974/
n2https://kar.kent.ac.uk/id/eprint/
wdrshttp://www.w3.org/2007/05/powder-s#
n19http://purl.org/ontology/bibo/status/
dchttp://purl.org/dc/elements/1.1/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n17https://kar.kent.ac.uk/id/subject/
n20https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n12http://eprints.org/ontology/
n11https://kar.kent.ac.uk/id/event/
bibohttp://purl.org/ontology/bibo/
n4https://kar.kent.ac.uk/id/publication/
n7https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n9https://kar.kent.ac.uk/id/
n16https://kar.kent.ac.uk/id/document/
xsdhhttp://www.w3.org/2001/XMLSchema#
n14https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n8https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:88974
rdf:type
n12:ConferenceItemEPrint n12:EPrint bibo:Article bibo:AcademicArticle
rdfs:seeAlso
n22:
owl:sameAs
n6:978-3-030-80049-9_44
n12:hasAccepted
n16:3242285
n12:hasDocument
n16:3242285
dc:hasVersion
n16:3242285
dcterms:title
Constructive mathematics, Church's Thesis, and free choice sequences
wdrs:describedby
n14:export_kar_RDFN3.n3 n20:export_kar_RDFN3.n3
dcterms:date
2021-07-02
dcterms:creator
n8:ext-d.a.turner@kent.ac.uk
bibo:status
n19:peerReviewed n19:published
dcterms:publisher
n7:ext-1c5ddec173ca8cdfba8b274309638579
bibo: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.
dcterms:isPartOf
n4:ext-03029743 n9:repository
dcterms:subject
n17:QA75 n17:QA21 n17:QA8
bibo:authorList
n18:authors
bibo:presentedAt
n11:ext-8b7d32058a37e95209bc531c4ded110e