FOM: Arbitrary objects

[Roger Bishop Jones]

Being in some doubt about the necessity for any additional logical
machinery for formalising such informal mathematical language
as:

	" let a be a natural number such that P "

I have paid scant attention so far to the discussion of arbirary objects.
However, after Martin Davis a requested a concise account of
the substance of Fine's book I have kept an eye open for a response.

Dan Velleman has come closest (IMO) to meeting the need and
his message has reinforced my doubt that a theory of arbitrary
objects does much for us.

It is standard practice in some subcultures of the "formal methods"
community to allow specifications to be developed by a sequence
of conservative extensions to some suitably rich foundation (e.g.
higher order logic or set theory).
The introduction of constants by loose conservative extension
seems to me to satisfy the needs for which "arbitrary objects" might
be thought necessary without any novel logical apparatus or theory.

The locution: " let a be a natural number such that P "
would then be formalised by infroducing a new constant "a"
with the conservative axiom |- P(a)
(allowed only if it is proven that there exists an a such that P)
It is also possible to achieve similar local effects with variables in
proofs, again all without any modification to the underlying logical
system or its theory.
The effect of the conservative extension is that the range of the
"arbitrary" or as I prefer to call it "loosely defined" object a is 
found by checking its values in the various models of the resulting
theory, and that complex dependencies between the values
of such constants can be realised.

I am interested to know whether the advocates of special mechanisms for
or theories about arbitrary objects think that by these means anything can
be achieved which is not accomplished by the introduction of new constants
by loose conservative extension, and if so what.

Roger Jones