# Do the proofes in set theory rely on the semantics of the formulas used in the axioms?

Motivation: The Axiom of separation

$$\forall w_1,\ldots,w_n \, \forall A \, \exists B \, \forall x \, ( x \in B \Leftrightarrow [ x \in A \wedge \phi(x, w_1, \ldots, w_n, A) ] )$$

is used to guaranty the existence of subsets by constructing formulas $\phi$ which, I assume, say true or false for every element you want in the subset or not. Then these subsets get used to construct proofs of whatever theorem. If you use formulas with other true/false values, you will get another subset.

Do the proofs in set theory rely on the semantics of the formulas used in the axioms?

Another elaboration from the comments (edit): I make a decision on what makes a specific subset (say the odd numbers in the natural numbers) by $\phi$'s which say yes and no to all elements in questions (say natural numbers here). I thereby constructed the subset (odds). Now I proof some theorems about said subset. And now if I then change if the $\phi$'s say yes or no afterwards, I'll get another subset out of it (not the odd numbers (anymore)). My question is if then automatically invalidates all statements/theorems made before. Semantics seem to decide what a set really is.

So again: If I suddently decide to rechange which $\phi$'s said yes/no (that's what I mean by dependence on semantics), can I still carry over theorems from set theory? And to what extend to proofs in set theory rely on semantics in general?

-
Your question is unclear to me. – Asaf Karagila Apr 20 '12 at 23:21
That's a vague statement too :) What I ask is: If I suddently decide to rechange which $\phi$'s said yes/no (that's what I mean by dependence on semantics), can I still carry over theorems from set theory? – NikolajK Apr 20 '12 at 23:23

Both of "rely on" and "semantics" are somewhat fluid concepts, but with assuming that we understand them in the most straightforward way: No, formal proofs do not rely on semantics.

Your elaborated question is a bit hard to understand because it is unclear what you mean by "change if the $\phi$'s say yes or no afterwards". There are several different interpretations one could give that:

If you mean that you decide to use a different formula instead of the $\phi$ you originally used, then naturally the proofs you've already constructed are in grave danger of becoming invalid. These proofs are full of $\phi$s -- or perhaps we should clarify what that means, because formal proofs do not really contain the letter "$\phi$". Instead there's some particular sequence of symbols in the language of set theory (such as "(", "$x$", "$y$, "$\neg$", "$\in$", "$\forall$" etc. but not "$\phi$") which appears at various places in the proof, and which, for our own convenience, we choose to call $\phi$ when speaking about the proof.

Now, deciding to use a different formula would amount to seeking out all occurrences of that sequence of symbols in the proof and replace it by a different sequence of symbols. But that is very unlikely to yield a valid proof, because there are probably (except in trivial cases) steps in the proof whose validity depend on the internal structure of $\phi$. For example, if your old $\phi$ had the form $\psi_1\to\psi_2$ (for some formulas $\psi_1$ and $\psi_2$), then there might well be a step in the proof that concludes $\psi_2$ from $\psi_1$ and $\phi$. However, when you replace $\phi$ by $\phi'$ in the proof, that replacement is not going to affect the hypothesis $\psi_1$ or the conclusion $\psi_2$ of that step, because the replacement only does something for the entire sequence of symbols that is $\phi$. And then suddenly you have a purported proof step that concludes $\psi_2$ from $\psi_1$ and $\phi'$, where the new $\phi'$ may have nothing to do with $\psi_1$ or $\psi_2$. Which makes the proof invalid, as a matter of pure syntax.

(Of course one may try to find appropriate substitutions for $\psi_1$ and $\psi_2$ that would make the substituted proof still work, but then what we're really doing is to attempt to adapt the proof rather than continuing to believe in the same proof).

Or perhaps by "change if the $\phi$'s say yes or no" you mean that you keep using the same formula but somehow cause it to have a different truth value? Then of course the syntactical integrity of your existing proofs is unharmed -- but the question instead arises: what is it actually that you imagine doing in order to cause the same $\phi$ have different truth values? This must depend on how you view the semantics of set theory:

If you're a set-theoretic Platonist, you believe that sets have some kind of independent extrinsic existence, and that the purpose of formal proofs is to discover facts about them that were already true, independent of any notion of proof. However, I don't think you're a Platonist, because that would leave you no room to do anything to make $\phi$ mean something different. As before, $\phi$ is some particular sequence of symbols, and each of those symbols already has a definite semantics -- that of "$\neg$" and ")" are given by the rules of propositional calculus, "$\in$" is fixed by what sets are, and the meaning of "$\forall$" is fixed by which sets actually exist (remember, in this paragraph we're pretending to be Platonists), etc.

So we're probably not Platonists. But then the only avaiable way to speak about whether $\phi(x)$ is "true" or not appears to be model theory. In model theory we can speak of an interpretation of the language of set theory, which is the combination of a class of "things" that the variables of set theory range over, and some definite way to decide whether the "$\in$" relation holds between two given "things". Having an interpretation gives a truth value for every (well-formed, closed) formula -- the meaning of "$\forall$" and "$\in$" come from the interpretation itself, and the meanings of all other symbols are fixed by the rules of model theory itself.

In this framework you can indeed change what your $\phi$ means, simply by choosing to consider one interpretation (of the entire language of set theory) rather than another. Will your old proofs still work after the change? Yes they will, provided that you're only considering interpretations where every axiom used in the proof is true. That is the core "soundness" property of first-order logic: If you have a valid formal proof using certain axioms, then in every model where those axioms are true, the conclusion of the proof also happens to be true in that interpretation.

However, of course, if you decide to use an interpretation that doesn't make the axioms true, then all of your proofs from those axioms become irrelevant.

-
Have you read my answer and the discussion followed it in the comments? I think that your answer is a very good complement to that and at least the way I read it - it conveys my point better. – Asaf Karagila Apr 21 '12 at 12:33
@Asaf: Yes; my answer is somewhat informed by the (now deleted) comment thread. You raise interesting points about proof "molds", such as interchangeable implementations of ordered pairs. I think one could formalize that fairly well in second-order logic: Formally prove as a lemma something like $(\exists f)(\forall x,y,w,z) f(x,y)=f(w,z) \leftrightarrow (x=w\land y=z)$, and then make that an explicit assumption of everything that speaks about pairs. – Henning Makholm Apr 21 '12 at 12:52