FOM: Arbitrary Objects

[Harvey Friedman]

Let me try to do something novel with this discussion of "arbitrary objects".

I had already given some of the obvious arguments against "arbitrary" being
a predicate (adjective) in my posting of 12:48PM  1/28/02.

So now let us assume that "arbitrary" is a predicate on objects. Let us see
what axioms we want to place on this concept. We write Arb(x) for "x is an
arbitrary object".

We first want

1. There exists an arbitrary object. I.e., (therexists x)(Arb(x)).

This is not very interesting by itself.

Obviously we can't have

*every property holds of some object holds of all arbitrary objects*

for that leads to an inconsistencyl see my earlier posting cited above.

However, what about

2. Every property either holds of all arbitrary objects or fails of all
arbitrary objects.

This seems interesting, although perhaps that is not something that
"arbitrary is a predicate" advocates would adhere to. I just don't know, as
I am not one of them.

We can present 2 more formally as follows.

2. (forall x)(Arb(x) implies phi) or (forall x)(Arb(x) implies notphi),
where phi is any formula of first order predicate calculus with equality
not mentioning Arb, all of whose free variables are x.

Thus we can think of 1,2 as an interesting extension of the usual first
order predicate calculus with equality, say with a countable infinity of
constant, relation, and function symbols.

CONSERVATIVE EXTENSIONS.

We can now ask

**Is this extension of first order predicate calculus conservative over
first order predicate calculus?**

The obvious answer is yes. This is because given any structure interpreting
everything except Arb, we can interpret Arb to hold of and only of any
particular object in the domain.

It now makes sense to strengthen 1 as follows:

1'. There exist infinitely many objects. This is a scheme.

The appropriate conservation question is:

**Is 1',2 conservative over first order logic with the axiom scheme "there
are infinitely many objects"?**

The answer is yes.

In fact, one can strengthen 2 considerably as follows:

2'. (forall distinct x1,...,xn)(if Arb(x1),...,Arb(xn) then (phi(x1,...,xn)
iff phi(xi1,...,xin))), where x1,...,xn are distinct variables, and
i1,...,in is a permutation of x1,...,xn, and phi is any formula not
mentioning Arb all of whose free variables are among x1,...,xn.

Again, 1',2' is conservative over first order logic with the axiom scheme
"there are infinitely many objects", by an argument using Ramsey's theorem.
I.e., the x such that Arb form an infinite set of indicernibles.

We now come to a more delicate situation. We can strengthen 2' further as
follows:

2''. (forall distinct x1,...,xn)(if Arb(x1),...,Arb(xn) then
(phi(x1,...,xn) iff phi(xi1,...,xin))), where x1,...,xn are distinct
variables, and i1,...,in is a permutation of x1,...,xn, and phi is any
formula all of whose free variables are among x1,...,xn.

Here the problem is that Arb may be mentioned in phi.

Nevertheless, one can still show that 1',2'' is conservative over first
order logic with the axiom scheme "there are infinitely many objects", by
an argument using the Galvin Prikry theorem.

LENGTHS OF PROOFS.

What is the comparison between the lengths of proofs of a sentence in first
order logic using 1',2', versus not using 1',2'? Using 1',2'', versus not
using 1',2'?

If there is no FOM posting answering this question, then I will think about it.

Also, what about the speedup issue if we are dealing only with some
interesting fragments of predicate calculus, such as restricting the
nonlogical symbols allowed?

And what other interesting formal issues come up if we take "arbitrary"
objects seriously as a predicate?