A student of mine, James R. Otto worked on this for his thesis. Unfortunately, it was famously unreadable. I don't think it was published and I have lost contact with him. It was in the early 90s. Michael On Wed, 2 Jul 2014, Vasili I. Galchin wrote:
Hello Cat Theory list,
Please be gentle.
In the past I studied computability theory. It seems to me that this theory is built on the category of Sets(elementary topos), i.e. this computability theory assumes using classical logic with LEM and boolean subobject classifier for concepts like semi-decidability, etc. Is there a notion of intuitionistic computability theory built on other topoi where LEM is absent from the accompanying higher logic and the topos' subobject classifier has a internal Heyting algebra(that is not boolean)?? Is this what realizibility delves into(I have yet to study realizibility concepts).
Kind regards,
Vasya
-- Every gun that is made, every warship launched, every rocket fired signifies, in the final sense, a theft from those who hunger and are not fed, those who are cold and are not clothed. -Dwight D. Eisenhower [For admin and other information see: http://www.mta.ca/~cat-dist/ ]