Model Theory in the Language of Peano Arithmetic

95 Views Asked by At

Most introductory textbooks on model theory establish the theory based on the ZF set theory (e.g. [1]). In particular, a structure is defined to be a 4-tuple of sets, and so on. In [2], I came to realize that this choice is unnecessary, i.e. the underlying theory ought not be ZF set theory; people suggested there are model theories based on other theories (e.g. Peano Arithmetic (PA), category theory, type theory.. etc).

It would be nice to learn about all those model theories, and about their differences. However, that's going to be too broad so here I specifically hope to start with model theory in PA (1). Please note that I'm not asking about models of PA, but model theory written in PA. A particularly interesting yet basic result is that model theory written in PA cannot prove the consistency of PA (cf this) (2).

By learning (1), I hope to see how a structure can be defined without the notion of sets. By learning (2), I hope to see how one can disprove an statement about "PA/PA" (PA over PA); should we need to work in yet another language X in order to justify that statement (i.e. working in "(PA/PA)/X")?

Could you recommend some good textbooks that explain (1) and (2) rigorously?

2

There are 2 best solutions below

2
On

I hope to see how a structure can be defined without the notion of sets.

Why would you want to do so? I don't think PA is the right theory in which to do model theory. The cornerstone of model theory is Gödel's completeness theorem; its proof certainly doesn't require the full strength of ZFC. If you look at the wiki page of Reverse mathematics, you see completeness theorem (for countable language) is provable in $\mathrm{WKL}_0$, which is roughly speaking a ridiculously weak set theory; in some sense it's even weaker than PA since it has proof theoretic ordinal $\omega^\omega$ while PA has $\varepsilon_0$, but it's still set theory.

That being said, I guess you can do some model theory in PA in an ad hoc way. Exercise I.16.19 in Kunen asks you to give a finitistic proof of the consistency of DTO, the theory of dense linear order without end points; finitistic means you can certainly carry this out in PA. If you look at the proof you are basically building a model of DTO within PA, without explicitly mentioning sets. Using this idea you can also prove in PA the consistency of ACF, RCF, etc.

2
On

$\mathsf{PA}$ isn't a great context for model theory, simply because it can't directly refer to (infinite) models at all. There are a couple ways to get around this:

  • We can work in a conservative extension of $\mathsf{PA}$, such as $\mathsf{ACA}_0$, which can directly talk about at least countably infinite structures and languages. A couple old posts of mine (1, 2) go into some detail on how this plays out.

  • We can work within $\mathsf{PA}$ itself and shift attention from structures to complete theories with the witness property which are definable; e.g., $\mathsf{PA}$ can (state and) prove "Every computable consistent theory in a computable language has a $0'$-computable complete extension in a computable language with the witness property," which can be thought of as the "$\mathsf{PA}$-version" of the completeness theorem. See also the arithmetized completeness theorem.

The real cost of doing model theory in $\mathsf{PA}$ or a $\mathsf{PA}$-adjacent theory like $\mathsf{ACA}_0$ is not the drop in strength but rather expressive power; for example, I don't see any useful way in which $\mathsf{PA}$ can naturally make sense of Morley's theorem ("A countable theory categorical in some uncountable cardinal is categorical in every uncountable cardinal") other than the rather-boring verification in $\mathsf{PA}$ that $\mathsf{ZFC}$ or similar proves Morley's theorem.