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
    Commented 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
    Commented 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
    Commented 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
    Commented Mar 30, 2014 at 1:33

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .