SUO: 21 May 2002 -- Unanswered Questions About SUMO Set Theory
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
SUO WG Members,
I have asked the SUMO Team a fairly routine set of questions:
| 1. What is the exact formulation of set theory used in SUMO?
|
| The extended family of SUMO documentation contains the
| remark that the set theory supposedly "built into KIF"
| is "a version of Von Neumann/Bernays/Godel set theory".
|
| 2. Can you provide a reference and a justification for this assertion?
|
| If the SUMO proposal no longer depends on this built-in set theory,
| it remains to specify what variety of set theory it does depend on.
|
| 3. Can you provide a detailed account and a justification of
| the differences, if any, between the SUMO set theory and
| standard versions of Von Neumann/Bernays/Godel set theory?
|
| A similar request would of course attach to departures of SUMO
| from any other standard versions of set theory that it invokes.
I have yet to receive anything approaching a straightforward answer.
I think that it should be obvious why we need to know these things,
but just in case, I will detail a few of the reasons that everyone
will appreciate are sufficiently compelling.
Writing axioms for set theory is an extremely treacherous business,
as the history of mathematics amply demonstrates, and it is hardly
a job for amateurs. The handful of standard variants that we have
to choose from, differing at some points in significant ways, have
all been worked over for a hundred years or more by a multitude of
very picky people, not to mention a few of the ablest minds of the
last couple of centuries. Needless to say, so I'd probably better
say it anyway, the intricate interactions of these sorts of axioms
do not allow the average axiom hacker the freedom to cut and paste
at will, snipping one there and jamming another there, without the
risk of total disaster. As a matter of fact, even with all of the
accumulated experience and the prima facie confidence that we have
inherited with the standard alternatives, we can't even prove them
consistent, the last that I heard, nor establish many other wished
for properties. Innovation is certainly possible, in this area as
in any other, but then one gives up the cachet of abridged refs to
established standards and has to provide independent justification.
Any measure of confidence in a proposed system depends on getting
clear, direct, and detailed answers to the questions I have asked.
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤