4 ms·

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 exclud

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?

kmill 10y ago
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.)
- vilhelm_s 10y ago
  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 http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf [2] http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf
vilhelm_s 10y ago
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.
- jwtadvice 10y ago
  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?

kmill 10y ago

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.)

vilhelm_s 10y ago
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 http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf [2] http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf

vilhelm_s 10y ago

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.

jwtadvice 10y ago
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?