5 ms·

Brouwer–Hilbert controversy

95 points by drnewman 8y ago

ocfnash 8y ago
For a long time, I used to dismiss intuitionism but more recently I've come to find it an attractive standpoint. For one thing, you really only gain by trying to be constructive. If, in some logical system without LEM (law of excluded middle), you cannot find a proof of P without using LEM, you still have a result, namely you can prove LEM -> P. You haven't really lost anything! Furthermore, I have often been surprised just how far you can go without LEM. Very often in fact. Finding constructive proofs can feel very much akin to removing an unnecessary dependency from a codebase. Also, even if ultimately, you do need LEM somewhere it is often possible to factor it into the "right" place in the proof rather than globally just sticking `LEM ->` at the front of the whole proof. Also, if you care about, first order logic then in fact you should love intuintionistic logic: it is a finer logic that actually contains first order logic: https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation Lastly, though I have yet to understand this better, constructive proofs seem to be enjoy better computational properties under Curry-Howard.
- maxiepoo 8y ago
  Removing an unnecessary dependency is a good analogy. From a Curry-Howard perspective, intuitionistic proofs correspond to programs without side-effects, and classical proofs correspond to programs that can use continuation effects (for the unfamiliar think of a more principled version of GOTO), so in a real sense intuitionistic proofs are more direct. The double-negation translation then corresponds to implementing continuations in a pure language using continuation-passing style. This also says why classical logic can still be useful: if I'm going to use continuations all the time, it's nicer to program with a language that supports them than to explicitly program in CPS. Pick the right language/logic for the task at hand!
- gnulinux 8y ago
  You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert). Practically, intuitionistic logic has a lot of applications to computer science thanks to Curry-Howard. Philosophically, soundness of LEM depends on where one originates the source of mathematics. If you're like Kant (or Brouwer) then LEM would make little sense since the source of mathematics, just like any other cognitive ability, is human cognition which exists independent of abstractions of the outer world. But, even without being a Platonist (like Godel) if mathematics has any sort of external source (e.g. abstracting the world or being a good abstraction of the world) then it's really hard to argue against LEM, although some epistemological arguments exist.
  - YorkshireSeason 8y ago
    soundness of LEM depends on where one originates the source of mathematics I disagree! One of Goedel's many great contributions was the double-negation translation (later refined by others), and what it does is show that (simplifying a bit) intuitionistic logic and classical logic are equiconsistent! In other words: any contradiction you can derive in classical logic, you can convert into a contradiction in intuitionistic logic. (The reverse direction is trivial because all intuitionistic proof principles are also classical.)
  - IngoBlechschmid 8y ago
    > You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert). Just wanted to chime in regarding the last sentence: There are right now ongoing efforts to eliminate any uses of LEM in algebraic geometry. We do this not only out of academic curiosity, in order to create a more elegant setup and to be able to extract algorithms from proofs, but also to carry out a program called "relativization by internalization". The idea is that we can automatically derive some results for "relative schemes" if we have proven them for ordinary schemes without using LEM or the axiom of choice.
- rntz 8y ago
  This is true, but it has a problem: if you prefer constructive logic to classical because it is "finer-grained", then where do you stop? Linear logic, for example, is finer-grained than both classical and constructive logic. Both can be embedded in it (just as classical embeds into constructive), and it makes distinctions they lack. But linear logic, too, comes in classical and intuitionistic versions, and again classical linear logic embeds into intuitionistic. And it doesn't stop there. Linear logic can be embedded in ordered logic, and ordered logic into the logic of bunched implications. For all I know there are even finer-grained logics out there. But doing all of mathematics in the logic of bunched implications would be an impractical nightmare, I think. I tend to prefer choosing whether to work classically or constructive (or linearly, or orderedly) according to whether it illuminates a relevant part of the problem. Sometimes you care about constructivity; sometimes you don't. If you don't, then don't waste your time trying to do the proof constructively. The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it! :)
  - enriquto 8y ago
    > The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it! This sounds more like a motivation than like a trouble.
  - danharaj 8y ago
    > classical linear logic embeds into intuitionistic. Wait, really? As I understand it there are things provable in LL that can't be proved in ILL. Can't find the citation though. It should be noted that double negation translations are more complicated at the proof level even though they capture provability.
protonfish 8y ago
This is fascinating, but only if you hold faith in inherent truth of mathematical symbolism. Unfortunately, this seems to be the standard dogma of mathematicians, though I haven't seen significant evidence necessary to warrant this belief. If you understand mathematics and logic as merely a formalized language of symbols then you can judge those systems on certain qualities (complexity, clarity, expressiveness, etc.) but not "truth." The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.
- popnroll 8y ago
  I'm really clueless about logic and mathematics theory, but isn't this the Gödel's incompleteness theorem?
  - protonfish 8y ago
    No, the incompleteness theorem only examines how formal systems relate to themselves, not to reality. It shows that no significantly expressive system can be designed that won't allow paradoxical statements.
    - mietek 8y ago
      > It shows that no significantly expressive system can be designed that won't allow paradoxical statements. The above is a complete misrepresentation of Gödel’s second incompleteness theorem. The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means. Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8]. All of these languages are designed to be consistent. Of course, implementation bugs do happen[9]. If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11]. [1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_conditions https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co... [2] Gödel’s second incompleteness theorem, https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theorems#Second_incompleteness_theorem https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor... [3] Dependent type, https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type [4] Total functional programming, https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [5] Agda programming language, http://agda.readthedocs.io http://agda.readthedocs.io [6] Coq proof assistant, http://coq.inria.fr http://coq.inria.fr [7] Idris programming language, http://www.idris-lang.org http://www.idris-lang.org [8] Lean theorem prover, http://leanprover.github.io http://leanprover.github.io [9] The rise and fall of @proofmarket, https://twitter.com/i/moments/921153475836305408 https://twitter.com/i/moments/921153475836305408 [10] Friedman, D.P., Christiansen, D.T. (2018) ‘The Little Typer’, https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer [11] Turner, D. (2004) ‘Total Functional Programming’, http://www.jucs.org/jucs_10_7/total_functional_programming http://www.jucs.org/jucs_10_7/total_functional_programming
danbruc 8y ago
What exactly is the claim here with regard to the law of excluded middle? Maybe somewhat naively it seems rather obvious to me that the law of excluded middle can be true or false depending on what objects you are dealing with. Maybe not the best possible example but in classical mechanics a particle is either inside a region R or it is not inside region R while in quantum mechanics the particle may be inside region R or it may not be inside region R or it may be somewhat inside region R. It seems rather obvious that the logic you are using has to match the behavior of the objects you are applying the logic to or you will of course end up with wrong conclusions. If we change the example a bit, the particle is in region R with probability zero or the particle is in region R with a probability larger than zero, then we again have a case where the set of possibilities is nicely partitioned into two mutually exclusive and exhaustive sets, probability zero and probability not zero. But I guess I am missing something or there wouldn't be a lot of smart people fighting over the issue.
- ratmice 8y ago
  I believe there are a couple of different claims being made in the above, I went ahead and just made a gist with some proofs (in lean) that try and hit some of the points about usage of law of excluded middle, double negation translation you should be able to copy/paste it into https://leanprover.github.io/live/latest/ https://leanprover.github.io/live/latest/ https://gist.github.com/ratmice/21f069b5811d1c40911850cb690a5b5e https://gist.github.com/ratmice/21f069b5811d1c40911850cb690a...
  - danbruc 8y ago
    Thanks for the effort but unfortunately for me the page just says running and nothing ever happens, especially no output at all. Not even for the small example included by default. But besides that I did not really want to make any claims and certainly nothing that could be easily addressed by a proof, I think. My point was more that one has to take care that the type of logic one uses has to fit together with the domain one wants to reason about with that logic. If in the domain you want to reason about the law of excluded middle does not hold or only does so in a non-straight forward way, then using a logic with law of excluded middle will at least be not as easy as it could be or even painful or in the worst case lead to wrong conclusions.
User23 8y ago
The invention of computing automata and the techniques required to program them, such as defining semantics, settles this issue concretely in favor of Hilbert.
- joel_ms 8y ago
  How so? I've always felt that intuitionism/constructivism were closer to theoretical computer science due to constructivism requiring you to produce (or compute) the what you're trying to prove.
  - User23 8y ago
    Dijkstra and Scholten's https://www.amazon.com/Predicate-Calculus-Semantics-Monographs-Computer/dp/1461279240 https://www.amazon.com/Predicate-Calculus-Semantics-Monograp... is a good example of what I mean. The state space is far too large to show a program is correct by constructing all possible processes it could execute. Instead you must show that the program admits no incorrect processes whatsoever, and as far as I know mathematical formalism is the only possible way to do that. Of course if one just wants to make money, formal correctness is observably of absolutely no importance. And there's nothing wrong with wanting to make money!
    - Firadeoclus 8y ago
      From Wikipedia: > Brouwer the intuitionist in particular objected to the use of the Law of Excluded Middle over infinite sets It always seems to me that using the LEM over infinite sets is akin to claiming that all problems are decidable.

95 points by drnewman 8y ago

For a long time, I used to dismiss intuitionism but more recently I've come to find it an attractive standpoint. For one thing, you really only gain by trying to be constructive. If, in some logical system without LEM (law of excluded middle), you cannot find a proof of P without using LEM, you still have a result, namely you can prove LEM -> P. You haven't really lost anything! Furthermore, I have often been surprised just how far you can go without LEM. Very often in fact. Finding constructive proofs can feel very much akin to removing an unnecessary dependency from a codebase. Also, even if ultimately, you do need LEM somewhere it is often possible to factor it into the "right" place in the proof rather than globally just sticking `LEM ->` at the front of the whole proof. Also, if you care about, first order logic then in fact you should love intuintionistic logic: it is a finer logic that actually contains first order logic: https://en.wikipedia.org/wiki/Double-negation_translation https://en.wikipedia.org/wiki/Double-negation_translation Lastly, though I have yet to understand this better, constructive proofs seem to be enjoy better computational properties under Curry-Howard.

maxiepoo 8y ago
Removing an unnecessary dependency is a good analogy. From a Curry-Howard perspective, intuitionistic proofs correspond to programs without side-effects, and classical proofs correspond to programs that can use continuation effects (for the unfamiliar think of a more principled version of GOTO), so in a real sense intuitionistic proofs are more direct. The double-negation translation then corresponds to implementing continuations in a pure language using continuation-passing style. This also says why classical logic can still be useful: if I'm going to use continuations all the time, it's nicer to program with a language that supports them than to explicitly program in CPS. Pick the right language/logic for the task at hand!
gnulinux 8y ago
You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert). Practically, intuitionistic logic has a lot of applications to computer science thanks to Curry-Howard. Philosophically, soundness of LEM depends on where one originates the source of mathematics. If you're like Kant (or Brouwer) then LEM would make little sense since the source of mathematics, just like any other cognitive ability, is human cognition which exists independent of abstractions of the outer world. But, even without being a Platonist (like Godel) if mathematics has any sort of external source (e.g. abstracting the world or being a good abstraction of the world) then it's really hard to argue against LEM, although some epistemological arguments exist.
- YorkshireSeason 8y ago
  soundness of LEM depends on where one originates the source of mathematics I disagree! One of Goedel's many great contributions was the double-negation translation (later refined by others), and what it does is show that (simplifying a bit) intuitionistic logic and classical logic are equiconsistent! In other words: any contradiction you can derive in classical logic, you can convert into a contradiction in intuitionistic logic. (The reverse direction is trivial because all intuitionistic proof principles are also classical.)
- IngoBlechschmid 8y ago
  > You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert). Just wanted to chime in regarding the last sentence: There are right now ongoing efforts to eliminate any uses of LEM in algebraic geometry. We do this not only out of academic curiosity, in order to create a more elegant setup and to be able to extract algorithms from proofs, but also to carry out a program called "relativization by internalization". The idea is that we can automatically derive some results for "relative schemes" if we have proven them for ordinary schemes without using LEM or the axiom of choice.
rntz 8y ago
This is true, but it has a problem: if you prefer constructive logic to classical because it is "finer-grained", then where do you stop? Linear logic, for example, is finer-grained than both classical and constructive logic. Both can be embedded in it (just as classical embeds into constructive), and it makes distinctions they lack. But linear logic, too, comes in classical and intuitionistic versions, and again classical linear logic embeds into intuitionistic. And it doesn't stop there. Linear logic can be embedded in ordered logic, and ordered logic into the logic of bunched implications. For all I know there are even finer-grained logics out there. But doing all of mathematics in the logic of bunched implications would be an impractical nightmare, I think. I tend to prefer choosing whether to work classically or constructive (or linearly, or orderedly) according to whether it illuminates a relevant part of the problem. Sometimes you care about constructivity; sometimes you don't. If you don't, then don't waste your time trying to do the proof constructively. The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it! :)
- enriquto 8y ago
  > The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it! This sounds more like a motivation than like a trouble.
- danharaj 8y ago
  > classical linear logic embeds into intuitionistic. Wait, really? As I understand it there are things provable in LL that can't be proved in ILL. Can't find the citation though. It should be noted that double negation translations are more complicated at the proof level even though they capture provability.

protonfish 8y ago

This is fascinating, but only if you hold faith in inherent truth of mathematical symbolism. Unfortunately, this seems to be the standard dogma of mathematicians, though I haven't seen significant evidence necessary to warrant this belief. If you understand mathematics and logic as merely a formalized language of symbols then you can judge those systems on certain qualities (complexity, clarity, expressiveness, etc.) but not "truth." The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.

popnroll 8y ago
I'm really clueless about logic and mathematics theory, but isn't this the Gödel's incompleteness theorem?
- protonfish 8y ago
  No, the incompleteness theorem only examines how formal systems relate to themselves, not to reality. It shows that no significantly expressive system can be designed that won't allow paradoxical statements.
  - mietek 8y ago
    > It shows that no significantly expressive system can be designed that won't allow paradoxical statements. The above is a complete misrepresentation of Gödel’s second incompleteness theorem. The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means. Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8]. All of these languages are designed to be consistent. Of course, implementation bugs do happen[9]. If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11]. [1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_conditions https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co... [2] Gödel’s second incompleteness theorem, https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theorems#Second_incompleteness_theorem https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor... [3] Dependent type, https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type [4] Total functional programming, https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming [5] Agda programming language, http://agda.readthedocs.io http://agda.readthedocs.io [6] Coq proof assistant, http://coq.inria.fr http://coq.inria.fr [7] Idris programming language, http://www.idris-lang.org http://www.idris-lang.org [8] Lean theorem prover, http://leanprover.github.io http://leanprover.github.io [9] The rise and fall of @proofmarket, https://twitter.com/i/moments/921153475836305408 https://twitter.com/i/moments/921153475836305408 [10] Friedman, D.P., Christiansen, D.T. (2018) ‘The Little Typer’, https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer [11] Turner, D. (2004) ‘Total Functional Programming’, http://www.jucs.org/jucs_10_7/total_functional_programming http://www.jucs.org/jucs_10_7/total_functional_programming

danbruc 8y ago

What exactly is the claim here with regard to the law of excluded middle? Maybe somewhat naively it seems rather obvious to me that the law of excluded middle can be true or false depending on what objects you are dealing with. Maybe not the best possible example but in classical mechanics a particle is either inside a region R or it is not inside region R while in quantum mechanics the particle may be inside region R or it may not be inside region R or it may be somewhat inside region R. It seems rather obvious that the logic you are using has to match the behavior of the objects you are applying the logic to or you will of course end up with wrong conclusions. If we change the example a bit, the particle is in region R with probability zero or the particle is in region R with a probability larger than zero, then we again have a case where the set of possibilities is nicely partitioned into two mutually exclusive and exhaustive sets, probability zero and probability not zero. But I guess I am missing something or there wouldn't be a lot of smart people fighting over the issue.

ratmice 8y ago
I believe there are a couple of different claims being made in the above, I went ahead and just made a gist with some proofs (in lean) that try and hit some of the points about usage of law of excluded middle, double negation translation you should be able to copy/paste it into https://leanprover.github.io/live/latest/ https://leanprover.github.io/live/latest/ https://gist.github.com/ratmice/21f069b5811d1c40911850cb690a5b5e https://gist.github.com/ratmice/21f069b5811d1c40911850cb690a...
- danbruc 8y ago
  Thanks for the effort but unfortunately for me the page just says running and nothing ever happens, especially no output at all. Not even for the small example included by default. But besides that I did not really want to make any claims and certainly nothing that could be easily addressed by a proof, I think. My point was more that one has to take care that the type of logic one uses has to fit together with the domain one wants to reason about with that logic. If in the domain you want to reason about the law of excluded middle does not hold or only does so in a non-straight forward way, then using a logic with law of excluded middle will at least be not as easy as it could be or even painful or in the worst case lead to wrong conclusions.

User23 8y ago

The invention of computing automata and the techniques required to program them, such as defining semantics, settles this issue concretely in favor of Hilbert.

joel_ms 8y ago
How so? I've always felt that intuitionism/constructivism were closer to theoretical computer science due to constructivism requiring you to produce (or compute) the what you're trying to prove.
- User23 8y ago
  Dijkstra and Scholten's https://www.amazon.com/Predicate-Calculus-Semantics-Monographs-Computer/dp/1461279240 https://www.amazon.com/Predicate-Calculus-Semantics-Monograp... is a good example of what I mean. The state space is far too large to show a program is correct by constructing all possible processes it could execute. Instead you must show that the program admits no incorrect processes whatsoever, and as far as I know mathematical formalism is the only possible way to do that. Of course if one just wants to make money, formal correctness is observably of absolutely no importance. And there's nothing wrong with wanting to make money!
  - Firadeoclus 8y ago
    From Wikipedia: > Brouwer the intuitionist in particular objected to the use of the Law of Excluded Middle over infinite sets It always seems to me that using the LEM over infinite sets is akin to claiming that all problems are decidable.