5 ms·

Anyone really familiar with this: are non-constructive proofs, things like Cantor Diagonalization or Erdos's Probabilistic Method, programs? Are they just non-t

Anyone really familiar with this: are non-constructive proofs, things like Cantor Diagonalization or Erdos's Probabilistic Method, programs? Are they just non-terminating programs? I can see Cantor Diagonalization as a non-terminating program really easily, but I don't understand what the Probabilistic Method looks like as a program.

LolWolf 10y ago
Sure, you can add an oracle for axiom of choice and you're done (note that AoC -> Excluded Middle). A proof is then "constructive" in the same way (e.g. Can be also written as a program, there).
openasocket 10y ago
Nit: I'm not sure I would consider Cantor Diagonalization non-constructive. I wouldn't consider it constructive either, though. It's used to prove things like the uncountability of the reals: how do you constructively prove that no bijection exists between the naturals and the reals?
black_knight 10y ago
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
ufo 10y ago
I think it is hard to talk about cantor diagonalization as constructive or non-constructive because it is reasoning about uncountable sets. A more down to earth example of a non-constructive proof would be proofs using non-constructive elements of classical logic like excluded middle (P V ~P), double negation elimination (~~P -> P) or Peirce's law (((P->Q)->P)->P). For example, this proof[1]. There are some similarities between non-constructive logic and non-purely-functional programming. It it possible to see language features such as mutable assignment, exceptions and call-with-current-continuation as analogous to the non-constructive parts of classical logic. These features all make the language depend on the order of evaluation, which destroys makes the program non-constructive[2] Anyway, I had a really good reference for this but I can't find it right now :( Hopefully someone else can provide a better link explaining how call/cc is equivalent to peirce's law. [1] http://math.stackexchange.com/a/1118851 http://math.stackexchange.com/a/1118851 [2] http://stackoverflow.com/questions/24711643 http://stackoverflow.com/questions/24711643
- User23 10y ago
  I've always seen some close parallels between Peirce's approach to logic and Dijkstra's approach to program construction. Both start with an "empty" object and then transform it according to simple rules until the finished product satisfies some chosen set of predicates. But most everyone here knows Dijkstra, so I'm mostly just replying to thank you for bringing up Peirce. He's wildly under acknowledged and more importantly under-appreciated. Truly an American genius.

LolWolf 10y ago

Sure, you can add an oracle for axiom of choice and you're done (note that AoC -> Excluded Middle). A proof is then "constructive" in the same way (e.g. Can be also written as a program, there).

openasocket 10y ago

Nit: I'm not sure I would consider Cantor Diagonalization non-constructive. I wouldn't consider it constructive either, though. It's used to prove things like the uncountability of the reals: how do you constructively prove that no bijection exists between the naturals and the reals?

black_knight 10y ago

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

ufo 10y ago

I think it is hard to talk about cantor diagonalization as constructive or non-constructive because it is reasoning about uncountable sets. A more down to earth example of a non-constructive proof would be proofs using non-constructive elements of classical logic like excluded middle (P V ~P), double negation elimination (~~P -> P) or Peirce's law (((P->Q)->P)->P). For example, this proof[1]. There are some similarities between non-constructive logic and non-purely-functional programming. It it possible to see language features such as mutable assignment, exceptions and call-with-current-continuation as analogous to the non-constructive parts of classical logic. These features all make the language depend on the order of evaluation, which destroys makes the program non-constructive[2] Anyway, I had a really good reference for this but I can't find it right now :( Hopefully someone else can provide a better link explaining how call/cc is equivalent to peirce's law. [1] http://math.stackexchange.com/a/1118851 http://math.stackexchange.com/a/1118851 [2] http://stackoverflow.com/questions/24711643 http://stackoverflow.com/questions/24711643

User23 10y ago
I've always seen some close parallels between Peirce's approach to logic and Dijkstra's approach to program construction. Both start with an "empty" object and then transform it according to simple rules until the finished product satisfies some chosen set of predicates. But most everyone here knows Dijkstra, so I'm mostly just replying to thank you for bringing up Peirce. He's wildly under acknowledged and more importantly under-appreciated. Truly an American genius.