🚀 go-pugleaf

In article <1992Sep30.140356.9401@cs.rochester.edu> fulk@cs.rochester.edu (Mark Fulk) writes:
>My previous post on this matter was poorly worded, and contained some
>mistakes in the presentation of the proof.  Herewith an improvement:

Wherein I still left a gap.

>Let f be the left projection function for some pairing function.
>Let J be the set of natural numbers.
>
>We construct I by deleting elements from N; note that this makes I co-r.e.
>In the construction, we will refer to certain requirements R_i:
>
>R_i: range phi_i is finite or there is y in N such that phi_i(y) not in I.
>
>We will also restrain some numbers into I for requirements R_i.  These
>restraints can be broken for higher-priority (lower-numbered) requirements,
>but the standard finite-injury argument will establish that every requirement
>gets met.  The point of these restraints is that the range of f restricted
>to I (f|I) will still be N; this forces any section of f|I to have an
>infinite range, since a section must be in injection.
>
>Stage s:
>
>   Search for s steps for all i such that: requirement i is not met,
>   and there are x,y such that phi_i(x) = y, f(y)=x, and y is not
>   restrained into I for any requirement i'<i.
>
>   Let i0 be the least such i found; let x0 and y0 be corresponding
>   values of x and y.
>
>   Delete y0 from I.
>
>   find y'>y0 such that y' has not yet been deleted from I, and such that
>   f(y') = f(y0) = x0, 

and restrain y' into I for requirement i0.

>
>   Mark requirement i0 as being met.
>
>   For all requirements i>i0 that are marked as met, remove the mark
>   (that is, start treating them as unmet).
>
>End stage s.
>
>I will leave the verification up to the reader.  The basic structure of
>the proof is that every requirement will be met, either by default
>(phi_i has finite range) or by being met in the construction.  The
>latter will happen to each requirement at most a finite number of times
>(2^(i-1) will do it).  Then note that meeting every requirement is enough
>to establish that f|I has no section.
>
>Mark
-- 
Mark A. Fulk			University of Rochester
Computer Science Department	fulk@cs.rochester.edu