[FOM] Reference request: realizability interpretations for CZF

[Robert Lubarsky]

A source for realizability that (arguably) pre-dates McCarty is Beeson's
book Foundations of Constructive Mathematics, which includes realizability
models for set theory (IZF-style and the like, since CZF was not then
around). This book naturally contains good references to the earlier
literature.

 

A site with lots of links to realizability resources is
http://www.staff.science.uu.nl/~ooste110/realizability.html, maintained by
van Oosten. In particular is listed there Algebraic Set Theory and the
Effective Topos--
<http://www.staff.science.uu.nl/~ooste110/realizability/feb05.ps.gz> ps.gz
file, Journ.Symb.Log.70(3) (2005),879-890, which describes McCarty's model,
and includes a correction of one of his lemmas. Van Oosten also has a book
called Realizability, which I don't have in front of me now, and so cannot
say whether it includes the proofs you desire, but it would be odd if it
were not a helpful reference.

 

Another option is my CZF and Second Order Arithmetic, Annals of Pure and
Applied Logic, 141 (2006), pp. 29-34, also available at
http://math.fau.edu/lubarsky/pubs.html. The verification that constructive
logic is realized is merely referenced out to McCarty, but if truth be told
that's fairly easy. The verification of the equality axioms is at least
sketched there. The best news is that the CZF-axioms are verified in detail,
so maybe this is what you're looking for. This model has also been studied
by Streicher and van den Berg, and is in van Oosten's book.

 

If you still want McCarty's thesis itself, have you tried contacting CMU for
the thesis or corresponding tech report? Or contacting McCarty or his
advisor Dana Scott? If all else fails, I would copy and send you the
relevant chapter.

 

Bob Lubarsky

 

From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] On Behalf Of
Anders Lundstedt
Sent: Tuesday, February 04, 2014 8:37 PM
To: fom at cs.nyu.edu
Subject: [FOM] Reference request: realizability interpretations for CZF

 

I am looking for references on realizability interpretations for CZF. All
papers I have found refer to the following for proofs.

D. C. McCarty. Realisability and Recursive Mathematics. PhD thesis,
Philosophy, Oxford University, 1984.

I would appreciate suggestions on how to obtain McCarty's thesis, or
references not referring to McCarty for proofs.

Thank you,

Anders Lundstedt

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140207/bac94495/attachment-0001.html>