[FOM] Reference request: realizability interpretations for CZF

[Oosten, J. van]

I believe the uncontested expert on realizability interpretations of CZF is Michael Rathjen. He has several papers on this topic. You can find a few of them on the web page of mine which Bob mentions.

Jaap van Oosten
________________________________
From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Robert Lubarsky [Lubarsky.Robert at comcast.net]
Sent: Friday, February 07, 2014 4:50 PM
To: 'Foundations of Mathematics'
Subject: Re: [FOM] Reference request: realizability interpretations for CZF

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--ps.gz file<http://www.staff.science.uu.nl/~ooste110/realizability/feb05.ps.gz>, 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/20140208/643afd1b/attachment-0001.html>