Comment by jwtadvice | Hacker News Reader

Comment by jwtadvice | Hacker News Reader

Parent Full thread

Gotcha. So basically the "axiom" of the law of excluded middle would become an oracle, and then with a call to that oracle a problem requiring the law of excluded middle becomes a proof. Basically - the axiomatic decisions made by mathematicians can be represented as programs by turning them into oracles.

In this case, with the axiom of choice implemented as an oracle, the program for Cantor's Diagonalization can be written.

This makes a kind of ultimate sense. Rice's Theorem shows how a program with an oracle about the behavior of a Turing Machine is contradictory, and this implies that "even with a finite set of axioms" there are no proofs about general classes of Turing Machines and thus there are statements independent of mathematics (a kind of Godelian statement).

Is that right?

If so, that's profoundly simple and also incredible to me. (Hopefully I haven't excited myself into thinking I "got it".)

Could you help me understand what Erdo's Probablistic Method looks like as a program? Which oracles might be required and how you would call them?

I was thinking about LEM today. Without the oracle, you can prove that the double negation of the law of the excluded middle is true, which can be represented with the following type:

    negneg_lem :: ((Either a (a -> r)) -> r) -> r

I'm using a polymorphic r to represent the void type, and I'm using the idea that "not a" is the same as "a -> r".

The proof of negneg_lem is just

    negneg_lem f = (f . Right)(f . Left)

No oracle there. If you had an oracle

    oracle :: ((a -> r) -> r) -> a

then you would get the normal LEM as

    lem = oracle negneg_lem

An interesting thing about the type (a -> r) -> r, i.e., double negation, is that it is the type for continuation-passing style. This suggests that a classical proof is something which is allowed to do backtracking search, but I'm still trying to understand exactly how that is.

(Also, the oracle is somewhat absurd. Really, if you have a function which takes functions, you can produce an element of the function's domain? It might almost make more sense if r was a void type.)

Yes, classical propositional logic can be given a constructive interpretation using call-with-current-continuation. This was first worked out by Timothy Griffin [1], and there is a cute story by Philip Wadler about making a deal with the devil [2, section 4].

[1] http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf [2] http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf

As black_knight said, you don't need the axiom of choice for Cantor's diagonalization proof---that particular proof is completely constructive and can be written as an ordinary non-oracular program.

Huh looks like I need to do a lot more reading to understand all of this! :)

I'm still trying to understand what the Probablistic Method looks like as a program. Any thoughts on that?

Reply on news.ycombinator.com