I understand that the expressive power of first order logic with one sort is the same as any many sorted first order logic, and that higher order logic with general semantics is the same as a many sorted first order logic. You can add additional predicates to stratify these sorts and reduce many sorted first order logic to the orthodox classical single sorted first order logic. This looks pretty useful for reasoning about the logic itself, like establishing completeness and soundness hold, at the cost of readability.

But it looks to me that having these additional sorts with comprehension axioms can not only be more readable but be more compact; If you can prove things about families of functions or predicates in higher order logic (Henkin semantics) then you don't have to have lemmas for every single function and predicate referenced, but just one. There might be increased cost in unification across different but unifiable sorts, but I imagine the proof might be shorter.

Is this intuition accurate? Is many-sorted first order logic more efficient in proof length than single sorted first order logic?

  • $\begingroup$ That's an interesting conjecture. Have you tried to formalise and prove it yourself? $\endgroup$ – Rob Arthan Jan 6 '15 at 2:25
  • $\begingroup$ No. I'm familiar with the speed-up theorem, but that's for systems of different strength rather than systems of the same strength but different rules. I'm not a mathematician by training, and most everything I know about math and logic is self taught; is this a hint that the question has an obvious answer? $\endgroup$ – dezakin Jan 6 '15 at 19:17
  • $\begingroup$ No. It was actually a hint that you are leading into quite a technical area, so I was encouraging you to think about how the technical details might look. $\endgroup$ – Rob Arthan Jan 6 '15 at 20:40
  • $\begingroup$ Alright. I'll have to spend some time thinking about it and see what I can do to come up with a proof or find a paper that illustrates an existing one, but without formal training it may take me some time... $\endgroup$ – dezakin Jan 6 '15 at 20:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.