2
$\begingroup$

First-order Peano arithmetic has no non-logical symbols other than S, +, *, < and variables. One allows finite quantification over predicates such as: $\forall k<n: \phi(k)$ where $\phi(k)$ is a logical formula containing some non-logical symbol such as Ak. This is because it is understood as a shorthand for $\phi(1)\land \phi(2)...\land \phi(n)$. That way the Ak-s are nothing but n different variables. For example:

$(A_0=1) \land \forall k<3: (A_{k+1} = A_k*(k+1))$

is actually:

$(A_0=1) \land (A_1 = A_0*1)\land (A_2 = A_1*2)$.

This way we can deal with primitive recursive functions.

However, situation is different when moving up in the arithmetical hierarchy. For example, in $\Sigma_1^0$ it is no longer possible to make the above substitution, because the number of variables will now depend on a non-fixed variable on which we quantify in a non-bounded way. Taking the above example, we now have:

$\exists n: (A_0=1) \land \forall k<n: (A_{k+1} = A_k*(k+1))$

which we obviously cannot turn into a formula with no new non-logical symbols.

So my question is: Do we actually allow other non-logical symbols in first-order Peano arithmetic in certain conditions? or do the arithmetical hierarchy formulas actually not belong to first-order Peano arithmetic? or am I missing something?

$\endgroup$
4
$\begingroup$

You are misinterpreting bounded quantifiers.

"$\forall x<y(\varphi)$" is shorhand for "$\forall x(x<y\rightarrow \varphi).$"

Similarly, "$\exists x<y(\varphi)$" is shorthand for "$\exists x(x<y\wedge\varphi)$."

This can be generalized greatly: in any language, for any definable binary relation $R$, we write "$\forall x Ry(\varphi)$" as shorthand for "$\forall x(xRy\rightarrow \varphi)$," etc. For example, expressions of the form "$\forall x\in y$" are common in set theory, and there's a corresponding version of the arithmetical hierarchy in which such expressions are "for free" (similarly to bounded quantification in arithmetic).


Note that the "substitution" interpretation you give breaks down immediately if the model under study is something other than the classical $\mathbb{N}$. Suppose $M$ is a nonstandard model of $PA$, and $c\in M$ is an infinite element. Then how would you interpret "$\forall x<c(\varphi(x))$"?

$\endgroup$
  • $\begingroup$ The interpretations of $\forall x<y$ and $\exists x<y$ might look annoyingly non-dual. To verify that they are reasonable, note that "$\neg\forall x<y(\neg\varphi)$" is shorthand for "$\neg\forall x[x<y\rightarrow \neg\varphi]$," which is equivalent to "$\exists x[\neg(x<y\rightarrow \neg\varphi)]$, which is in turn equivalent to "$\exists x[x<y\wedge \varphi]$" - that is, "$\exists x<y(\varphi)$." The duality is clearer if we write "$\forall x[x\not<y\vee\varphi]$" as the translation of "$\forall x<y(\varphi)$." $\endgroup$ – Noah Schweber Jun 15 '16 at 22:09
  • $\begingroup$ Thanks, but I don't misinterpret, I meant exactly what you wrote. My question was, how can you write such stuff in first-order arithmetic if you're not allowed to add non-logical symbols such as $A_n$ to the syntax? $\endgroup$ – Dani Jun 16 '16 at 4:51
  • $\begingroup$ @Dani : ​ He "can you write such stuff in first-order arithmetic" the way he wrote it in this answer, since he did not attempt "to add non-logical symbols such as $A_n$ to the syntax". ​ ​ ​ ​ $\endgroup$ – user57159 Jun 17 '16 at 20:16
  • $\begingroup$ In fact he did add R, the very same symbol he wanted to define. $\endgroup$ – Dani Jun 17 '16 at 23:32
  • $\begingroup$ @Dani $R$ was just a placeholder, showing how the translation works - I didn't add any symbols. (Saying "$R$ is a definable relation" is shorthand for "$R$ is some formula $\theta$ with two free variables," and "$xRy$" is shorthand for "$\theta(x, y)$".) Your description of how the bounded quantifiers are formally treated is not really correct (although as your answer demonstrates, that wasn't the main focus of your question - I apologize for the misread). $\endgroup$ – Noah Schweber Jun 17 '16 at 23:44
2
$\begingroup$

It turns out that https://en.wikipedia.org/wiki/Course-of-values_recursion is the way to make this possible.

More elaborately, for any quantifier-free formula $\varphi$ one has to create the Goedel number of the formula:

$a_0 = C \land \forall n: a_{n+1} = \varphi(n, a_n)$

where C is some constant (e.g. C could be 1).

Then it can be shown that there is a number and some (other) first-order formula $\psi$ such that:

$\psi(G, 0, C)$

and:

$\psi(G,n,m)$ if and only if, in first order arithmetic to which we add the predicate $a_n$, the recursion formula defined by $\varphi$ implies: $a_n = m$. Thus in proper first order arithmetic (without addition of new predicates) the recursion can be "recreated" by G and $\psi$.

One way to do that is with Goedel's beta function: https://en.wikipedia.org/wiki/G%C3%B6del%27s_%CE%B2_function.

$\endgroup$
  • 2
    $\begingroup$ Of course, it is not necessary to have course of values recursion just to state bounded quantifiers in PA; $(\forall k < n)\phi(k)$ is defined to be an abbreviation for $(\forall k)[k < n \to \phi(k)]$, which is already a formula in the language of PA. Course-of-values recursion is useful to see that if $R(m)$ is a primitive recursive predicate then so is $(\forall k < n)R(k)$, but that is not really about formulas of PA, it's about primitive recursive functions. Every formula of the arithmetical hierarchy is already a formula of Peano arithmetic. $\endgroup$ – Carl Mummert Jun 20 '16 at 0:32
  • $\begingroup$ The first sentence is indeed not in place. Also, obviously every formula of the arithmetical hierarchy is already a formula of Peano arithmetic by definition. The point of my question was how can functions of certain kinds be defined in PA. Once one shows that for primitive recursive functions, course of values recursion can be used to show this holds for functions defined in a somewhat more general way. $\endgroup$ – Dani Jun 20 '16 at 17:06

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.