[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.


IMartin Davis
Professor Emeritus, Courant-NYU
Visiting Scholar, UC Berkeley
eipye + 1 = 0

More information about the FOM mailing list