4 ms·

People bringing up GIT (Goedel's Incompleteness Theorem) don't understand that GIT is a limitation of formal logic which affects human mathematicians as much as

People bringing up GIT (Goedel's Incompleteness Theorem) don't understand that GIT is a limitation of formal logic which affects human mathematicians as much as computer-based mathematicians. Both humans and computers are forced to work with a recursively enumerable set of axioms when constructing mathematical proofs, and so therefore are bound by the same limitations. Also, if you can check a proof, then you can certainly automatically construct a proof, merely by dove-tailing over all possible proofs and checking whether they're correct and imply the desired conjecture. In other words, using GIT when discussing proof automation is irrelevant.

__MatrixMan__ 6y ago
I agree that GIT limits human provers as much as it limits automated ones, but I don't agree that it's irrelevant to the issue. A human mathematician can lean on intuition in ways that a computer can't. Given a theorem that resists proof, a human might develop a feel for whether it's worth continuing to prove via conventional means or whether the troublesome territory is better approached from a different axiom set. That intuition may be driven by the problematic theorem being one of the true-but-unprovable ones that Godel assures us exists without that cause being apparent to the mathematician. The automated prover, on the other hand, faces a halting problem here. Unless it is given some explicit reason to expect that the target is not attainable, it might try forever. So such a prover might need to be GIT-aware in ways that a human doesn't.
- ampdepolymerase 6y ago
  That's where ML comes in, to provide the 'intuition' for pruning the search space.
- jackfoxy 6y ago
  As a human this explanation is emotionally satisfying. It appeals to my sense of human exceptionalism. However how many true but unprovable theorems do we know about? Has anyone ever bothered to compile a list of true but unprovable under the axioms xyz? I would think it is exceedingly hard to manage such research as every axiom set xyz would require companion axioms abc to be provable, and such theorems (at least the non-trivial interesting ones) are possibly hard to reach. This intuition for unprovableness may just be a mechanism for escaping local minima that gets lucky often enough.
  - wisnesky 6y ago
    Many such lists exist. For example: https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC https://en.wikipedia.org/wiki/List_of_statements_independent...
    - __MatrixMan__ 6y ago
      That's certainly true, but Godel-type unprovability is separate from logical independence, and indeed much harder to make lists of. My earlier point is not that we could know for sure that our struggles are due to being up against such a wall--just that our ability to suspect as much is relevant to how we allocate our time.
      - wisnesky 6y ago
        Oh, such as a list of statements unprovable under a specific Godel numbering? Definitely much more difficult - I never saw such a list in grad school, although I wouldn't rule out the existence of one.
      - p0llard 6y ago
        > Godel-type unprovability is separate from logical independence What do you mean by this? The Goedel sentence of a system is logically independent from the system by the standard meaning of "logical independence".
  - p0llard 6y ago
    > true but unprovable under the axioms xyz? Careful: we don't really talk about things which are "true but unprovable" in first-order logics. By Goedel's completeness theorem, if a statement is true in all models of a first-order theory then it is provable. For any recursively axiomisable first-order theory of sufficient complexity, there exists some sentence which isn't provable [Goedel's First Incompleteness Theorem]: by contraposition of completeness, there exist models of the theory where the sentence is true, and models where the sentence is false. So when you say "true but unprovable", you're probably talking about truth in the so-called "intended model": if something is independent of the first-order system (e.g. ZF) you're using as a foundation of mathematics, then you get to decide whether it's true or not! Once you've proven independence via e.g. forcing, it's up to you to decide whether the sentence should hold in your intended model: then you can add the appropriate axiom to your system. Choice is independent from ZF: most mathematicians are OK with choice, so they chose to work in ZFC, but some aren't. Neither is "more valid" or "more true" from a purely logical perspective.
- sukilot 6y ago
  That's simply not true. The kinds of statements that are unprovable aren't "intuitive". Gödel provided an algorithm for creating them!
  - __MatrixMan__ 6y ago
    But there's no reason to believe that his algorithm gives us all of them. Nobody has proven, for instance, that the Goldbach conjecture is unprovable, but the collective intuition of the community of number theorists is such that nobody spends much time trying to prove it anymore. What, aside from some coded-in GIT awareness-would lead an automated prover to do the same?
    - tialaramex 6y ago
      Why can't an automated prover have intuition? Today's automated provers don't, but then not so many years ago the successful computer chess players were all these boring rules-based brute force engines. And then DeepMind showed that a very different approach is better.
- didibus 6y ago
  One could argue human intuition is just statistical sampling. In effect, we might not be able to prove something, but we've observed that when used "assumed to be true" in other contexts, it seems to yield our expected result. I don't see why we couldn't build a similar system of intuition into a computer as well.
  - username90 6y ago
    > One could argue human intuition is just statistical sampling. Human intuition lets us walk and drive cars. It has proven really hard to replicate using computers. I really doubt we will solve this any time soon.
    - whatshisface 6y ago
      Human intuition can also add small numbers and recognize faces, and computers can do those already. Computers replicating all of human intuition is not a prerequisite for computers beating one aspect of human intuition.
alquemist 6y ago
True. Yet humans are embodied beings in a physical world. This affects their mathematical taste in at least two ways. Humans will prefer axiomatic systems / problem spaces that have some bearing onto the physical world. Humans will also prefer axiomatic systems / problem spaces that have some match to their sensorial systems, and the sensorial systems are shaped by the physical world. That being said, we are not too far from embodied computers, coming online soon as autonomous cars and autonomous killer drones. While this will not immediately give raise to physical biases in computer mathematicians, computers will become, for all intents and purposes, subject to the same physical reality which shapes humans.
- sukilot 6y ago
  You are describing (some of) physics, not math. Most of math is already far beyond human physical senses, and theoretical physics largely is too.
  - whatshisface 6y ago
    It's all still based on intuitive concepts like "sets" and "integers." Furthermore, inference rules are all based on the ones we use every day. You could have "alien logic" if you wanted but nobody seems to be very interested. Of course this has no bearing on computer proofs because you can tell the computer what your preferences are.
zitterbewegung 6y ago
This is a good time to illustrate that you can prove SOME programs can terminate. The halting problem doesn't limit you in proving that the following loop will halt or not: for x in range(0,10): x = x + 1 Microsoft research even had(has?) a program that attempts to prove functions that halt and they called in the Terminator. See https://cstheory.stackexchange.com/questions/39932/practical-approaches-to-solving-whether-programs-will-halt/39933#39933 https://cstheory.stackexchange.com/questions/39932/practical...
- deleted 6y ago
  [deleted]
deleted 6y ago
[deleted]
bawolff 6y ago
NP completeness seems much more relavent than GIT to me (still not really fully relavent. The question is can computers rivial humans, not can they prove all provable theorems in reasonable time, since clearly humans cant do that)

__MatrixMan__ 6y ago

I agree that GIT limits human provers as much as it limits automated ones, but I don't agree that it's irrelevant to the issue. A human mathematician can lean on intuition in ways that a computer can't. Given a theorem that resists proof, a human might develop a feel for whether it's worth continuing to prove via conventional means or whether the troublesome territory is better approached from a different axiom set. That intuition may be driven by the problematic theorem being one of the true-but-unprovable ones that Godel assures us exists without that cause being apparent to the mathematician. The automated prover, on the other hand, faces a halting problem here. Unless it is given some explicit reason to expect that the target is not attainable, it might try forever. So such a prover might need to be GIT-aware in ways that a human doesn't.

ampdepolymerase 6y ago
That's where ML comes in, to provide the 'intuition' for pruning the search space.
jackfoxy 6y ago
As a human this explanation is emotionally satisfying. It appeals to my sense of human exceptionalism. However how many true but unprovable theorems do we know about? Has anyone ever bothered to compile a list of true but unprovable under the axioms xyz? I would think it is exceedingly hard to manage such research as every axiom set xyz would require companion axioms abc to be provable, and such theorems (at least the non-trivial interesting ones) are possibly hard to reach. This intuition for unprovableness may just be a mechanism for escaping local minima that gets lucky often enough.
- wisnesky 6y ago
  Many such lists exist. For example: https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC https://en.wikipedia.org/wiki/List_of_statements_independent...
  - __MatrixMan__ 6y ago
    That's certainly true, but Godel-type unprovability is separate from logical independence, and indeed much harder to make lists of. My earlier point is not that we could know for sure that our struggles are due to being up against such a wall--just that our ability to suspect as much is relevant to how we allocate our time.
    - wisnesky 6y ago
      Oh, such as a list of statements unprovable under a specific Godel numbering? Definitely much more difficult - I never saw such a list in grad school, although I wouldn't rule out the existence of one.
    - p0llard 6y ago
      > Godel-type unprovability is separate from logical independence What do you mean by this? The Goedel sentence of a system is logically independent from the system by the standard meaning of "logical independence".
- p0llard 6y ago
  > true but unprovable under the axioms xyz? Careful: we don't really talk about things which are "true but unprovable" in first-order logics. By Goedel's completeness theorem, if a statement is true in all models of a first-order theory then it is provable. For any recursively axiomisable first-order theory of sufficient complexity, there exists some sentence which isn't provable [Goedel's First Incompleteness Theorem]: by contraposition of completeness, there exist models of the theory where the sentence is true, and models where the sentence is false. So when you say "true but unprovable", you're probably talking about truth in the so-called "intended model": if something is independent of the first-order system (e.g. ZF) you're using as a foundation of mathematics, then you get to decide whether it's true or not! Once you've proven independence via e.g. forcing, it's up to you to decide whether the sentence should hold in your intended model: then you can add the appropriate axiom to your system. Choice is independent from ZF: most mathematicians are OK with choice, so they chose to work in ZFC, but some aren't. Neither is "more valid" or "more true" from a purely logical perspective.
sukilot 6y ago
That's simply not true. The kinds of statements that are unprovable aren't "intuitive". Gödel provided an algorithm for creating them!
- __MatrixMan__ 6y ago
  But there's no reason to believe that his algorithm gives us all of them. Nobody has proven, for instance, that the Goldbach conjecture is unprovable, but the collective intuition of the community of number theorists is such that nobody spends much time trying to prove it anymore. What, aside from some coded-in GIT awareness-would lead an automated prover to do the same?
  - tialaramex 6y ago
    Why can't an automated prover have intuition? Today's automated provers don't, but then not so many years ago the successful computer chess players were all these boring rules-based brute force engines. And then DeepMind showed that a very different approach is better.
didibus 6y ago
One could argue human intuition is just statistical sampling. In effect, we might not be able to prove something, but we've observed that when used "assumed to be true" in other contexts, it seems to yield our expected result. I don't see why we couldn't build a similar system of intuition into a computer as well.
- username90 6y ago
  > One could argue human intuition is just statistical sampling. Human intuition lets us walk and drive cars. It has proven really hard to replicate using computers. I really doubt we will solve this any time soon.
  - whatshisface 6y ago
    Human intuition can also add small numbers and recognize faces, and computers can do those already. Computers replicating all of human intuition is not a prerequisite for computers beating one aspect of human intuition.

alquemist 6y ago

True. Yet humans are embodied beings in a physical world. This affects their mathematical taste in at least two ways. Humans will prefer axiomatic systems / problem spaces that have some bearing onto the physical world. Humans will also prefer axiomatic systems / problem spaces that have some match to their sensorial systems, and the sensorial systems are shaped by the physical world. That being said, we are not too far from embodied computers, coming online soon as autonomous cars and autonomous killer drones. While this will not immediately give raise to physical biases in computer mathematicians, computers will become, for all intents and purposes, subject to the same physical reality which shapes humans.

sukilot 6y ago
You are describing (some of) physics, not math. Most of math is already far beyond human physical senses, and theoretical physics largely is too.
- whatshisface 6y ago
  It's all still based on intuitive concepts like "sets" and "integers." Furthermore, inference rules are all based on the ones we use every day. You could have "alien logic" if you wanted but nobody seems to be very interested. Of course this has no bearing on computer proofs because you can tell the computer what your preferences are.

zitterbewegung 6y ago

This is a good time to illustrate that you can prove SOME programs can terminate. The halting problem doesn't limit you in proving that the following loop will halt or not: for x in range(0,10): x = x + 1 Microsoft research even had(has?) a program that attempts to prove functions that halt and they called in the Terminator. See https://cstheory.stackexchange.com/questions/39932/practical-approaches-to-solving-whether-programs-will-halt/39933#39933 https://cstheory.stackexchange.com/questions/39932/practical...

deleted 6y ago
[deleted]

deleted 6y ago

[deleted]

bawolff 6y ago

NP completeness seems much more relavent than GIT to me (still not really fully relavent. The question is can computers rivial humans, not can they prove all provable theorems in reasonable time, since clearly humans cant do that)