Typed logic vs many-sorted logic

Question

I am confused as to what is the difference between many-sorted logic and typed logic.

Are they the same thing? If not, what are the differences?

Answer 1

Many-sorted first-order logic is exactly the same thing as first-order logic over a simple type theory without any type constructors. You may want to look into the first four chapters Jacobs' book Categorical logic and type theory to see how it plays out exactly.

Chapter 4 of that book describes predicate logic over simple type theory, and when you remove all the simple type constructors then you arguably get exactly many-sorted first-order logic. The only difference is maybe one of presentation. In the type theoretical version formulas with free variables will always appear together with a context $x:A,y:B,...$ which declares the sorts of the variables. In other presentations it might be that you have a different stock of variables for each sort, so that they do not have to be explicitly declared. The deductive system in Jacobs book is a sequent calculus. Classical logic books typically use an axiomatic system, or maybe natural deduction. But the theorems which you can prove are the same.