[Agda] Classical Mathematics for a Constructive World

[Peter Hancock]

On 27/11/2012 22:20, Martin Escardo wrote:
> There is also Peter Hancock's question. Well, probably not a
> question. But I lost your message, Peter, and I can't find it.

I don't think I had a question... oh yes I did!

First, let me try to state my position wrt Church's thesis.

MP: I would be extremely suspicious of any formal system, or
    style of formal system intended to formalise constructive mathematics
    if it was not compatible with some version of Church's thesis.
    A little more precisely, it should admit a model, constructed in a vanilla
    constructive metatheory, (well, Matin-Lof's system without special/anomalous
    stuff like identity types, extensionality in any form, etc)  
    in which a weak version of Church's thesis comes out true.  I would
    be horrified to be shown a closed term of type N->N from which I could not
    read off a Turing machine and a(n internal) proof that it computes the
    denotation of the term in the standard mode.

    Incidentally, the same/similar goes for axioms of continuity at type "2", ie. (N->N)->N,
    and even more so for axioms of extensionality at type 2.  I am *not*
    sufficiently mad to expect strong forms of (a) Church's thesis and (b) continuity at type 2 both to
    hold in the same model.

Now, what is all this about "weak" and "strong"?  Essentially, it is a matter of whether
the existential quantifier in Church's thesis (or a continuity axiom, or whatever it is)
should be full-blooded \Sigma, or a more pusillanimous \exists.  One way of weakening
Sigma is to stick notnot in front of it.  Here is what I'd call a *strong* form of CT, where T is
Kleene's "T-predicate", and U strips the result out of a terminated trace.

  CT:  (Pi f : N->N)(Sigma e : N)(Pi n : N)(Sigma m : N) T(e,n,m) and f(n)=U(m)

Here's something I'd call a *weak* form of Church's thesis.
    
  WCT:  (Pi f : N->N)notnot[(Sigma e : N)(Pi n : N)(Sigma m : N) T(e,n,m) and f(n)=U(m)]
  
Similar things can be formulated for continuity at type 2, where the thing that is said to "exist"
is roughly speaking a well-founded countably-branching tree that represents the type2 functional
a la Ghani/Hancock/Pattinson or Escardo.

Now, my question, such as it was.  Something I got from rereading an ancient
book by Troelstra, is essentially this:

   SCT + EXT2 + AC are jointly inconsistent over HAomega

EXT2 is extensionality at type (N->N)->N.
I also saw something like this in Beeson's book.  Troelstra indicates that
from these 3 ingredients one could solve the halting problem.  He mentions
that a proof can also be constructed from the Kreisel-Lacombe-Shoenfield theorem (from 1959).
I was surprised that SCT is so hostile, even to extensionality.  Univalence apparantly
implies EXT2 inter alia, and is compatible with AC.

NEVERTHELESS,

   WCT + EXT2 + AC are jointly consistent wrt HAomega

All 3 thing are jointly satisfied in a model HEO of the hereditarily effective operations of finite type.
Apparently.

I simply wondered if I had got hold of the wrong end of the stick, or was misreading Troelstra
and got lost in all the metamathematical details.   I felt the need to bleat pathetically for an
expert in such things (eminently, Dr. Escardo) to prevent me from misleading people.

Notnot appears to be a (crude?) form of "squashing", or "bracketing", or "smashing" constructions
of a Sigma type down to "just one", or hiding all distinctions between them.
It seems to have a quite dramatic effect on principles like CT, continuity, and even choice.
Maybe there are other forms of squashing.

By the way, I for (the only?) one am not very sympathetic to all this stuff about "many worlds",
coming from Andrej Bauer.  But that's a whole other topic.

Peter Hancock





>
> My quibble with the so-called Church's Thesis in constructive
> mathematics is that ... I never need it when I prove a theorem.
> Knowing that my input is computable doesn't help me in my
> calculations. I have no need to inspect the source code of the input,
> or of merely knowing that the source code exists.
>
> Moreover, I would think that many inputs come without evidence of
> computability.
>
> Example 1. Suppose I program a certified web server in Agda. My input
> is a stream, and so is my output. If I assumed CT, the protocol would
> have to work like this: please, before sending me the stream, send me
> its Godel number, or promise that it secretly exists, and send me
> evidence of your promise.
>
> Example 2. Suppose I program a certified flight control system for
> airports. Again my input and output are streams. Assuming that the
> inputs come with their Godel numbers, there is no need for radars or
> other tracking devices. I can compute what will happen from the Godel
> number, and I can effectively predict which planes will be where and
> when by just computing. Wouldn't that be marvelous?
>
> Example 3. Suppose I program a certified nuclear power station
> control system. One of my stream inputs comes from a Geiger counter.
> I ask the physicists and engineers to design and build an improved
> Geiger counter that first gives the Godel number of the sequence that
> it produces.
>
> What do you need to know that your input if computable for? And what
> if your input is not (known to be) computable?
>
> Should you implement a validation procedure that rejects
> non-computable input?
>
> Martin _______________________________________________ Agda mailing
> list Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda