What does a proof that $\mathcal{N} \models PA$ (where $\mathcal{N}$ is the structure $($$\mathbb{N}$ $, 0, 1, S, +, \times, \leq)$, $\models$ is the satisfaction relation, and $PA$ is first-order Peano arithmetic) look like? By which I mean, what machinery is used in whatever meta-theory is being used for this proof? If Tarski's undefinability theorem says that a theory (with sufficient arithmetical power) can never define the truth of its own formulas and we need a meta-theory to handle that task, how does the meta-theory handle that task?

I have seen it said that systems much weaker than $PA$ can be used as the meta-theory for these results, e.g. primitive recursive arithmetic. How does $PRA$ prove that $\mathcal{N}$ is a model of $PA$, when $PA$ is much stronger than $PRA$? What aspect of $PA$ allows it to prove $V$ is a model of $ZFC$? I can only assume it's done through Gödel coding, what exactly is being encoded?

I understand that an interpretation is a tuple $<D,F>$ where $D$ is a domain of individuals ands predicates/functions and $F$ is a function that maps each member of $D$ to the syntactic objects of whatever theory is being talked about (which means that the interpretation is a meta-object, correct?). How, then, does $PRA$ prove "$<$($\mathbb{N}$ $, 0, 1, S, +, \times, \leq), F>$ correctly satisfies PA"? Or to get more to the point of my confusion, how does PRA assure that "when $F$ interprets the sentences of PA with $($$\mathbb{N}$ $, 0, 1, S, +, \times, \leq)$, there is never a sentence that is interpreted falsely" when $F$ is chosen correctly? Wouldn't $PRA$ need to prove either a statement about an infinite object, which it cannot do, or an infinite amount of things for this to be the case? Is this getting into Hilbert's idea of a finitary proof and an example of the impossibility of what he wanted?

Intuitively, I believe that $($$\mathbb{N}$ $, 0, 1, S, +, \times, \leq)$ does satisfy $PA$ under a proper assignment, but that is only because I have seen it said many times that PA captures the correct notions of arithmetical addition and multiplication and because of my (innate and naively platonistic) belief that $\mathbb{N}$ exists and arithmetic is well defined. By which I mean, I do not believe it because I have seen the mechanics of a formal proof that $\mathcal{N} \models PA$, and that is what I would ultimately like to see. To paraphrase, my justification for why I believe $($$\mathbb{N}$ $, 0, 1, S, +, \times, \leq) \models PA$ is because of inductive (real induction, not mathematical) reasons and not deductive reasons, and I would hopefully like to see a deductive proof.

This question is motivated by my confusion about what exactly is allowed to happen and does happen in a meta-theory, and I used a lot of individual questions to try and outline my specific confusion. That being said, I really don't want this question to be closed for asking multiple questions, especially because it isn't actually. So I'll reiterate that the real question that I'm asking is the same as the question in the title:

What does a proof (in, for example, $PRA$) that $\mathcal{N}$ is a model of $PA$ look like?

  • $\begingroup$ How are you defining $\mathbb N$ and the operations on it? $\endgroup$ – Mark Bennet Mar 30 '18 at 9:17
  • $\begingroup$ @MarkBennet I did use an abuse of notation (only putting the domain and not the constants/functions/predicates) a few times but further down I'm pretty explicit that I am talking about the standard model of $PA$ which we all intuitively agree means what we learned in elementary school about counting numbers and basic arithmetic. $\mathbb{N}$ is the set of natural numbers, $0$ is zero, $1$ is one, $S$ is the successor function, $+$ is the addition function, $\times$ is multiplication, and $\leq$ is less than or equal to. $\endgroup$ – user462082 Mar 30 '18 at 10:10
  • $\begingroup$ This question seems to be based on the false idea that PRA proves $\mathbb{N} \models PA$. I think it may help if you go back to clarify for yourself what that theory PRA actually is, and what kinds of things can be expressed in it. It would also help, when writing the question, if you give an explicit source for things you claim others say - the second paragraph is not very clear. The fourth paragraph also doesn't really contribute towards the question, and that kind of paragraph is more likely to lead to closure than having multiple subquestions. $\endgroup$ – Carl Mummert Mar 30 '18 at 11:05
  • 2
    $\begingroup$ Just to remove two misconceptions: PRA cannot even express that $\mathcal N\models\text{PA}$, let alone prove it. PA cannot even express that $V\models\text{ZF}$, let alone prove it. $\endgroup$ – Andreas Blass Mar 30 '18 at 12:35
  • $\begingroup$ Yes my confusion was between relative consistency proofs and satisfaction proofs, I think that my main issue is that both of them are meta theoretic and people are often vague when they say things about this. For example, in Professor Hamkins' answer to this question he says explicitly "The main fact is that a very weak meta-theory typically suffices, for theorems about models of set theory." This is vague and misleading if what everyone has said here is true. $\endgroup$ – user462082 Mar 30 '18 at 23:05

To prove that any model $M$ is a model of PA, in the usual sense of "model of PA", you have to work in a metatheory that has the ability to form the satisfaction relation $\models$ for $M$. Otherwise, the metatheory can't express "is a model".

Compare this outline of how ZFC set theory proves that $\mathbb{N} \models \text{PA}$. First, we can use ZFC to form the satisfaction relation $\models$ for $\mathbb{N}$. Second, we look at how $\mathbb{N}$ is defined in ZFC to see that the satisfaction relation thinks that all the basic axioms are true. Finally, we again use the way that $\mathbb{N}$ is defined in ZFC to show that it satisfies each of the induction axioms of PA. This fact that ZFC proves $\mathbb{N} \models PA$ also leads quickly to the theorem that ZFC proves PA is consistent.

Weak theories like PRA do not have enough strength to even talk about satisfaction relations, much less construct them. So, in PRA, we cannot directly express a relation such as $\mathbb{N} \models \phi$. Moreover, we know that PRA does not prove that PA is consistent, so we know there will be some real limits on how much we can prove about PA in PRA.

PRA is mostly useful as a metatheory when we are working syntactically, looking at proofs instead of models. In that situation, although PRA doesn't prove the consistency of many theories, it can prove the relative consistency of many pairs of theories, e.g $\text{PRA}\vdash \text{Con}(\text{ZFC})\to\text{Con}(\text{PA})$. PRA is also strong enough to prove formalized versions of Gödel's incompleteness theorem and Tarski's undefinability theorem - both of which, in the end, are about provability. But PRA can only do so much, because it is an extremely limited theory.

Similarly, PA cannot express what it would mean for the set theoretic universe to model ZFC. PA has no way to define the satisfaction relation $\models$ for $V$. Even ZFC itself can't do that. But, more generally, PA is not able to talk about sets or models in the way that we talk about them in introductory logic.

For metatheoretic results involving models, the easiest metatheory to work in is ZFC set theory. Occasionally we need to look at stronger systems, but only when we look at the metatheory of set theory itself. Occasionally we work in weaker, intermediate systems, but these are mostly of technical interest.

| cite | improve this answer | |
  • $\begingroup$ Can you give me examples of references where these are actually worked out and not just sketched? One of the reasons for my confusion is because people would say things like your second paragraph but never actually work it out, (I don't have a concrete idea of what " First, we can use ZFC to form the satisfaction relation ⊨ for ℕ" means, only a vague idea). Could you give me a reference that shows a working through of a relative consistency proof and one of a proof in ZFC that $\omega$ satisfies ZFC's interpretation of the PA axioms? $\endgroup$ – user462082 Mar 30 '18 at 22:57

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.