1
$\begingroup$

I am very familiar with the fact that when introducing model theory and the meta theorems describing a formal system, set theoretic notions are inevitably required which we include in the meta theory. My problem is, I believe that the meta theory should only contain what we already know as far as human intuition could capture, without additional axioms or assumptions that would otherwise disregard that idea.

I also believe that we can't just carelessly adopt sets without restriction to avoid introducing the well-known paradoxes; among related posts I've read about attaching ZFC to the meta theory which I think is a standard way of resolving this. I assume that the phrase "treating ZFC (or sometimes, PA) as the meta theory" doesn't refer to the actual first-order theories in their respective formal languages, but rather as mathematics that is formalizable in said theories.

Here's where my problem begins; ZFC is a collection of axioms and talking within ZFC-formalizable mathematics thus requires some sort of informal axiomatic approach to lay out the desired restrictions. This is also very evident in Paul Halmos' famous book Naive Set Theory. A couple ways I could think around this is that the axioms are self-evident and aren't necessarily assumptuous (which is how I would always describe axioms), and secondly, that axioms could be replaced by definitions (which really are implicit axioms, but I feel more comfortable with definitions nonetheless), but I'm not entirely sure how this is done for axiom of pairing, replacement, and choice which are relevant when dealing with ordinals. Thank you in advance.

|cite|improve this question
$\endgroup$
  • $\begingroup$ We cannot solve the chicken-and-egg problem... But it is Worth to note that the theory of Hereditarily finite sets is enough for meta-theory. $\endgroup$ – Mauro ALLEGRANZA Jun 12 at 6:02
  • $\begingroup$ @Mauro ALLEGRANZA I used to struggle with the chicken-and-egg problem but I wouldn't fully agree. If you mean it in the sense that it is indeed impossible to fully develop first-order logic without set theory, then you're correct. I look at it differently and treat the informal set theoretic apparatus used to develop FOL and its formalized version as two completely different objects; ZFC set theory is technically just a mere bunch of strings in a formal language. My concern is that we want the informal set theory to be paradox free and it means we'll have to take an axiomatic approach. $\endgroup$ – mjtsquared Jun 12 at 7:53
  • $\begingroup$ @mjtsquared I’m not sure I understand your concern. Yes, we should axiomatize the metatheory, but then in what sense is it informal? Why does it need to be informal, why can’t it just be ZFC? $\endgroup$ – spaceisdarkgreen Jun 12 at 15:28
  • $\begingroup$ @spaceisdarkgreen It’s informal in the sense that we don’t axiomatize it in a formal system, because we use it to talk about the formal system. Thing is, as I’ve seen in a lot of posts, some people (incl. me) adopt a particular view wherein the (informal) set theory used to develop FOL is different from the set theory (ZFC) formalized in FOL to avoid the uncomfortable circularity and my concern leans more on whether this “informal” set theory might not be paradox free unless we turn it into some kind of informal treatment of ZFC. Doing so means we have to sort of, axiomatize it similar to ZFC. $\endgroup$ – mjtsquared Jun 13 at 1:18
  • $\begingroup$ For instance, the Lowenheim-Skolem thorem requires a notion of infinite cardinals; constructing maximal sets requires a notion of countability; soundness theorem assumes the principle of mathematical induction. It is indeed ZFC set theory in the meta theory, but not its formal version in a formal system itself, but rather in the sense that it’s mathematics that can be formalized in ZFC. My concern is that doing this doesn’t kind of feel right, since it means that the said metalogical properties are true only within the theory, namely a bunch of hypothesis, and not universally. $\endgroup$ – mjtsquared Jun 13 at 1:29
3
$\begingroup$

I think this question has multiple aspects, some of which are fundamentally hard to address. However, I believe the following will be useful for the pragmatic aspect:

What sorts of commitments do we actually need in the metatheory to develop model theory in a satisfactory way?

In particular we want to measure two things, one subjective and one technical:

  • Naturality: To what extent can we get away with using only "what we already know as far as human intuition could capture"?

  • Consistency strength: How can we maximize our confidence in the consistency of the system we adopt?

Note that naturality is no guarantee of confidence a priori - per the collapse of naive set theory, this is a distinction we need to recognize.

Before diving in to my answer proper, let me give some good sources (since there's a ton of really interesting material here):

  • For fragments of Peano arithmetic: Metamathematics of first-order logic by Hajek and Pudlak.

  • For theories of second-order arithmetic, that is, reverse mathematics: Subsystems of second-order arithmetic by Simpson. (Only the first chapter is freely available, but it's really good and has lots of "meat" - and quite frankly it's a much more fun read than the rest of the book, which is fairly technical).

  • For weak set theories (= vastly weaker than ZFC): Mathias' amazing paper The strength of MacLane set theory (although it's very technical; I'll add a less technical source if I can find one).

Additionally, you may become interested in theories stronger than ZFC or extremely weak theories of arithmetic; for these I recommend The higher infinite by Kanamori (of which only the introduction is freely available, but again it's still quite good) and Bounded arithmetic by Buss, respectively.

So first let's think about what we really need for model theory. The key principles are:

  • Reasoning about syntax.

    • Essentially this corresponds to a "strong enough" theory of arithmetic. The most natural of course is Peano arithmetic, but in fact we can do much better: the very weak fragment I$\Sigma_1$ (basically, PA with induction restricted to "very simple" formulas) suffices, and is of drastically weaker consistency strength than PA. In particular, there is a hierarchy I$\Sigma_n$ ($n\in\mathbb{N}$) of fragments of PA; PA is the union of these fragments, and for each $n$ the theory I$\Sigma_{n+1}$ proves the consistency of the theory I$\Sigma_n$.

  • Defining structures.

    • In order to talk about structures, we need to work with theories in a broader language - at the very least, the language of second-order arithmetic (= natural numbers and sets of natural numbers; contra the name, the theories in this language we'll consider will be first-order theories, just as how ZFC is a theory considering arbitrary sets but is still first-order). This is a perfectly satisfying framework for treating theories in a finite language, which is fine for the meta-theory (there's a bit to be said here, but for now take it on faith).

Our paradigm will be: we'll want a theory in the language of second-order arithmetic, but we'll measure its consistency strength by looking at its "first-order fragment" (which is consistent iff the original theory is), since theories of first-order arithmetic are more natural in my opinion.

  • Model existence and Tarskian truth.

    • This is where real strength creeps in. There are three key things we want: the soundness theorem, the completeness theorem (from which follows the compactness theorem), and what I'll call "Tarski's theorem" - the fact that for every structure $\mathcal{M}$ and every sentence $\varphi$ either $\mathcal{M}\models\varphi$ or $\mathcal{M}\models\neg\varphi$. These turn out to correspond to three very natural theories of second-order arithmetic: RCA$_0$, WKL$_0$, and ACA$_0$. RCA$_0$ and WKL$_0$ are conservative over I$\Sigma_1$: if I$\Sigma_1$ is consistent then so are each of them (and PRA, a theory far weaker than I$\Sigma_1$, can prove this). ACA$_0$, however, is much stronger: its first-order arithmetic part is PA. So we can only believe that ACA$_0$ is consistent if we believe that PA is consistent. Fortunately, that's not too controversial in my opinion.

This is how, then, I'll sum up the situation:

ACA$_0$ forms a satisfactory context for developing model theory. Moreover, it's conservative over PA (and this is provable by an uneblievably weak theory), which is an extremely natural theory of very low consistency strength.

This leaves open of course the naturality question: while we've succeeded in tying its consistency to that of an extremely natural theory, that doesn't mean that the theory itself is natural. So at this point I want to present the theory ACA$_0$. It consists of:

  • The ordered semiring axioms for the natural numbers, and the extensionality axiom for sets.

  • The induction scheme for formulas without set quantifiers (but allowing individual set parameters).

  • For each formula without set quantifiers (but again allowing individual set parameters), the set of numbers satisfying that formula exists.

And that's it! The prohibition of set quantifiers in induction and comprehension (= set formation) can be thought of as a kind of skepticism towards the set of all sets of numbers; this is in my opinion a pretty reasonable skepticism to have. In particular, ACA$_0$ doesn't think that the powerset of $\mathbb{N}$ is actually a thing. In my opinion, ACA$_0$ amounts to exactly the set-theoretic commitments that grow naturally out of a commitment to Peano arithmetic, and is quite natural indeed (if a bit technical to state precisely).

Now there's an obvious missing point in the above analysis: **what about the downward Lowenheim-Skolem theorem? That doesn't even make sense in the context of second-order arithmetic, so we've completely missed out on it.

The point is that the second-order arithmetic approach adopts a very strong ontological skepticism. It can talk about talking about uncountable objects - e.g. ACA$_0$ can prove "Every model of ZFC satisfies the downwards Lowenheim-Skolem theorem - but it itself doesn't consider them actual objects. By contrast, it really views the soundness, completeness/compactness, and Tarskian truth theorems as genuinely correct. I would consider this a satisfactory situation.

If you don't, though, we wind up climbing a bit higher in the consistency strength hierarchy. The weakest natural theory in my opinion which proves the downward Lowenheim-Skolem theorem is KP (+ Inf). The consistency strength of this theory is stronger than that of ACA$_0$, but not too much stronger: KP is consistent relative to ATR$_0$, a theory in second-order arithmetic which is well-studied in reverse mathematics (it's one of the "Big Five" - in increasing order of strength these are $$\mbox{RCA$_0$ < WKL$_0$ < ACA$_0$ < ATR$_0$ < $\Pi^1_1$-CA$_0$}.$$

(I can't remember whether ATR$_0$ proves the consistency of KP+Inf, though.)

But maybe you think KP+Inf is still too weak - after all, it can't prove that uncountable sets exist. For that we probably want powersets, and at this point we wind up with Zermelo set theory Z (or ZC = Z + Choice, if we prefer) or one of its fragments. The difference between Z and ZF is that Z doesn't have the axiom (scheme) of replacement; this makes it much, much weaker than ZF, even in terms of consistency strength.

At this point the only real thing we're missing is transfinite recursion, and this is exactly the replacement scheme - that is, Z(C) + Replacement = ZF(C). And that's a good stopping point on the ladder (although we can keep going).

A final mention should be made about choice: although it's arguably quite counterintuitive, it doesn't yield an increase in consistency strength over Z or ZF: if Z is consistent then ZC is consistent and if ZF is consistent then ZFC is consistent. The latter is quite well-known (Godel proved this via inner models); for the former (and information on weak set theories in general), see Mathias' paper mentioned earlier.

|cite|improve this answer
$\endgroup$

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.