Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
From: Rob Arthan <rda@uk.co.icl.win>
Date: Mon, 11 Nov 91 11:39:43+010
Message-Id: <9111111039.8577.0@win.icl.co.uk>
To: info-hol@edu.uidaho.cs.ted, windley@edu.uidaho.cs.ted
Subject: Witnesses for a polymorphic class of groups.


Phil Windley writes:


>       ... I want to prove:
>
>
>       "? g:(*)group . IS_GROUP g"
>

where ":(*)group" is essentially ":(*) >< (*->*->*) >< (*->*)", and
"IS_GROUP g" says that the three components of "g" are the identity
element, multiplication operation and inverse operation of a group
whose elements comprise (all of) the type ":*".  (Note that it is the
words `all of' which cause the problem here:  The above is easy to
prove if we add in a predicate indicating a subset of ":*" and
relativise the conditions on the operations to that subset as in Elsa
Gunter's group library.)

It is not clear to me why Phil wants to prove this conjecture - if the
aim is just to exercise the definitions in order to check that
"IS_GROUP" has been defined correctly, then it will be a lot simpler to
prove a specific instance, e.g. "?g:(bool)group.IS_GROUP g".  If,
however, the general result is what's wanted then there's quite a lot
of mathematics to do:

What "IS_GROUP(g:(*)group)" means is that for any type ":*", "g" makes
":*" into a group. As far as I can see, defining such a "g" involves:


(a) a case split based on whether or not ":*" is finite (in which case ":*"
is in 1-1 correspondence with the cyclic group on "n" elements for some
"n");

and:

(b) some non-trivial reasoning with infinite cardinalities to handle
the infinite case (e.g.  by constructing the the free group on ":*" as
an explicit group structure on ":(* >< int)list", and then showing that
":(* >< int)list" is in 1-1 correspondence with ":*" for infinite
":*").

The upward Lowenheim-Skolem theorem is a general metatheorem ensuring
the existence of arbitrarily large (infinite) models for suitable sets of
first-order axioms - I do not know whether some analogous general
result could be formulated and used to help here.

It is probable that I've missed the point again here (as I think I did
with Phil's earlier example about the polymorphic identity function).
The problem with the group example is the fact that groups are rather
special things (as are most other algebraic structures like rings,
fields, etc.) and, in particular, given a non-empty set "X" there is no
natural way to define a group whose elements comprise "X".


Rob Arthan. (rda@win.icl.co.uk)                 ICL Secure Systems,
                                                Eskdale Rd.
                                                Winnersh,
                                                Wokingham
                                                Berks. RG11 5TT