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?

  • 2
    $\begingroup$ Every formula is equivalent to one in "prenex normal form", i.e., with all the quantifiers at the beginning. The closed subformulas are then all atomic sentences, which (in ZFC or Peano Arithmetic) can be systematically removed. So every "defining formula" can be written, in ZFC or Peano Arithmeic, in such a way that there are no closed subformulas. $\endgroup$ – Sidney Raffer Jul 24 '10 at 21:52
  • $\begingroup$ Ah, nice! Much slicker than how I did it. I've been working in constructive logic so much recently that I tend to forget about prenex normal form and all the other useful tools available in the classical case :-) $\endgroup$ – Peter LeFanu Lumsdaine Jul 24 '10 at 22:03
  • 1
    $\begingroup$ @jeq yet another trifling edit made to a question that was asked and resolved over two years ago. What, pray is being achieved here? $\endgroup$ – Yemon Choi Jul 9 '13 at 2:54

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!)

  • $\begingroup$ On a strictly formal level, you solve the problem. But doesn't this just show that the question is maybe posed in the wrong way? After all, you are just introducing dummy variables to avoid closed formulas. $\endgroup$ – Stefan Geschke Jul 25 '10 at 12:47
  • $\begingroup$ Yes, agreed. But I'm not quite sure what would be a way to refine the idea behind this question… I think what these approaches both show (mine and SJR's prenex-n-f approach) is that “has no closed subformula” won't be an interesting property in any context where we only care about formulas up to equivalence. (So it could be interesting from e.g. a re-writing theory point of view, or something.) $\endgroup$ – Peter LeFanu Lumsdaine Jul 25 '10 at 16:42

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.