Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!allegra!princeton!caip!lll-crg!seismo!mcvax!enea!sicsten!lhe
From: lhe@sicsten.UUCP (Lars-Henrik Eriksson)
Newsgroups: net.lang.prolog
Subject: Re: Standard behavior?
Message-ID: <1172@sicsten.UUCP>
Date: Sat, 14-Jun-86 03:00:53 EDT
Article-I.D.: sicsten.1172
Posted: Sat Jun 14 03:00:53 1986
Date-Received: Tue, 17-Jun-86 23:02:19 EDT
References: <6500005@uicsl> <29700028@uiucdcs> <768@aimmi.UUCP>
Reply-To: lhe@sicsten.UUCP (Lars-Henrik Eriksson)
Organization: Swedish Institute of Computer Science
Lines: 21

In article <768@aimmi.UUCP> gilbert@aimmi.UUCP (Gilbert Cockton) writes:
>...
>var(X) = All t in Term: can_unify(t,X)
>
>where can_unify is true if a most general unifier can be found for both
>its arguments.
>
>nonvar(X) = Exists t in Term: NOT(can_unify(t,X))
>
>Dirty structures like lists with uninstantiated tails (as in the unit
>time queue trick) are nonvar under these definitions.
>
>I've had minimal training in Logic, so I don't know if the set of all
>Terms is an ok construct. Seems ok to me. 
>...

There is nothing wrong with your definitions, except that you now have to
define the predicate "can_unify"... This can't be done within predicate
logic, either. To defend a claim that something can be defined, you have
to define it completely, and not depend on new predicates with dubious
definability.