Re: [CL] The Decidability Fetish
Robert and Michel,
As you know, I have a great deal of sympathy for
the IFF project, and I have consistently voted for
it and supported it during the SUO discussions.
I have also questioned the desirability of basing
all of mathematics on set theory, and I have been
interested in various alternatives or supplements,
such as category theory, mereology, and topos theory.
But I also sympathize with the needs of programmers
who want tools they can pick up and use without
spending several years of advanced study in math.
Paragraphs like the following do not give me the
impression that the IFF report will receive an
enthusiastic welcome from most working programmers:
REK> The ``adjunctive axiomatization'' style follows
> the conceptual lines expressed in the book *Set for
> Mathematics* by Lawvere and Rosebrugh, which presents
> the category of sets in terms of Topos Theory. The
> third phase of the IFF development is presenting the
> IFF descriptive metatheory in terms of Topos Theory.
This sounds like an interesting research project.
That is good. But it is not what the IEEE is looking
for in a standard for the SUO. For example, the IEEE
standards for floating-point arithmetic do not go into
the details of Peano's axioms.
The standards documents are written for programmers
and engineers who want to start implementing the spec's.
They do not want to spend time studying proofs of
soundness, completeness, and other such properties.
How close are we to getting documents that ordinary
programmers can begin to use?
John Sowa