Translating from First Order Logic to Order-Sorted Logic

first-order-logiclogicproof-theory

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.

enter image description here

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.

enter image description here

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.

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

Related Question