[FOM] Proofs in Computability Theories

[Andrej Bauer]

> 1. Shouldn't the study of computability be constructive - thinking of
> Markov, and
> 2. Shouldn't the proofs therefore be intuitionistic?

Those are questions that require value judgements which I shall avoid,
but to give some references:

1. Fred Richman's "Church's thesis without tears", The Journal of
Symbolic Logic, Vol. 48, No. 3 (Sep., 1983), pp. 797-803,
http://www.jstor.org/pss/2273473 , is computability theory in
Bishop-style constructive mathematics. This is a lovely short paper
which just shows how to do it.

2. One chapter of Bridges & Richman's "Varieties of Constructive
Mathematics", Cambridge University Press 1987, elaborates on 1.

3. Category-theoretic approaches with their algebraic approach have a
certain constructive sense to them. The authors are not always careful
about the meta-theory, but the models they study are always a kind of
"computability universe" whose internal logics are intuitionistic.
Here the relevant work would include at least (listed in vaugely
chronological order):

* Mulry, P., Generalized Banach-Mazur functionals in the topos of
recursive sets,
Journal of Pure and Applied Algebra 26 (1982), pp. 71–83.

* Hyland, J., The effective topos, in: A. Troelstra and D. V. Dalen,
editors, The
L.E.J. Brouwer Centenary Symposium (1982), pp. 165–216.

* Rosolini, G., “Continuity and Effectiveness in Topoi,” Ph.D. thesis,
University
of Oxford (1986).

* Robert A. Di Paola and Alex Heller: "Dominical Categories: Recursion
Theory without Elements", J. Symbolic Logic Volume 52, Issue 3 (1987),
594-635.

* J. R. B. Cockett, P. J. W. Hofstra: "Introduction to Turing
categories", http://dx.doi.org/10.1016/j.apal.2008.04.005 available at
http://www.mathstat.uottawa.ca/~phofstra/T1submit.pdf . See also these
slides: http://www.mathstat.uottawa.ca/~phofstra/Philadelphia.pdf

4. As a sort of combination of the effective topos and points 1. and
2. above, I have worked out a "synthetic" approach to computability.
This is constructive logic with non-classical axioms which then allow
us to prove basic results in computability (no priority methods--yet).
The most important special axioms are (in addition to countable
choice):

   Axiom of Enumerability: There are countably many countable subsets
of the natural
   numbers.

  Markov Principle: If a binary sequence is not all zeroes, then it
contains a one.

I should point out that the very basic theorems (Projection Theorem,
Selection Theorem, total functions do not have a computable
enumeration) follow _without_ any special axioms simply because the
logic is constructive.

The first axiom, when interpreted in the effective topos, says that
there is an acceptable numbering of c.e. sets. See
http://math.andrej.com/category/synthetic-computability/ for further
information. To get a sense of how it is done, see for example the
proof of Recursion Theorem on page 45 of the tutorial
http://math.andrej.com/wp-content/uploads/2007/05/syncomp-mfps23.pdf .

With kind regards,

Andrej Bauer