Timeline for $n$th order arithmetic with predicates for orders
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 30, 2014 at 1:33 | comment | added | Noah Schweber | 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. | |
| Mar 30, 2014 at 1:29 | comment | added | Carl Mummert | @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? | |
| Mar 29, 2014 at 13:07 | comment | added | François G. Dorais | 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. | |
| Mar 29, 2014 at 8:32 | comment | added | Noah Schweber | 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. | |
| Mar 29, 2014 at 6:46 | history | asked | Colin McLarty | CC BY-SA 3.0 |