[Agda] Classical Mathematics for a Constructive World

[Peter Hancock]

On 25/11/2012 22:36, Peter Divianszky wrote:
> On 25/11/2012 20:03, Peter Hancock wrote:
...
>> 1. If we wanted to prove something specifically about computable
>> sequences, then we could either prove it about
>>     a. sequences for which there is a turing machine computing
>> extensionally the same function.
>>     b. sequences for which it is not absurd that there exists...(ditto).
>
> I am a bit confused.
> Is
>   ℕ → ₂
> not the space of computable functions from ℕ to ₂?
> Are ℕ → ₂, a. and b. three different things, given that the domain is ℕ and the image is ₂ ?
> Could you highlight the difference?

I think the situation is this.

1.The analysis of computable functions by Turing
is equally meaningful in constructive and in classical mathematics.  I'm not aware
of any significant divergence between constructive and classical methematics
in the elementary parts of what used be called "recursion theory" but is nowadays called "computability theory".

2. You can formulate "Church's thesis", that in rough terms says "all functions are computable"
in 2 ways, corresponding to my "a" and "b" above (ie. with the Sigma quantifier, or some
"squashed" version of Sigma such as "double-negated" Sigma).  This can be done in Heyting's
arithmetic, or type-theory, or whatever.  Then you can ask what happens when "CT" is taken
as an axiom/postulate.  As far as I know,
a. The strong of CT, is inconsistent with extensionality (EXT2) for functions (N->N)->N, and the axiom of choice (AC).
    From these assumptions we can solve the halting problem.  I think this has been known since the late 1950's.
    There are a number of results in the same direction.  I think there is some discussion of this in the
    book by Beeson "Foundations of Constructive Mathematics".
b. The weak form of CT is compatible with EXT and AC.  This can be shown by a "recursive" realisability model.

I may be mistaken in some details -- maybe some expert (Martin?) will show up and put me right.
But "something like that".  Apologies for being vague.

The upshot, modulo some details, is that N->2, a and b are 3 different things, in the sense that over a
sane system for formulating parts of constructive mathematics, like HA, HAw, and TT, there are models
(defined using a constructive metatheory, by the way) that separate all 3.



I just wanted to revise one further thing I said:

>> 2. What is a classical sequence?  Conceivably, it is a relation between
>> Nat and 2 for which it is not absurd that it is total.

I should have said a relation R \subseteq (N >< 2) st
    forall n : N. not not (exists b : 2) R n b
I put the notnot in the wrong place, before the forall.
One should in general be careful about shunting notnot across a universal quantifier.

Peter (H)