FOM: "function" as a basic mathematical concept

[Vaughan Pratt]

From: Stephen G Simpson <simpson at math.psu.edu>
Date: Wed, 14 Jan 1998 15:11:21 -0500 (EST)
>
>I'm wondering what will happen when you try to set up the rudiments of
>real analysis, in the elementary topos setup.  Will you get enough real
>analysis to build bridges?  Or will you get a horrible, ill-motivated
>mess that nobody can make sense out of?

I would expect a mess, but one no less horrible than what you get by
setting up real analysis in the ZFC setup.  It is one thing to claim that
it can be done, but it is all too easy to underestimate the complexity of
the passage from such an in-principle claim to its actual realization.

The situation is much the same as with Goedel numbers of recursive
functions witnessing say the existence of a recursive function f which
given i and j yields f(i,j) such that phi_{f(i,j)} = phi_j o phi_i
(effectiveness of composition).  No one questions the existence of such
Goedel numbers, but to my knowledge there exists no textbook containing
the actual Goedel number of a proof of a significant theorem in recursion
theory.

At the risk of undermining my point somewhat I will admit that I've
computed the Goedel number of a proof of Kleene's recursion theorem,
in a programming language designed expressly for making this task
easy:  the number is 3838203982098382039820993982082099383820909383
8203982098383820398209838203982099398208209938382090998382039820999.
I obtained it with pencil and paper, no calculators or computers.

To people who prefer to communicate their mathematics in English this
proof may well appear horrible and unmotivated.  To a person or computer
who prefers to communicate in terms of numbers, this number is a slick
two-line argument.

The traditional way to defend such arbitrary judgments of esthetic and
motivation is to rally one's friends around you and say "See, we all
disagree with you."  If you have a substantively different defense it
would be very interesting to see it.

---

Name: Vaughan Pratt
Position: Professor of Computer Science
Institution: Stanford University
Research interests: Foundations of computation and mathematics
For more information: http://boole.stanford.edu