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.
Best Answer
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.
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.)