Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 30 May 1995 13:52:09 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA204355670;
          Tue, 30 May 1995 06:07:50 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA203745629;
          Tue, 30 May 1995 06:07:09 -0600
Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 30 May 1995 10:45:13 +0100
X-Mailer: exmh version 1.6 4/21/95
To: Rob Arthan <rda@win.icl.co.uk>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: Finite+Infinite Sequences
X-Uri: <URL:http://www.cl.cam.ac.uk/users/lcp>
X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> 
        E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 
        13swsz`i*9}*8fy}.au9jo.
In-Reply-To: Your message of Wed, 24 May 1995 21:15:33 -0000. <9505242015.20242.0@win.icl.co.uk>
Date: Tue, 30 May 1995 10:45:04 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:008210:950530094520"@cl.cam.ac.uk>

> But the functor in question, F(Z) = 1 + A*Z, has no greatest fixed
> point in ZF, does it? 

That is correct, or more precisely, the gfp is the same as the lfp.  My papers 
describe alternative definitions of + and * such that the constructions work.  
These definitions are very simple.  They are based on an alternative 
definition of ordered pair, namely <a;b> == ({0}*a) U ({1}*b), where here * 
stands for the traditional Cartesian product.  I think some authors have 
referred to this as a "flat" ordered pair.  For details, please see the 
papers.  The ZF one is more detailed.

							Larry Paulson