FOM: Conservative Extension

[Roger Bishop Jones]

Recent elucidation of the notion of "conservative extension" has
omitted mention of what seems to me its most important role in f.o.m.

The idea of conservative extension is a generalisation
of the notion of definition. (and is used self-consciously
in that way by some proof tools e.g. HOL)

What distinguishes a "foundation system" from other logical
systems is that in a foundation system it is possible to
derive the main body of mathematics using only conservative
extensions. (of course, people used to say "definitions")

So the notion of "conservative extension" features in the
*definition* of a f.o.m. (or at least, in my preferred definition)

This draws out the fact that the thing which a "foundation"
does (e.g. ZFC) which is not done by a logic (e.g. FOL)
is to provide a formal basis for settling questions of
consistency, or alternatively put, for settling when a new concept
is well-defined, without which the soundness of proofs cannot
be assured.

The importance of this aspect of the notion of conservative extension
is perhaps more conspicuous for those who want to use formal systems
for deriving mathematics (usually with the help of a machine) than
it is for f.o.m. researchers, who are primarily interested in 
metamathematical results.

The use of conservative extensions rather than more restricted
forms of definition is also helpful in mitigating some of the objections
which have been raised against set theoretic foundations.
In particualar it allows one to introduce constructors which are
conventionally defined using some arbitrary "coding" (e.g. the ordered
pair constructor) by specifying the properties of the constructor rather than
a specific encoding.

Roger Jones



email: rbjones at rbjones.com   www:  http://www.rbjones.com/