Skip to content

FOL as expressive as Many-Sorted FOL?

August 29, 2010

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 S be a sort, so from this
\forall x : S \bullet \varphi(x)
\forall x (S(x) \to \varphi(x))

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.

  1. There are many logics modelled well by MSFOL and we lose naturalness if we shift everything to FOL.
  2. 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.
  3. 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!

No comments yet

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: