I am reading "Extensions of First Order Logic" by Maria Manzano (1996). It develops the thesis that
"[M]ost reasonable logical systems can be naturally translated into many-sorted first order logic. ... All the logic systems treated in this book are put in direct correspondence with many sorted logic, because this logic offers a unifying framework to place other logics. ... Currently [in 1996], the proliferation of logics used in philosophy, computer science, artificial intelligence, mathematics and linguistic makes a working reduction of this variety an urgent issue."
-- Maria Manzano, Extensions of First Order Logic
Interesting, but it's 22 years old! What is the status of this thesis now? Do we have many logic systems that are used in practice, say in computer science, foundations of physics, etc. that cannot be translated into many-sorted logic. Also, does this thesis say that we could also directly use many-sorted logic in these applications or is it that a lot is lost in the translation in terms of convenience. Any reference would be appreciated. Are there more recent books that followed up this thesis? BTW, I have just read the first three chapters and like this book very much. I would love to see the same in a more recent book, perhaps with a different angle.
Here is a link to a pdf document "Eight European Summer School in Logic, Language and Information Reader of Course: Extensions of First Order Logic" that basically contains paste and cut sections of the book. The book has 350 pages, whereas this document has 90 pages, but it maintains the same thesis. In fact, the Introduction is a paste and cut.
Here are some related questions: Henkin vs. "Full" Semantics for Second-order Logic and Multi-Sorted First Order Interpretations, https://mathoverflow.net/questions/105234/second-order-term-in-first-order-logic, advantage of first-order logic over second-order logic .
NOTE ADDED to clarify the question: Here is a quote from the book which provides some idea about the arguments that support the thesis:
Throughout the pages of this book you will find good reasons for wondering whether the philosophy of standard structures is the only possible choice. The reasons are directly related to the following questions:
- Are we satisfied with the limitation on the class of models they require? Would it not be highly instructive to discover new and sensible models for a known existing theory?
- Don’t we feel uneasy about crossing the border with set theory? Don’t second order validities refer to the given set-theoretical environment instead of the logic in itself?
- Do we need all the expressive power they provide?
-- Maria Manzano, Extensions of First Order Logic
The last two (rhetorical) questions point toward the idea that the goal of a logic should not be to talk in details about the background set theoretical environment, the mathematical universe. In other words, a so called interpretation in the mathematical universe is not necessarily the "practical" interpretation that concerns us and thus we should not care about the extra "expressive power" of standard SOL. If, given this extra flexibility, we accept Henkin semantic and thus give up on the (supposedly in practice inexistant) extra expressive power of standard SOL, then, as mentioned in many text books, we have:
In effect, using general pre-structures amounts to treating a second-order language as a many-sorted first-order language.
-- Enderton, Herbert B., in "Second-order and Higher-order Logic", The Stanford Encyclopedia of Philosophy (Fall 2015 Edition), Edward N. Zalta (ed.), URL = https://plato.stanford.edu/archives/fall2015/entries/logic-higher-order/.
Because this last point is well known, it is not the subject of this question. The thesis that is the subject of the question is whether we are OK in practice to give up the extra expressive power and other semantic properties of standard SOL? In that sense, is really many-sorted logic a unifying logic?
SECOND NOTE ADDED. Here is an excerpt of the abstract of a paper that was suggested to me by @Carl Mummert to find the answer:
This paper aims to outline an analysis and interpretation of the process that led to First-Order Logic and its consolidation as a core system of modern logic. We begin with an historical overview of landmarks along the road to modern logic, and proceed to a philosophical discussion casting doubt on the possibility of a purely rational justification of the actual delimitation of First-Order Logic.
-- Ferreirós, José. (2001). The Road to Modern Logic-An Interpretation. Bulletin of Symbolic Logic. 7. 10.2307/2687794.
THIRD NOTE ADDED. Indeed, thanks to @Carl, the issue was appropriately discussed in this article. Here is an excerpt that gives the idea:
Skolem’s conference, obscurely published as a paper in 1923, was a masterpiece of clarity and rigorous argument. The only point that is not clearly argued is, unfortunately, why (as he asserts) axiomatization requires a restriction of the quantifiers to the first-order level.
... if we are interested in producing an axiomatic system, we can only use first-order logic. I interpret this to mean that, in his view, the spirit of axiomatics—in the tradition of Pasch, Dedekind, Peano, Hilbert— can only be consistent with the use of FOL as an underlying logic. Let us see how this interpretation can be justified.
... the requirement [for a rigorous derivation of a body of theory] was recognized as equivalent with a principle of independence from meaning, and ultimately with the principle of free realizability of the axiom systems — the freedom, that is, to regard completely different object-domains as models of the system.
... reading the second-order quantifiers as referring to “any (all) class(es)” of objects in the domain, can we assume arbitrary classes, arbitrary subsets of the domain, or not? The former would be consistent with abstract mathematics but, by taking arbitrary subsets to be validated by logic, we would be moving in circles—preempting the desired result of securing with absolute certainty foundations of abstract mathematics.
This is an interpretation given in 2001 of a 1923 argument of Skolem, which, the article says, has been misunderstood! This is a strong interpretation in support of Henkin general semantic, because the standard semantic is only one particular restricted meaning, the one associated with the background mathematical universe. This is basically the thesis given five years before by Manzano, but also seventy eight years before by Skolem and perhaps often in between.
FOURTH NOTE ADDED after the answer of @user21820. Because of the three previous notes added, the emphasis shifted to a comparison between second order logic and first order logic and the related issue of expressive power. However, before these added notes, every thing in the question, especially the first paragraph, was about the possibility to translate efficiently other logics, not only SOL, into many sorted logic. Much of Manzano's book is about the translation of other logics into many sorted logic. This is the main way that she defends the thesis that it is a unifying logic. Still, it is necessary to clear out the confusion created by the different notions of "expressive power" involved in the comparison betwen FOL and SOL so that the answer can focus on the main question. However, because this would take too long as a comment or an added note (to express what is already understood), I provided my answer to that aspect of the question in the list of answers below.