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.