4
$\begingroup$

Two papers I have looked at lately axiomatize $n$-th order arithmetic in a single sorted language with predicates $Z_1,\dots,Z_n$ and axioms like $\forall x(Z_1(x)\vee\dots\vee Z_n(x))$ to say everything has one of the orders $1,\dots,n$. Another axiom says nothing has two distinct orders, and another says that if $x\in y$ then $x$ has order one lower than $y$. The axioms use finite disjunctions over the predicates $Z_n$, not quantifiers on $n$. I can type all that out in symbols if people feel it would be helpful.

My question is: are there any technical differences to beware of between such axioms for $n$-th order arithmetic and axioms in an $n$-sorted language with type rules?

The $n$-sorted version immediately translates into the single-sorted. Then, intuitively the axioms on $Z_1,\dots,Z_n$ should be true, but of course they do not follow as translates of anything provable (or even expressible) in the $n$-sorted version. The single-sorted has many sentences not translating naturally into the $n$-sorted, though intuitively those sentences are never true or useful in any way. Is there a more sophisticated translation that I am not thinking of? Or do you somehow prove the untranslatable sentences are irrelevant?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ The only time the difference between the two approaches actually matters is when dealing with structures with infinitely many sorts. The two most interesting - to me - cases of this are $\omega$-sorted logic, with all finite sorts, and the elimination of imaginaries in model theory, where given a structure $\mathcal{M}$ in a language $\mathcal{L}$, we expand to a structure $\mathcal{M}^{eq}$ in a many-sorted language $\mathcal{L}^{eq}$. My limited understanding is that this really is a non-first-order construction, that is, this requires actual sorts and not just a bunch of new predicates. $\endgroup$
    – Noah Schweber
    Mar 29, 2014 at 8:32
  • 1
    $\begingroup$ One subtlety (that fortunately doesn't affect arithmetic theories much) are empty domains and their effect on the behavior of the existential quantifiers. In the usual interpretation of multi-sorted logic, $\exists x^1(x^1 =_1 x^1) \lor \cdots \lor \exists x^n(x^n =_n x^n)$ is not a tautology but $\exists x(x = x)$ is usually a tautology in classical single-sorted first-order logic. It's perhaps best to use free logic or similar when encoding using the single-sorted version, or to relax $\forall x(Z_1(x) \lor \cdots \lor Z_n(x))$ a bit to allow for all domains to be empty. $\endgroup$
    – François G. Dorais
    Mar 29, 2014 at 13:07
  • $\begingroup$ @Noah S: it seems to me that one can interpret $\omega$-sorted arithmetic in all finite types, $\mathsf{PA}^\omega$, into an appropriate theory $P$ with only one sort and an infinite collection of relation symbols, one for each of the original sorts. It is true that some objects in a model of $P$ may not satisfy any of the relations that makes these objects be of one of the original sorts, but the interpretation should still go through. Is there something I am missing? $\endgroup$
    – Carl Mummert
    Mar 30, 2014 at 1:29
  • $\begingroup$ I didn't mean that it can't be done, I just meant that it results, as you said, in some models with "untyped" objects; in contrast to the finite-sort case, where it really is the same as the predicate-symbol case. You're right, of course, though. $\endgroup$
    – Noah Schweber
    Mar 30, 2014 at 1:33

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.