Hi Thorsten,

On Thursday 01 February 2007 08:55:30 Thorsten Altenkirch wrote:
> thank you - indeed this is a very interesting observation. This was
> the proof I had in mind when I first claimed that the axiom of choice
> is provable in OTT. However, I was deluded in believing that OTT/
> predicative topoi exactly characterize the theory of the setoid
> model. As you clearly point out this is not the case. To me this is
> an incompleteness of the formal system (OTT/predicative topoi) wrt
> the intended interpretation. This should be fixable, leading to OTT+X
> or predicative topoi + X which should be complete wrt the setoid
> model. More categorically we could say that X characterizes the
> predicative topoi obtained by an exact completion of an LCCC - I think.

First of all, I am not sure whether a "fix" is needed. My recent experience in 
constructive mathematics is that it is actually quite pleasant to work 
without countable choice. Initial experience shows that it may lead to better 
algorithms implicit in the proofs. (Most of this is in my work with Thierry 
Coquand.) As you know, choice breaks abstract datatypes. See for instance the 
encoding of ADT as existential types by Mitchell and Plotkin. This is not 
possible in dependent type theory precisely because we have choice (this was 
pointed out to me by Jesper Carlstrom some time ago). I understand one 
motivation for your work on OTT as an attempt to bring back (some?) ADTs in 
type theory. It would be a pity to throw them out again without a good 

Having said that here are some quick remarks on your proposal below. 
Having choice for N->N as somewhat uncommon. It is not present in Bishop's 
constructive mathematics, i.e. more or less the setoid model of ML type 
theory. However, it is present in Brouwerian intuitionism and in some 
realizability models. Brouwer does not have choice for (N->N)->N.

Martin Hofmann has some discussion on choice and extensionality in his thesis, 
but uses a syntactic criterion somewhat like the one that you outline.

One semantic candidate for X could be `all types have a projective cover'. 
This is what is used in realizability theory and what Erik Palmgren 
translated to type theory. A type P is projective if for all f:A->B and every 
function g:P->B there is a function h:P->A with f o h = g. Projective 
types "have choice". The idea is that the projective types are Bishop's 
pre-sets or the types in the setoid construction.



Research Group Foundations/ Institute for Computing and Information Sciences
Radboud University Nijmegen www.cs.ru.nl/~spitters/

Reply via email to