Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Simon Finn <simon@ahl.co.uk>
Date: Fri, 28 Jan 1994 16:53:52 +0000
Message-Id: <372.9401281653@alpha.ahl.co.uk>
To: info-hol@cs.uidaho.edu, wishnu@cs.ruu.nl
Subject: Re: is this formula perhaps decidable?
Content-Length: 1458

Wishnu Prasetya wrote:

> Here is the formula I'm trying to prove:
> 
>     "(!x:*A. ~TC U x x) ==> (!x. InDAG U x)"
> 
> TC U is the least transitive closure of U. InDAG U x means x is in the
> dag induced by relation U.
> 

I don't think this is a theorem, given the supplied definitions:

> let TC_INDUCTIVE = new_definition
>   (`TC_INDUCTIVE`,
>    "TC_INDUCTIVE (U:^MonoRel) P = !y. (!x. (TC U) x y ==> P x) ==> P y") ;;
> 
> let InDAG = new_definition
>   (`InDAG`,
>    "InDAG (U:^MonoRel) x = !P. TC_INDUCTIVE U P ==> P x") ;;
> 

Suppose I take U (and TC U) to be the ordinary < relation on integers
(NB not naturals). Then  "InDAG < z" is

   !P. (!y. (!x. x < y ==> P x) ==> P y) ==> P z

but this is false, because if I instantiate P to \w.false, I get

       (!y. (!x. x < y ==> false) ==> false) ==> false

which simplifies to

       (!y. (!x. ~(x < y)) ==> false) ==> false
(*)    (!y. false          ==> false) ==> false
       (!y. true)                     ==> false 
       true                           ==> false
                                          false

But the ordering relation, "<", is certainly acyclic, which
provides a counter-example to the intended theorem.

It looks to me as if the foramalisation of InDAG needs to be
changed (I think it works for finite domains).

Simon Finn (Abstract Hardware Limited)

(*) because every integer has a predecessor - this is where
we need to use integers rather than naturals.