A question about definability in first order theories based upon classical logic

Question

Let T be a theory formalized in the classical first order predicate calculus with equality. If P(x) is a formula of T in which one and only one variable of T--here denoted by 'x'--occurs free, and if the following pair of statements are provable in T, then P(x) is said to be a defining formula of T.

(1) "There exists an x such that P(x)" and 
(2) "For any y and any z, P(y) and P(z) imply y=z"-where "y" and "z" denote variables of T.

Now if T were ZFC, for example, consider the formula of T which states "The continuum hypothesis implies that x is the set of all positive integers and the negation of the continuum hypothesis implies that x is the set of all negative integers". This is a defining formula of T and Sierpinski often used formulae of this type to define sets which were "non-effective" in some way. But many might ask whether such definitions are really "legitimate". They arise when the formula P(x) contains sub-formulae which are sentences of T (i.e. closed formulae in which no variables occur free). My question is, to what extent (if any) would such first order theories as Peano's Arithmetic or ZFC be weakened, if their defining formulae were not allowed to contain sub-formulae that are closed?

Answer 1

Not weakened at all!

In PA and ZFC (and a wide class of other f-o theories), every defining formula is equivalent to one with no closed subformula. Let's start with ZFC. Suppose $\varphi(x)$ is a defining formula, with $x$ free; now let $z$ be any variable not appearing anywhere in $\varphi$, and for each subformula $\psi$ of $\varphi$, define a new formula $\psi^z(z)$ (with all the same free variables as $\psi$, plus $z$) by:

• if $\psi$ is an atomic formula, take $\psi^z\ :=\ \psi \land (z=z)$;
• if $\psi = \top$, take $\psi^z\ :=\ (z=z)$
• if $\psi = \bot$, take $\psi^z\ :=\ \forall z'.\ z \in z'$
• if $\psi = \psi_1 \land \psi_2$, then take $\psi^z\ :=\ \psi_1^z \land \psi_2^z$

…and so on: all the remaining cases (non-nullary connectives and quantifiers) just commute with $(-)^z$, same as $\land$. Anyway, we've defined these new versions of all subformulas; by induction, they all have $z$ free, have no closed subformulas, and are equivalent to the original versions; so up at the top we apply it to our original formula, and have $\varphi^z(z,x)$; now $\forall z.\ \varphi^z (z,x)$ is equivalent to $\varphi(x)$ and has no closed subformula.

Now, this relied on the fact that ZFC has (in most presentations) no closed terms (indeed, no terms except variables), for the atomic formula case to work: in PA, for instance, $0=0$ gets bumped up to $0=0 \land z=z$, which still has a closed subformula. So for eg PA, we have to work a bit harder at defining that case:

• for $\psi$ an atomic formula $R(t_1,\ldots,t_n)$, take $\psi^z\ :=\ \exists w.\ [w = t_1\ \land\ R(w,\ldots,t_n)\ \land\ z=z]$.

This now makes it all work again! But, this relied on all basic relations $R$ taking at least one argument. In any language with this property, we're good. The one thing we can't generally deal with is theories with nullary relation symbols, aka propositional constants — although we can sometimes still handle them like we handled $\top$ and $\bot$ in $ZFC$.

(Actually, I'm not quite sure what you mean by “how would ZFC and PA be weakened if we changed the definition of a defining formula” – since I don't know axiomatisations of those theories that involve this term. But the standard axiomatisation of ZFC does involve functions (in the replacement axiom), which are just defining formulas $f(x,y)$ with an extra free variable $y$, so I guess what you have in mind might be something like strengthening the definition of function allowed in there? But I think the above construction should answer the question, in any case!)

Answer 2

This seems to be vaguely related to a question that I am now unable to find, about theorems that have proofs from an unproved conjecture and from the negation of this conjecture. There are statements that follow from the Riemann Hypothesis and from its negation, showing that these statements are simply true, no matter whether the Riemann hypothesis is true or not. I have no idea whether such statements necessarily have proofs that avoid formulas with closed subformulas.

I recall the construction of an example in general topology that is the disjoint union of two spaces, the first providing the desired properties if CH fails, the other if CH holds. So even if I can't answer your question completely, at least it seems that some existing proofs make substantial use of objects with defining formulas that have closed subformulas.