# FOL as expressive as Many-Sorted FOL?

It has been suggested to me that Many-Sorted First Order Logic (MSFOL) is no more expressive than ordinary/classical First Order Logic. So I did some reading around and looks like Maria Manzano’s Extensions of First Order Logic has a treatment on this. This was raised to me when I was talking about Common Algebraic Specification Language (CASL) which uses MSFOL. The idea is to change the sort to a unary predicate representation.

Let be a sort, so from this

to

The suggestion struck me, it sounded reductionistic; I took it as saying that MSFOL is somewhat not necessary in the end because FOL can be used to simulate MSFOL anyhow. Perhaps it was just a comment and I need not be sensitive. It did make me dig a bit further. Manzano gives the following rationale why MSFOL is useful and why doing sorted stuff in FOL is a bad idea.

- There are many logics modelled well by MSFOL and we lose naturalness if we shift everything to FOL.
- When it comes to Craig’s Interpolation Lemma, MSFOL is better (due to Feferman) because an improved version of it can be proved on the premise of this multi-sortedness.
- FOL version becomes very verbose and a baggage, from the point of view of automated theorem proving, this is pointless overhead.

Due to the above, I can see why the CASL inventors used MSFOL and I would say it was a clever choice!