[opentheory-users] Troubleshooting an article reader

[Rob Arthan]

Mario,

On 16 Oct 2014, at 08:36, Mario Carneiro <di.gama at gmail.com> wrote:

> 
> \a. (abs (rep a)) = \a. a
> 
> and similarly for the other:
> 
> P = \r. ((rep (abs r)) = r
> 

In fact, you win today’s star prize, because the above characterisations
give a workable way of formulating using only the typed lambda calculus
the type specification principle that is discussed in the HOL4 documentation,
but has never actually been implemented (despite having some really nice properties).

As described in the HOL4 logic manual, the type specification principle
would not be acceptable in the HOL Light or OpenTheory kernels because
it depends on various non-primitive constants. The problem is to
express using only the typed lambda-calculus something equiprovable with
the following sequent, (*) say;

Gamma |- (?f. TypeDefn P f) => Q

where P and Q are closed terms satisfying certain conditions.
From this (and another theorem that is easy to express without
the logical connectives), you get a new type operator (alpha1, … alphaN) op
whose defining property is q[alpha1, … alphaN) op/alpha].
This generalises new_type_definition, which is the special case when
Gamma is empty and Q is ?f.TypeDefn P f.

Now ?f. TypeDefn p f is equivalent to ?abs.?rep. R P abs rep,
where R P abs rep asserts that abs is left-inverse to rep and that
rep is left-inverse to abs precisely where P holds (i.e., the properties
that new_type_definition gives you of the abstraction and
representation functions that HOL Light insists on defining for you).
So (*) is equivalent to (**):

Gamma |- (?abs.?rep. R P abs rep) => Q

By first-order logic, (**) is equiprovable with:

Gamma, P = (\r.rep(abs r) = r), (\a.abs(rep a)) = (\a.a) |- Q

I had been fiddling around with various not very nice
approximations to the above. With your improvements you get
something that is relatively easy to understand and is
simple enough to propose for serious consideration
as a more general replacement for new_type_definition.
(Note that it also satisfies you desiderata for naming things:
the names of rep and abs above are whatever the user chooses.)

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141016/273c281e/attachment.html>