5 ms·

>> For me it just means that you need to put additional restrictions of what you can do in math so that kind of statement is excluded from math. The thing abou

>> For me it just means that you need to put additional restrictions of what you can do in math so that kind of statement is excluded from math. The thing about Godel's proof is that he didn't just come up with one example of a "this statement is not provable" sentence; he proved that any sufficiently complex math system will have unprovable sentences (some true, some false, some you'll never be able to know). And "sufficently complex" is not all that complex! So if you want to be able to do calculus, or even most arithmetic, you can't just "put additional restrictions ... so that kind of statement is excluded from math."

scotty79 5y ago
Sure you can. Just ban the concept of provability from your math language (or some elements that lead to it). Same way like they banned weird kinds of sets and started talking about set families instead of sets of sets. If you declare that set being its own element is nonsensical statement you no longer have a paradox with set of sets that are not their own elements. Base assumption of math is that correctly constructed mathematical statement is not nonsensical. It must be true or false or not determined by current set of axioms. And I think that assumption of sensibility of any math statement leads to paradoxes.
- magneticnorth 5y ago
  In the case of set theory, you can exclude sets of sets and still have an extremely rich and deep mathematical theory of sets. (But it is definitely still incomplete - for example ZFC can't prove the continuum hypothesis, and if you take the continuum hypothesis or its negation as an axiom, there are still infinitely more unprovable statements in that mathematical theory) In the case of Godel's incompleteness theorem, excluding the amount of math you need to in order to avoid unprovable sentences leaves you with only very simple axiom systems. If your mathematics is complete enough to even do simple arithmetic (i.e. Peano arithmetic), then there are unprovable statements. It's not as easy a fix as Russell's set theory paradox, which is why it's an important and foundational aspect of nearly all mathematics even today.
- magneticnorth 5y ago
  Perhaps a better explanation - it's similar to the halting problem in computer science. There are programs p where "Program p halts on input x" is unprovable (equivalently there is no computable way to determine which p,x halt), and the key is that we have no way of knowing which programs p and x this is true for, of the ones we don't yet have proofs/halt-prediction-programs about. You may want to argue that this can be "solved" by never letting programs take other programs as input, which isn't wrong, exactly, but you're left with not very much you can compute in that paradigm for computation.
- rssoconnor 5y ago
  A set of elements that lead to the concept of provability[1] are: 0, 1, addition, multiplication, quotient, remainder and inequality. Quotient and remainder are definable implicitly in the language of number theory (the language of Peano Arithmetic). Sometimes inequality is explicitly defined, and sometimes it is implicitly defined using exists and addition. From these elements you can go on to define the Goedel beta function, which allows you to encode lists of numbers and extract the nth element from such an encoding. From there you can go on to define arbitrary primitive recursion (and even more). From there provability can be defined as a primitive recursive function. I'm not sure which element there you want to ban. Maybe you want to ban multiplication? [1]http://r6.ca/blog/20190223T161625Z.html http://r6.ca/blog/20190223T161625Z.html
  - scotty79 5y ago
    You can ban the way how you combine the elements. When you reach the step where you define primitive recursion you could say that statements that involve recursion of depth of more than hundred are not true or false or undecided but just meaningless and excluded from mathematical consideration. I know it sounds silly but the statements that prevent infinite recursion in programming languages often do look silly. They look like a hackish stopgap that doesn't fit the pristine recursive algorithm. Yet they work and protect you at the cost of the recursion not to be able to correctly deal wit stuff that would need a deeper recursion.
    - rssoconnor 5y ago
      These statements are not phrased in terms of recursion. Once you inline all the definitions then they are phrased in terms of arithmetic. That's the whole point of all this! Have a look at http://tachyos.org/godel/Godel_statement.html http://tachyos.org/godel/Godel_statement.html and tell me exactly why that formula is banned? Is the formula too long? To many uses of multiplication? Give me a decision procedure.
      - scotty79 5y ago
        Yes. To avoid paradoxes you need to limit nesting, inlined or not. This statement reeks of uncontrolled infinities with all the quantifiers and I don't even know what some symbols mean like 0''' Because of my ignorance I can't point the exact problem here but I don't think it is the multiplication. Alternatively you might just redefine the concept of something being true such that you only provable things are true and unprovable ones are either false, undecidable or nonsensical. And nonsensical thing is defined as a statement thats unprovable but seemingly true. I think there many ways to fix this just by restricting yourself with how you define things. And it's not about restricting arithmetc because that's not the core of the issue, that's just the (simplest?) example.
runT1ME 5y ago
I think it's important to point out that you can do calculus and arithmetic and only construct proofs that are provable. The possibility of deriving unprovable but true statements in an axiomatic system doesn't mean they're common or you can't prove all the satatements one has encountered thus far.
Animats 5y ago
He proved that any sufficiently complex math system will have unprovable sentences. That's mostly because "sufficiently complex" is defined by mathematicians, not computer scientists. In particular, it includes infinities, which do not exist in the physical universe. Godel's proof requires allowing unlimited depth recursion, which does not exist in the physical world. The halting problem is decidable for any deterministic system with finite memory. Either you halt, or you repeat a state. This covers most real-world computer programs. There's a useful subset of arithmetic and logic which is completely decidable. It contains integer addition, subtraction, multiplication by constants, and all the logic operators. This covers most subscript checking in programs, which is quite useful. You can probably add modular arithmetic with a fixed upper bound to that subset. Now, some systems may require very large amounts of work to prove, but that's different from being undecidable. "Very large" is not infinite. That heads us off into the theory of lower bounds, P = NP, and all that, where there are still many open questions. This knocks out many of the sillier claims about undecidability making something impossible in the real world.
- alok-g 5y ago
  Exactly! For the same reason, when someone uses halting problem to 'explain' why their program freezes, they are wrong. They are wrong on multiple counts actually. For pure mathematics, this stuff is relevant. For all practical purposes, it is not (as far as infinite-precision analog memories are not involved).
- anon_tor_12345 5y ago
  >In particular, it includes infinities, which do not exist in the physical universe. Bold claim. As far as I know the centers of black holes are indeed non-removable singularities of (some) solutions to GR equations. What's funny is I had a debate with a cosmologist where I was on your side of the debate because he was a mathematical realist (and therefore forced to reconcile the same divergences with the "reality" of math).
- rssoconnor 5y ago
  > The halting problem is decidable for any deterministic system with finite memory. Either you halt, or you repeat a state. This covers most real-world computer programs. Problem being that you cannot decide whether a system with such finite memory halts without using another different system that has even more memory. And if that larger system doesn't "real-world" exist, can you truly say that the halting problem is decidable?

scotty79 5y ago

Sure you can. Just ban the concept of provability from your math language (or some elements that lead to it). Same way like they banned weird kinds of sets and started talking about set families instead of sets of sets. If you declare that set being its own element is nonsensical statement you no longer have a paradox with set of sets that are not their own elements. Base assumption of math is that correctly constructed mathematical statement is not nonsensical. It must be true or false or not determined by current set of axioms. And I think that assumption of sensibility of any math statement leads to paradoxes.

magneticnorth 5y ago
In the case of set theory, you can exclude sets of sets and still have an extremely rich and deep mathematical theory of sets. (But it is definitely still incomplete - for example ZFC can't prove the continuum hypothesis, and if you take the continuum hypothesis or its negation as an axiom, there are still infinitely more unprovable statements in that mathematical theory) In the case of Godel's incompleteness theorem, excluding the amount of math you need to in order to avoid unprovable sentences leaves you with only very simple axiom systems. If your mathematics is complete enough to even do simple arithmetic (i.e. Peano arithmetic), then there are unprovable statements. It's not as easy a fix as Russell's set theory paradox, which is why it's an important and foundational aspect of nearly all mathematics even today.
magneticnorth 5y ago
Perhaps a better explanation - it's similar to the halting problem in computer science. There are programs p where "Program p halts on input x" is unprovable (equivalently there is no computable way to determine which p,x halt), and the key is that we have no way of knowing which programs p and x this is true for, of the ones we don't yet have proofs/halt-prediction-programs about. You may want to argue that this can be "solved" by never letting programs take other programs as input, which isn't wrong, exactly, but you're left with not very much you can compute in that paradigm for computation.
rssoconnor 5y ago
A set of elements that lead to the concept of provability[1] are: 0, 1, addition, multiplication, quotient, remainder and inequality. Quotient and remainder are definable implicitly in the language of number theory (the language of Peano Arithmetic). Sometimes inequality is explicitly defined, and sometimes it is implicitly defined using exists and addition. From these elements you can go on to define the Goedel beta function, which allows you to encode lists of numbers and extract the nth element from such an encoding. From there you can go on to define arbitrary primitive recursion (and even more). From there provability can be defined as a primitive recursive function. I'm not sure which element there you want to ban. Maybe you want to ban multiplication? [1]http://r6.ca/blog/20190223T161625Z.html http://r6.ca/blog/20190223T161625Z.html
- scotty79 5y ago
  You can ban the way how you combine the elements. When you reach the step where you define primitive recursion you could say that statements that involve recursion of depth of more than hundred are not true or false or undecided but just meaningless and excluded from mathematical consideration. I know it sounds silly but the statements that prevent infinite recursion in programming languages often do look silly. They look like a hackish stopgap that doesn't fit the pristine recursive algorithm. Yet they work and protect you at the cost of the recursion not to be able to correctly deal wit stuff that would need a deeper recursion.
  - rssoconnor 5y ago
    These statements are not phrased in terms of recursion. Once you inline all the definitions then they are phrased in terms of arithmetic. That's the whole point of all this! Have a look at http://tachyos.org/godel/Godel_statement.html http://tachyos.org/godel/Godel_statement.html and tell me exactly why that formula is banned? Is the formula too long? To many uses of multiplication? Give me a decision procedure.
    - scotty79 5y ago
      Yes. To avoid paradoxes you need to limit nesting, inlined or not. This statement reeks of uncontrolled infinities with all the quantifiers and I don't even know what some symbols mean like 0''' Because of my ignorance I can't point the exact problem here but I don't think it is the multiplication. Alternatively you might just redefine the concept of something being true such that you only provable things are true and unprovable ones are either false, undecidable or nonsensical. And nonsensical thing is defined as a statement thats unprovable but seemingly true. I think there many ways to fix this just by restricting yourself with how you define things. And it's not about restricting arithmetc because that's not the core of the issue, that's just the (simplest?) example.

runT1ME 5y ago

I think it's important to point out that you can do calculus and arithmetic and only construct proofs that are provable. The possibility of deriving unprovable but true statements in an axiomatic system doesn't mean they're common or you can't prove all the satatements one has encountered thus far.

Animats 5y ago

He proved that any sufficiently complex math system will have unprovable sentences. That's mostly because "sufficiently complex" is defined by mathematicians, not computer scientists. In particular, it includes infinities, which do not exist in the physical universe. Godel's proof requires allowing unlimited depth recursion, which does not exist in the physical world. The halting problem is decidable for any deterministic system with finite memory. Either you halt, or you repeat a state. This covers most real-world computer programs. There's a useful subset of arithmetic and logic which is completely decidable. It contains integer addition, subtraction, multiplication by constants, and all the logic operators. This covers most subscript checking in programs, which is quite useful. You can probably add modular arithmetic with a fixed upper bound to that subset. Now, some systems may require very large amounts of work to prove, but that's different from being undecidable. "Very large" is not infinite. That heads us off into the theory of lower bounds, P = NP, and all that, where there are still many open questions. This knocks out many of the sillier claims about undecidability making something impossible in the real world.

alok-g 5y ago
Exactly! For the same reason, when someone uses halting problem to 'explain' why their program freezes, they are wrong. They are wrong on multiple counts actually. For pure mathematics, this stuff is relevant. For all practical purposes, it is not (as far as infinite-precision analog memories are not involved).
anon_tor_12345 5y ago
>In particular, it includes infinities, which do not exist in the physical universe. Bold claim. As far as I know the centers of black holes are indeed non-removable singularities of (some) solutions to GR equations. What's funny is I had a debate with a cosmologist where I was on your side of the debate because he was a mathematical realist (and therefore forced to reconcile the same divergences with the "reality" of math).
rssoconnor 5y ago
> The halting problem is decidable for any deterministic system with finite memory. Either you halt, or you repeat a state. This covers most real-world computer programs. Problem being that you cannot decide whether a system with such finite memory halts without using another different system that has even more memory. And if that larger system doesn't "real-world" exist, can you truly say that the halting problem is decidable?