3
$\begingroup$

The locus classicus of this theorem (the ''reflexivity'' of PA) is Mostowski's 1952 On models of axiomatic systems. I freely admit that I can't read the rather archaic formalism of this paper. Is there a more accessible, modern source where this theorem is proven? Or alternatively, does somebody know the proof, and would like to carry it out here? Furthermore, can the theorem be formally reproduced inside PA? I.e., can PA itself verify that it verifies the consistency of each of its finite sub-theories?

Many thanks in advance.

$\endgroup$
2
$\begingroup$

This is a somewhat standard result. One way to approach it is:

  • Stratify the induction scheme into a sequence $I\Sigma_n$ of stronger and stronger schemes. For each $n$ the scheme $I\Sigma_n$ includes induction for $\Sigma_n$ formulas only.

  • Show that $I\Sigma_{n+1}$ (and thus PA) proves the consistency of $I\Sigma_n$ for each $n \geq 0$. A proof of this is sketched on page 140 of Kaye's Models of Peano Arithmetic. The proof uses a universal $\Sigma_n$ formula, also known as a "truth predicate" or "partial truth predicate". This method is also used to show that each scheme $I\Sigma_n$ is itself finitely axiomatizable, for $n \geq 1$, as sketched by Kaye on p. 134. The construction of a universal $\Sigma_n$ formula is standard, but tedious. Kaye's book has the details.

  • Because there are only a finite number of non-induction axioms on PA, every finite subtheory of PA is included in $I\Sigma_n$ for some $n$. Hence PA proves the consistency of each of its finite subtheories.

The overall results

  • "for all $n$, $I\Sigma_n$ is consistent" and
  • "every finite subtheory of PA is consistent"

cannot be proved in PA, because PA proves "If every finite subtheory of PA is consistent then PA is consistent", because given a derivation of $0=1$ in PA the finite subtheory consisting of only the axioms used in that derivation will also be inconsistent.

$\endgroup$
  • 1
    $\begingroup$ Now I'm happy - +1. $\endgroup$ – Noah Schweber Mar 25 at 15:47
  • 1
    $\begingroup$ I've turned my comments into an auxiliary answer - let me know if there's a point in it I can improve. $\endgroup$ – Noah Schweber Mar 25 at 15:55
  • $\begingroup$ Brilliant, thank you very much! It was in fact precisely my having read about "partial truth predicates" that lead me to ask this question. Your answer provides me with exactly the right explanations and references (Kaye's Models is on the desk). Accepted. $\endgroup$ – mar_cel Mar 25 at 17:13
  • 1
    $\begingroup$ Would you mind explaining the second point in a bit more detail? The key seems to be that whenever a $\Sigma_n$ formula is provable from $\Sigma_n$ induction, then it has a proof that goes through only $\Sigma_n$ formulas. Why is this true? $\endgroup$ – mbsq Mar 25 at 21:39
  • 1
    $\begingroup$ @mbsq: the key method is controlled cut elimination. The main way unexpected formulas get into proofs is through cuts. Kaye's method is: first, work in a natural deduction proof system, and reformulate the induction scheme as a set of inference rules. Second, prove a kind of cut elimination theorem showing that for each provable theorem there is another proof that only uses cuts in a particular controlled way. Third, use that cut elimination theorem to show there is a derivation in which every formula is $\Sigma_n$. $\endgroup$ – Carl Mummert Mar 25 at 22:03
1
$\begingroup$

A quick comment building on Carl's answer:

While - as Carl says - PA does not prove

$(*)\quad$"For all $n$, $I\Sigma_n$ is consistent,"

I believe PA does indeed prove

$(**)\quad$"For all $n$, PA proves that $I\Sigma_n$ is consistent"

just by checking that the usual proof goes through in PA with a bit of care re: how we talk about models, which PA can't actually directly handle. This is of course a nontrivial task; I'll put in a reference to it when I have time to find it (but see below).

These two facts aren't in contradiction: perhaps surprisingly, theories rarely prove that provability implies truth!


Above I kind of punted on the issue of whether $(**)$ is in fact true. It is however quite easy to show that $(**)$ is plausible, as follows:

Define a sequence of theories $(T_i)_{i\in\mathbb{N}}$ recursively as $$T_0=PA, \quad T_{i+1}=T_i\cup\{Con(F): F\subseteq_{fin} T_i\}$$ (where "$X\subseteq_{fin}Y$" means "$X$ is a finite subset of $Y$"). Let $T=\bigcup_{i\in\mathbb{N}}T_i$; then $T$ is recursive and (by induction) sound. But clearly $T$ proves that $T$ proves the consistency of each of its finite subtheories.

  • Incidentally, the soundness of $T$ can be proved from the soundness of PA (in an appropriately weak base theory). So the "soundness strength" of $T$ is no greater than that of PA.

So even before we check whether the specific theory PA proves its own reflection, we can quickly show that a theory "very similar" to PA has this property. In particular, no "coarse" argument will show that PA doesn't prove that PA has the reflection property.

$\endgroup$
  • 1
    $\begingroup$ I think that it does seem plausible to just formalize the entire argument that Kaye gives inside PA. The argument is a combination of a cut elimination lemma, which Kaye indicates is provable in $I\Sigma_1$, and induction on the universal $\Sigma_n$ formula. So I don't see any immediate obstacle, although checking the details would take a while. $\endgroup$ – Carl Mummert Mar 25 at 16:09
  • 1
    $\begingroup$ @CarlMummert Oh, I remembered there being some model theory - if not, then yeah, it shouldn't take any cleverness at all. $\endgroup$ – Noah Schweber Mar 25 at 16:10
  • $\begingroup$ Any idea how the choice of terminology "reflexive"/"reflection" comes about? Reflection principles like bew(x) --> x are not immediately related, are they? BTW thank you for this helpful elaboration on Carl's answer! $\endgroup$ – mar_cel Mar 27 at 7:22

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.