I've started reading Model Theory: An Introduction by Marker. I'm not sure whether it covers multi-sorted languages. It seems that it doesn't. So, the question is whether there is something I could read on the topic and whether multi-sorted model theories make sense.
-
2$\begingroup$ Multi sorted languages are no issue at all in model theory. Though they can make notation awkward in abstract treatments. My advice: learn (the basics of) the single sorted approach first and it will be very easy to adapt to the multi sorted approach. Chances are you will even see yourself how to do it! $\endgroup$– Mark KamsmaCommented Nov 6, 2023 at 17:01
-
$\begingroup$ @Mark Kamsma, I could simulate multi-sorted languages by introducing a relation symbol for each sort. What do you think about that? But the question is whether there is a special formalism that addresses specifically multi-sorted languages. $\endgroup$– SeekerCommented Nov 6, 2023 at 17:19
-
2$\begingroup$ That is indeed a popular way of showing that you can 'encode' sorts in a single-sorted framework. This works perfectly fine. However, this approach has some minor issues if you need infinitely many sorts (by the compactness theorem you would get elements that live in none of the sorts). Another approach is simply checking that all the definitions and results go through straightforwardly for the multi-sorted approach... $\endgroup$– Mark KamsmaCommented Nov 6, 2023 at 17:32
1 Answer
As Mark Kamsma says in the comments, the traditional approach is to learn the basics of model theory in a single-sorted context, and then at some point observe that "everything generalizes" to the multi-sorted context. This is basically correct (see this related question and its answers), but it may seem a bit unsatisfying.
I once taught a class on basic model theory in which we used multi-sorted logic (and allowed empty structures and empty sorts) from the beginning. This included setting up a proof system for multi-sorted first-order logic (with empty sorts allowed) and proving the completeness theorem. My lecture notes are available here. I'm not sure this is the most pedagogically sound approach - I mostly did it this way because I wanted to work through the details for myself at least once.
Since you ask about Marker's book: it (very briefly) introduces multi-sorted logic on p. 28, in the section "Multi-sorted Structures and $\mathcal{M}^{\mathrm{eq}}$". Most of the book implicitly works in the single-sorted context, but occasionally (especially in Chapters 6-8 on stability theory), it is useful to work in the multi-sorted expansion $\mathcal{M}^{\mathrm{eq}}$, which eliminates imaginaries.
-
$\begingroup$ Thanks a lot, Alex! Your answer has motivated me to continue investigating the subject! $\endgroup$– SeekerCommented Nov 7, 2023 at 14:46