🚀 go-pugleaf

My previous post on this matter was poorly worded, and contained some
mistakes in the presentation of the proof.  Herewith an improvement:

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, 

   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
-- 
Mark A. Fulk			University of Rochester
Computer Science Department	fulk@cs.rochester.edu