🚀 go-pugleaf

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.