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.

 A: 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.)
