Bug in ``New types; also opacity without passkeys''

[Michael R. Blair <ziggy@martigny.ai.mit.edu>]

Will Clinger proposed:
>--------------------------------------------------------------------------
> MAKE-NEW-TYPE takes no arguments.  The result of MAKE-NEW-TYPE
> is not a predicate, but a new type descriptor <type> that is
> different from all existing type descriptors.  (This is made
> more precise below.)
> 
>     (GET-NEW-CONSTRUCTOR <type>),
>     (GET-NEW-SELECTOR <type>), and
>     (GET-NEW-PREDICATE <type>)
> 
> respectively return a constructor U, a selector D, and a predicate P?
> that satisfy the following constraints.
> 
> Let <object> be any object, and let <object2> be any object that
> was not constructed by U.  Let <type2> be the result of a call
> to MAKE-NEW-TYPE that is dynamically distinct from the call
> that returned <type>.  Then
> 
>1.   (GET-NEW-CONSTRUCTOR <type>) = U       that is, successive
>2.   (GET-NEW-SELECTOR <type>) = D          calls return the
>3.   (GET-NEW-PREDICATE <type>) = P?        same procedures
> 
>4.   (P? (U <object>)) = #T
> 
>5.   (P? <object2>) = #F
> 
>6.   ((GET-NEW-PREDICATE <type2>) <object>) = #F
>
> .
> .
> .
>
>--------------------------------------------------------------------------
[I took the liberty of numbering the above axioms to facilitate discussion.]

I believe you must have meant:

 6.   ((GET-NEW-PREDICATE <type2>) (U <object>)) = #F
                                   ^^         ^
                                   ++         +

Otherwise, since I can choose any <object>, I choose:

 <object> = ((GET-NEW-CONSTRUCTOR <type2>) <object>')  for any <object>'


Now, as you had written it, there is a contradiction in:

 1'.  (GET-NEW-CONSTRUCTOR <type2>) = U'
 3'.  (GET-NEW-PREDICATE <type2>) = P?'

 4'.  (P?' (U' <object>')) = #T

 6'.  ((GET-NEW-PREDICATE <type2>) <object>) = #F

   => ((GET-NEW-PREDICATE <type2>)
       ((GET-NEW-CONSTRUCTOR <type2>) <object>')) = #F

   => (P?' (U' <object>')) = #F


So 4' <=> 6'.   Q.E.D.

--

With the corrected 6. I have offered, no such contradiction ensues.

--

I have not yet looked carefully at the rest of your axioms or claims.