[FOM] Constructive treatment of computability theory in Kleene's IM
Martin Davis
martin at eipye.com
Wed Jun 19 16:20:28 EDT 2013
In "Introduction to Metamathematics", Kleene is very careful to stick
to constructive proofs in his treatment of computability aka general
recursiveness. Specifically, he was unwilling to include the empty
set among the recursively enumerable sets (defined as the range of a
(total) recursive function) because of the use of non-constructive
excluded middle in asserting that a set of natural numbers (as for
example defined by a Pi-0-1 predicate) is either empty or has a least element.
Martin
IMartin Davis
Professor Emeritus, Courant-NYU
Visiting Scholar, UC Berkeley
eipye + 1 = 0
More information about the FOM
mailing list