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/ ]

A slightly different take on computability is given by Pieter Hofstra and I in "Introduction to Turing Categories" (APAL 156, issue 2-3, 2010, 183-209). This described a continuation of the program of doing "recursion theory without elements" initiated by Alex Heller and Robert Di Paola -- which we refer to more prosaically as abstract computability. We extended the original ideas to not only cover the standard setting of recursion theory but also, for example, the total models (from the lambda calculus). Essentially a Turing category can be characterized as the computable functions of a pca living somewhere. As the pca need not live in sets the total functions of a Turing category can be considerably less than all the computable functions (of course they could also include much more). Significantly the total functions can be any "functional complexity class". Thus, there are Turing categories whose total functions are precisely the PTIME functions (and similarly for the LOGSPACE functions etc.). These examples are the basis for claiming that abstract computability might be useful in unifying computability and complexity. The basis for the statement that there are Turing categories with these properties is spelled out in "Timed sets, functional complexity, and computability" (ENTCS 286, 2012 pages 117-137). This year in MFPS Pieter Hofstra (with Pavel Hrubes and I) continued this work and described abstractly exactly which categories can be the total maps of a Turing category. -robin (Robin Cockett) On Wed, Jul 2, 2014 at 11:55 AM, Vasili I. Galchin <vigalchin@gmail.com> 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

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]