Translating from First Order Logic to Order-Sorted Logic

The following single sorted FOL sentences are from Stanford. Sorts or types are represented by predicates (e.g. $Horse(x)$) \begin{align*} &(1a) \forall x, \forall y ((Horse(x) \land Dog(y)) \Rightarrow Faster(x,y))\\ &(2a) \exists y (Greyhound(y) \land \forall z (Rabbit(z) \Rightarrow Faster(y,z)))\\ &(3a)\forall y (Greyhound(y) \Rightarrow Dog(y))\\ &(4a)\forall x, \forall y, \forall z(Faster(x,y) \land Faster(y,z) \Rightarrow Faster(x,z))\\ &(5a)Horse(Harry)\\ &(6a) Rabbit(Ralph) \end{align*} There is a proof of $Faster(Harry,Ralph)$ at Stanford, which is 16 lines in length.

The Order Sorted Logic that I have in mind was developed in the context of Order-sorted Algebra from Goguen and Meseguer (OSA). Axioms can be expressed over more than one domain of discourse. Variables and constants are typed. A predicates can only accept a term as an argument if the term's sort matches the predicate's declaration. Inference rules must respect a sort/type hierarchy.

Below is my attempt to translate the above to OSL and prove that Harry is faster than Ralph. I have added a super-sort $Animal$ which does not appear in the original FOL representation. In my translation $Dog$, $Horse$, and $Rabbit$ are sub-sorts of $Animal$ and $Greyhound$ is a sub-sort of $Dog$. The relation $Faster$ is overloaded wrt these sorts. I used the Fitch system from Barwise and Etchemendy in my proof attempt. I will try to complete a Latex version soon. I was hoping that the sorted proof would be shorter than the Stanford version without sorts/types (or sets). Perhaps I need a deeper understanding of "types as sets"

My motivation is that I wish to translate arbitrary FOL theories to OSL theories with a view to representing them in an algebraic specification language (CafeOBJ) where OSL theorems can be proved.

My overall approach to the translation consists of:

• Representing sorts as set, with sub-sorts as subsets (e.g. $Dog \subseteq Animal$)
• Replacing the sort predicates with variables of a sort with the same name as the predicate (e.g. $Horse(x)$ translates to $\forall x (x \in Horse)$). My intuition is that this would be $x:Horse$ in a programming language.
• Removing the antecedent from the logical implications where the antecedent consists of sort predicates (e.g. $\forall x, \forall y ((Horse(x) \land Dog(y)) \Rightarrow Faster(x,y))$ translates to $\forall x : Horse, \forall y : Dog \bullet Faster(x,y)$).
• Representing constants as elements of a given sort (e.g. $Harry \in Horse$).

My problem is that my approach is based on ad-hoc intuition which seems reasonable to me. There are some papers that cover the many-sorted case, but I cannot find any papers that validate this approach or provide more formal approaches to the translation. Are there papers that propose other, possibly better approaches?

Below is a second attempt that makes better use of the subsets of order sortedness. • how is your proof a proof? You start by making an assumption on line 10b that never gets discharged ... – Bram28 Aug 12 '18 at 1:03
• @Bram28 Thanks for feedback. Yes, I think my attempted represents my inability to perform a proof in OSL. – Patrick Browne Aug 12 '18 at 10:15
• @Bram28 I think the proof is OK now. – Patrick Browne Aug 13 '18 at 10:04
• Nice! The proof is longer because you use the 'element in' parts as part of the logic statements, but in a sorted logic that's all taken care of by the system. So basically, you translated the sorted logic back into plain first-order logic ... which actually increased the complexity of the proof. – Bram28 Aug 13 '18 at 11:48
• @Bram28 Agreed, but what can I use as an inference step? Do I just use sub-set relation? I have tried to prove this theorem using an OSL prover, but because the goal has fixed types the more general transitive axiom was not used. – Patrick Browne Aug 13 '18 at 14:15

I don't know about the OSA system specifically. However, here's a proof that I wrote up in Coq using types. Most of the length of this is just the setup, then the actual proof becomes very short.

Parameters Horse Dog Greyhound Rabbit Animal : Type.
Parameter Horse_inc_Animal : Horse -> Animal.
Parameter Dog_inc_Animal : Dog -> Animal.
Parameter Greyhound_inc_Dog : Greyhound -> Dog.  (* 3a *)
Parameter Rabbit_inc_Animal : Rabbit -> Animal.

Coercion Horse_inc_Animal : Horse >-> Animal.
Coercion Dog_inc_Animal : Dog >-> Animal.
Coercion Greyhound_inc_Dog : Greyhound >-> Dog.
Coercion Rabbit_inc_Animal : Rabbit >-> Animal.

Parameter Faster : Animal -> Animal -> Prop.

Axiom stmt_1a : forall (x : Horse) (y : Dog),
Faster x y.
Axiom stmt_2a : exists y : Greyhound,
forall z : Rabbit, Faster y z.
Axiom stmt_4a : forall x y z : Animal,
Faster x y -> Faster y z -> Faster x z.

Parameter Harry : Horse. (* 5a *)
Parameter Ralph : Rabbit. (* 6a *)

(* Main result... *)
Goal Faster Harry Ralph.
Proof.

(* existential elimination on (2a) *)
destruct stmt_2a as [g].

(* specialization of (4a), and also implicitly applies ->E (modus ponens)
a couple of times *)
apply stmt_4a with (y := g).

(* Subgoal: Faster Harry g,
proved by specializing (1a) *)
+ apply stmt_1a.

(* Subgoal: Faster g Ralph,
proved by specializing the statement
H : forall z : Rabbit, faster g z
gotten from the existential elimination *)
+ apply H.
Qed.


Again, I don't know how much this would help in constructing a proof in your particular system - I'm just posting in the hopes that it might be close enough to be of some help. (Do keep in mind that Coq is often oriented towards top-down programming of a proof, as in this case, whereas Fitch-style systems are often closer to bottom-up serializations of the same proof term.)

• Thanks for your solution. I am not familiar with COQ, but I think that I get the gist of it. – Patrick Browne Aug 25 '18 at 7:51