2
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ how is your proof a proof? You start by making an assumption on line 10b that never gets discharged ... $\endgroup$ – Bram28 Aug 12 '18 at 1:03
  • $\begingroup$ @Bram28 Thanks for feedback. Yes, I think my attempted represents my inability to perform a proof in OSL. $\endgroup$ – Patrick Browne Aug 12 '18 at 10:15
  • $\begingroup$ @Bram28 I think the proof is OK now. $\endgroup$ – Patrick Browne Aug 13 '18 at 10:04
  • 1
    $\begingroup$ 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. $\endgroup$ – Bram28 Aug 13 '18 at 11:48
  • $\begingroup$ @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. $\endgroup$ – Patrick Browne Aug 13 '18 at 14:15
1
$\begingroup$

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

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

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.