I recently saw the proof of the independence of ZF (with allowance for multiple empty sets) and AC. The proof constructed the model based on a set theory generated by infinitely many empty sets and then restricted this model to those with a hereditary finite basis (HFB). However, this model did not seem to conform to my intuition about set theory. Rather, it seemed like an odd construction which is not what I think of as the theory of sets, yet which did in fact formally satisfy all the axioms of ZF as well as negation of AC. Although we may have proved that the ZF axioms do not imply choice, I do not feel at all convinced that AC does not have to be true in set theory. Rather, although what I'm about to say is imprecise, I feel that in any model of set theory which is actually like our intuitive notion of set theory, AC should be true.
Similarly, at this thead, one constructed a model of arithmetic (without induction) in which $\pi$ is rational. However, I know the integers very well, and even though this model satisfied the axioms of the integers, these were intuitively clearly not the integers.
My question is, I feel that with my of these independence proofs, if you precisely identify the notion we're talking about (like the integers, set theory), then these pathological models don't exist. Maybe it means these axioms aren't sufficient – are there any better sets of axioms? Or maybe it means that we should be focusing on particular models rather than theories in general (as in, a different philosophy of doing mathematical logic)? I'm trying to understand whether there's a way to precise-ify things so that any independence proof we do really shows that something is independent of the actual thing we're considering (not some set of axioms which happen to conform to that thing). This is guided in part by the intuition that if we really know which mathematical object (or collection of objects) we are talking about, then in some sense, any statement should simply either be true or false.
Best Answer
I'm inclined to agree that "if you precisely identify the notion we're talking about (like the integers, set theory), then these pathological models don't exist." The problem is that it's not so easy to precisely identify such structures.
The usual approach to precisely identifying a structure is to write down its essential properties, the axioms governing it. To make use of such axioms, we need to derive consequences from them, and here we find ourselves in a dilemma. On the one hand, there is a perfectly clear notion of logical deduction in the context of first-order logic. On the other hand, the L"owenheim-Skolem-Tarski theorem guarantees that, in the context of first-order logic, there will be unintended models of the axioms (as long as the intended model was infinite). So first-order logic does not accomplish what is wanted.
So let's use second- (or higher-)order logic insterad. (Here you can quantify over subsets of the structure, and those quantified variables are assumed to really range over all subsets, not just, say, definable ones.) Now structures like the integers and the reals can be uniquely specified. But there is no complete deductive system for second-order logic. (More precisely, the set of valid second-order sentences is not recursively enumerable.) Furthermore, the intended meaning of second-order quantifiers depends on the general notion of "set," which is one of the concepts that we were hoping to precisely specify.
So the bottom line, in my opinion, is that, while we might want to build mathematics on the basis of unique specifications of the relevant structures, it simply can't be done, at least not if we want the specifications to contain actual information about the structures (as opposed to just saying "I mean the genuine integers, you know") and to be able to deduce the logical consequences of that information.