5 ms·

Cantor's diagonalisation is certainly constructive. Given a a sequence of sequences of binary digits, it gives a way of constructing a sequence not occurring in

Cantor's diagonalisation is certainly constructive. Given a a sequence of sequences of binary digits, it gives a way of constructing a sequence not occurring in the sequence of sequences. The resulting sequence is as computable as the input. But to answer your question: Many mathematicians regard their (classical) proofs as algorithms. They just allow themselves to use an oracle call for any well-formed question: Say I want to prove B. Then, at some point in my proof, I formulate a sentence A, and make a call to the oracle. My proof/algorithm then branches: in one branch I assume A is true, in the other I assume A is false. If I can continue such each branch gives B true, then my proof works (classically). [0] The constructive critique is that such an algorithm cannot be executed my humans, or turing machines for that matter. Also there is a whole continuum of stronger and stronger oracles below this ultimate oracle allowed by classical logic — which is an interesting continuum to study. Often one can locate an exact class of oracles needed for a given classical proof to work out. [0]: This is the «church encoding» version of the law of excluded middle: For all B, we have (A → B) → (¬A → B) → B, which is equivalent to the usual formulation (A ∨ ¬A).

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

jwtadvice 10y ago

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?