# Is many sorted logic really a unifying logic?

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.

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:

1. 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?
2. 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?
3. 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.

• Reading a review of the book, it doesn't sound like it addresses substructural logics or logics that are weaker than (classical) FOL such as intuitionistic or paraconsistent logic. – Derek Elkins Oct 8 '18 at 3:24
• Google for any of "HOL", "Coq", "Agda" or "Lean" to find out about ongoing work on widely used logics and tools that implement higher-order type systems of various kinds, which subsume many-sorted first-order logic and cannot easily be translated into many-sorted logic. I think Manzano was talking about variations on first-order logic (where she was probably right) and not thinking about higher-order logics. – Rob Arthan Oct 9 '18 at 22:15
• The book dedicates its first chapter to second order logic (with standard semantic) and argues that we don't need it in practice. One point is that a change of semantic does not change the language in itself (the set of formulas, etc.) or the proof method. So, the semantic is only important (in automatic proof systems, etc.) if you want to speak about the semantic properties of the logic. For example, if we want to say that HOL/Isabelle is complete, then it's not standard semantic. If it's not standard semantic, then it might be translatable into a many sorted logic. Not sure, I'm learning. – Dominic108 Oct 10 '18 at 4:21
• @Dominic108 Intuitionistic and paraconsistent logics are typically sublanguages of classical logic. The issue is that it is harder to remove power than add it. Using weaker logics makes more distinctions which get obliterated in stronger logic. This is especially pointed for substructural logics as the logical connectives split into multiple forms, e.g. multiple forms of conjunction. Weaker logics also allow anti-classical axioms to be added. Finally, weaker logics have a broader range of semantics. Embedding into classical FOL makes all this impossible or at least much more complicated. – Derek Elkins Oct 11 '18 at 5:10
• @Dominic108 That paper doesn't reduce intuitionistic logic to classical logic, but second order logic in the classical and intuitionistic varieties to first order logic in the corresponding variety. – Derek Elkins Nov 15 '18 at 6:14

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.

It is actually misleading to think of SOL with full semantics as 'allowing talk' about the background mathematical universe. This is because full semantics is really and truly a semantic notion totally separate from the (syntactic) second-order system itself. I think it is important to maintain a very clear distinction between syntax and semantics; a system cannot talk about any interpretations of itself. Even if we can interpret it to be doing that, it is still just an interpretation, and not what it is doing. In other words, the symbols are meaningless until we interpret them. You can choose to interpret an SOL system using full semantics, or you can choose to use Henkin semantics, and neither choice has anything to do with the system itself; it generates the same theorems.

Furthermore, the formal system meant for foundational purposes has to be one with a computable proof verifier (or equivalently theorem generator). So it would make no sense to ask for a formal system that is complete with respect to SOL with full semantics, since any reasonable foundational system must be able to reason about finite program runs, which by the generalized incompleteness theorems is incompatible with full-semantics SOL, since PA2 (second-order PA) is categorical but the theory of $$\mathbb{N}$$ is uncomputable.

This means that if we are interested in full-semantics SOL it cannot be for foundational purposes, and so must simply be a mathematical notion residing in our meta-system (MS). Of course in MS we can discuss formal systems as objects, but for the reasons above, MS cannot be based on any formal system that is complete with respect to full-semantics SOL, and so necessarily no system captured by an object in MS can pin down the 'true' natural numbers, because the mathematical notion $$\mathbb{N}$$ itself is merely an object in MS, very incompletely pinned down by MS itself. Same goes for anything that appears to be essentially uniquely defined by some second-order system under full semantics.

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.

As explained above, one cannot consider full-semantics SOL to have more "expressive power" in the specific sense of being able to express more, since it does not. Of course, MS may assume (or prove) the existence of a full-semantics model of PA2, and may further prove that this model is essentially unique. But (in my view) it is not full-semantics PA2 that is more expressive than (first-order) PA; it is MS that is more expressive!

To clarify my objection to the use of the word "expressive", consider what you think PA2 is really expressing. Its meaning under full semantics can only be defined with respect to the collections that exist in MS, and what collections exist in MS are obviously governed by MS. So it is misleading to think of PA2 as expressing anything on its own since its meaning is tied to what MS can express.

In contrast, the notion of models of an FOL system is quite independent of MS. Although the domain still must be a collection in MS, and each symbol must be interpreted by some function or relation in MS, the truth-values of sentences in each model is fixed, independent of MS (as long as you agree that collections, functions and relations are meaningful independently of MS). Similarly with Henkin models of an SOL system. This is not so with full-semantics models of an SOL system, because the collection of sets must be exactly the powerset of the collection of individuals, where "powerset" must exactly coincide with what MS 'thinks'. Clearly then we are importing all the assumptions of MS into the notion of a full-semantics model.

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?

So (as per above) it does not make sense to say that full-semantics SOL had any extra expressive power over FOL at all. It is analogous to claiming that we can get more by assuming that $$\mathbb{N}$$ is a standard model of PA than by just assuming it is a model of PA. Of course, but this assumption is made in the MS, not in PA.

In the same manner, if we are building a foundational higher-order formal system, we should reasonably want it to be complete for Henkin semantics, because that captures more or less what second-order objects we are certain necessarily exist (since the comprehension axioms correspond exactly to the definable subsets over the first-order objects). Thus a formal system that is complete for Henkin semantics is not only more general (unifying) than one for full-semantics, but will also be more robust.

For example, any reasonable MS can prove (via the incompleteness theorems) that if MS itself is consistent then MS has a model with a non-isomorphic $$\mathbb{N}$$. So it means nothing for second-order PA to be categorical under full semantics. In contrast, there is no 'illusion' of categoricity for Henkin semantics.

Note that what I wrote is based on my interpretation of the English words "expressive" and "talk" and "unifying" and so on, and other logicians may not have the same notion in mind when they use the same words. But anyway the mathematics is the same; MS knows that for every model of itself there will always be another model that disagrees on full-semantics models of PA2 even though it is categorical, and that is the core of what I am getting at when I say that full semantics gives an 'illusion' of expressiveness. It is not that Henkin semantics allows you to 'express less', but rather it does not give the impression that you can pin down structures that cannot be pinned down. Hope it is clearer. =)

And now I'm going to say something about translation of practical formal systems into FOL.

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.

Technically speaking, every possible practical foundational system $$S$$ can be translated uniformly and easily into FOL. This is because (as stated above) it must have a computable proof verifier, and so even a weak MS such as TC (theory of concatenation) or PA will be able to 'trace' the finite runs of the verifier and hence capture which statements are proven by $$S$$.

Specifically, there is a $$2$$-parameter sentence $$V$$ over TC such that for every strings $$p,x$$ we have that MS proves $$V(p,x)$$ iff $$p$$ is a valid proof over $$S$$ of statement $$x$$. (The same holds for PA but we of course have to encode strings say using Godel numbering, whereas the encoding is trivial for TC.) Note that MS is a first-order theory, and so we have effectively translated $$S$$ into a first-order system, since the theorems of $$S$$ can be recovered directly from the theorems of MS of the form $$V(p,x)$$. (Note that this depends on the soundness of MS, but almost every logician accepts the soundness of TC and PA.)

Such a translation is not only uniform for all practical formal systems but also easy to perform. However, the catch should be obvious; it is a purely syntactic translation. It fulfills the stated goal of representing any target system within a first-order system, but you may ask whether there is a 'natural' translation that also 'captures' the intended semantics. For example, you might want (what are intended to be interpreted as) collections in $$S$$ to also be something like collections in the target first-order system $$T$$.

But what does that actually mean? In the first place, the notion of "collection" will have to be a meta-theoretic notion, namely a concept in MS, otherwise the goal would be no more meaningful than a syntactic translation. Then the answer is no; there cannot always be 'natural' translations, because the intended semantics for collections in $$S$$ may well be incompatible with the intended semantics for collections in MS. For example, if MS is ZFC and $$S$$ is NF, then it is impossible for $$U := \{ x : x=x \}$$ in NF to be a set in ZFC with the same members, since $$U∈U$$ in NF, contrary to Foundation in ZFC. Although NF is a classical first-order theory, you can imagine non-classical variants of NF that still admit a universal 'set'. The point remains that you cannot expect to be able to 'naturally' translate any given arbitrary $$S$$ uniformly into FOL, without it degenerating into a syntactic transform.

Another way to put it is that 'natural' translations are necessarily ad-hoc. For example, you can 'naturally' translate HOA (higher-order arithmetic) into ZFC because we can construct iterated powersets of $$\mathbb{N}$$ in ZFC, and you can 'naturally' translate plenty of stratified type theories (such as CiC) into ZFC plus some large cardinal (e.g. CiC into ZFC plus countably many inaccessibles), because the stratification ensures that the intended semantics are compatible.

Moreover, I would say that it is impossible to 'naturally' translate even some 'pure logics' into FOL, such as provability logic. This is because the modal operator allows us to drop quotation symbols, which in the first place cannot be represented natively as first-order symbols, since quotations are essentially meta-operators. Observe that the PDF you linked to essentially constructs Kripke frames to translate the modal logics mentioned. This is clearly an instance of importing capabilities of MS, and not a 'natural' translation. It also only works because we have proven that those modal logics correspond to some first-order frame condition! If you actually perform that given translation on provability logic and try working in the resulting first-order system, I am sure you will be forced to agree that it is not 'natural'.

As for foundational systems that are applied (in computer science or physical sciences), the whole purpose of designing stratified type theories was to make them somewhat philosophically justifiable (and hence hopefully not suffer from arithmetical unsoundness). Also, as far as we know, almost every mathematical theorem with direct real-world applications can be proven naturally in HOA (especially if you have the base types $$\mathbb{N}$$ and $$bool$$ and you have the type $$S→T$$ for every types $$S,T$$, rather than just one type for each powerset iterate of $$\mathbb{N}$$). This is of course trivial to express as a many-sorted FOL system, with one sort for each type.

It is true that HOA is unable to prove things about arbitrary types, and that perhaps is the most convincing reason we should go beyond it, if only for conceptual 'completeness'. Unfortunately, as Russell's paradox shows, we cannot possibly have both boolean set membership and unrestricted set comprehension. ZFC discards the latter. But since practical applications almost solely involve 'concrete' objects (below some finite order in HOA), it is unlikely that future proof assistants will be based on radically different foundational systems, since mathematicians will not give up HOA, and it is sufficient for 'concrete' mathematics.

Currently, as far as I know all major proof assistants (such as those listed on Wikipedia) are indeed based on either a classical set theory like ZFC plus some large cardinal axiom, or a stratified type theory like CiC. For instance, Mizar is based on ZFC plus Grothendieck universes, and Coq is based on CiC. This at least implies that work done in established proof assistants can all be 'naturally' translated into a suitable first-order system. This is subjective, but you would have to try it yourself to form your own opinion.

Finally, I will note that many apparently modal logics that are widely used in applied computer science are actually easily translatable into FOL. For example, temporal logic is easily expressed using an axiomatization of time and events in time instead of using modal operators for tenses. Sure, it will be less elegant, but it would be far more general and also fit nicely into standard foundational systems.

• I find this a bit confusing. You write "neither choice has anything to do with the system itself; it generates the same theorems" - I presume "system" here refers to the language + proof system combination? Similarly, when you write "a logic that is complete with respect to SOL with full semantics" I presume "logic" refers to the proof system alone? Given that "system" and "logic" (and similar terms) get used in a variety of ways (to put it mildly), I think it would be worth defining them explicitly. (cont'd) – Noah Schweber Apr 7 at 20:37
• Meanwhile, I disagree strongly with the statement "it is simply wrong to consider full-semantics SOL to have more "expressive power", since it does not." After all, in a precise sense ZFC proves the sentence "the full semantics for SOL is more expressive than the Henkin semantics," and these sorts of statements are actually mathematically valuable. I'm not advocating Platonism, but I do think an important distinction is being lost here. – Noah Schweber Apr 7 at 20:41
• This seems to go along the thesis of Manzano and others. It depends on the purpose that we attach to a logic. It does not mean much that it can express more truths because of a limited full semantic, limited because it has less models than the Henkin semantic. I agree that this is not more expressive power. My way out of this dilemma is to view the logic as separate from the semantic (full, general, Henkin, etc.). I prefer to view the proof system as a way to give a meaning to the sentences and the semantic is a tool to analyze the logic created by both the sentences and the proof system. – Dominic108 Apr 8 at 2:27
• @NoahSchweber, there is no doubt that it is very valuable to consider a domain with less models and that more things can be true in that case. The confusion comes from the fact that this limited set of models, i.e, the full semantic, comes naturally with set theory, which in itself seems completely general. It's definitively an hard to think issue. But from a formal logic view point, we want to separate the general notion of truth from set theory. – Dominic108 Apr 8 at 2:33
• +1 from me (but I think "It is not that Henkin semantics allows you to 'express more'" is a typo)! – Noah Schweber Apr 8 at 16:52

The question is about the current status of translations of different kind logic systems into many sorted logic. These translations are at the core of Manzano's thesis. This is a partial answer to that question, because it deals only with the issue created by the greater expressive power of the full semantic of the second order logic, but it might be seen by many as the most important and fundamental aspect of the answer. The TLDR answer is that the expressive power of a semantic (in the sense of truths existing in that semantic) should not be confused with the expressive power of the logic itself.

Originally and fundamentally, as mentioned by Enderton,

Symbolic logic is a model in much the same way that modern probability theory is a model for situations involving chance and uncertainty.

... you select some features of [a real life] object to be represented in the model ... then you build an object that is like the original in some ways. ... [In Logic,] (t)he real-life objects are certain "logically correct" deductions.

-- H.B. Enderton, A Mathematical Introduction to Logic, Second Edition, in the Introduction.

In a way, we can say that we have two notions of truth. The truth as determined by the axioms and the deductive system and the truth in the "real objects". The idea is that we hope that the deductive system captures all the truths that are normally associated with the counterparts of the axioms in the "real objects". Enderton does not mention it explicitly, but even mathematical notions can be included in this "real-world". In fact, as Popper and many philosophers of science would tell you, we can never directly consider the real world in a theoretical manner. The only things that we can consider directly in a theoretical manner are sentences about this real world. A theory always considers relationships between sentences.

The connection between logic and other mathematical models (in the sense of an abstract theoretical representations of real world objects) is simply that logic use the same languages as in any other models, but the focus shift on the logical relationship between sentences and we are not interested in particular axioms. One key point is that logic should not be tied up with a particular real object or collection of real objects. It should be only about the logical relations between sentences.

This original concept of logic precedes the introduction of Modern Set Theory by Cantor in the 19th century, which he introduced as a way to investigate infinite sets of real numbers. But,

(A)s with other branch branches of mathematics [Logic] has grown beyond the circumstances of its birth. -- Enderton, idem.

... and so has Set Theory. Because of the discovery of paradoxes in Set theory in the early 1900, set theory had to be formulated more rigorously based on logic. In the following years, having a solid logical foundation, Set Theory gained in importance as a basis for mathematics. Worth of mention in this regard, is the Principia Mathematica written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913 (see https://en.wikipedia.org/wiki/Principia_Mathematica)

We mention this aspect of the history to emphasize that during the next 20 years or so, Logic was behind set theory, but there was no formal relationship in the other direction. It is only with Tarski and Godel, in the early 1930, that a meta-logical notion of truth given by mathematical structures was introduced. In this meta-logical notion, a sentence is considered true (a validity), if it is true in all mathematical structures that respect a given signature fixed by the logic. This was the birth of modern logic as we know it now. The semantic (the collection of mathematical structures with the given signature) is nowaday an integral part of the logic. So, coming with any logic, we have now a third notion of truth. We recall that the first notion of truth is fixed by the deductive system and that the second is the "real world" of logical relationships, not necessarily attached to Set Theory. The third one is the notion of truth fixed by the chosen semantic.

With this third notion of truth, came also a new notion of expressive power, which depends on the chosen semantic. The natural choice is to pick a semantic that corresponds as much as possible to the "real world" of logical relationships. Let's recall that we want a logic that is independent of any specific "real world" object or domain of objects. Therefore, this suggests that the semantic should include all structures that can possibly be described formally. Given the previous argument that we can only directly consider sentences about the real world, if we believe in the general ability of the mathematical universe to express those sentences, the third notion of truth coming with this natural semantic becomes identical to the second notion of truth, the truth in the "real world" of logical relationships. It seems the right choice of semantic. This is the argument of Skolem’s conference published in 1923, of Manzano in 1996 (a student of Henkin) and of many others.

Now, we need to explain why a different semantic has been originally used for SOL instead of this natural choice. The history is important to put things in their context. If the signature of a logic has variables that represent sets and we can have quantifiers over these variables, it is considered a second order logic. To define the semantic, we must fix what are the possible domains for such a variable in the different interpretations. If the domain of such a variable is always, i.e, in all interpretations, all possible subsets of the universe (which is itself fixed in the structure), then it is the standard or full semantic. This is a very natural definition. It also makes the logic very expressive, because there is less structures. This is such a natural and attractive definition for the domain of a variable (that represents a set) that it is only in 1950 that a more general semantics was proposed by Henkin. Henkin realized what we discussed before and much more. He proved the interesting result that with a more general and flexible semantic that accepts all structures that can be formally described, we have only one notion of truth ! The deductive systems match perfectly with the "real world" of logical relationships as captured by the Henkin semantic !

Still, aren't we losing something by not using the expressive power of the full semantic? This is a bad question. Who said that we should not use it? The mathematical universe that is used to describe the models of the full semantics is itself described in first order logic. So, we have access to this limited collection of structures in the world of first order logic and we are not saying that we cannot consider it as a "real world" object and study it, again with a first order logic. The point here is only that we should not use this limited collection of models to define the semantic of a logic. What is the advantage of using the full semantic to define a logic, when it is known that the deductive system cannot prove the corresponding validities?