5 ms·

>His proof is fairly difficult to understand - it involves prime numbers, factorization, all this number theory. Actually, the textbook proof itself is not ver

>His proof is fairly difficult to understand - it involves prime numbers, factorization, all this number theory. Actually, the textbook proof itself is not very different from the presentation in this article, so not hard at all. The difficult part is in formalizing that you can write "a program that proves a program halts". To do so you have to encode it into the language of mathematics, and that is the painful part. To be clear: you have the paradox of the set that contains all sets that don't contain themselves. In naïve set theory, it is trivial to write down formally. However the Berry paradox is not a real paradox because there is no way to encode "The smallest positive integer not definable in under sixty letters". So the whole point of going through the encoding is to show that yes, we can encode what a provable statement, and thus the first 'paradox' is actually a crucial flaw in the mathematical theory, whereas the second is a flaw/paradox in human language, but does not mean anything. The computer world is not as strict, it's more squishy (human?) than mathematics.

skissane 5y ago
> However the Berry paradox is not a real paradox because there is no way to encode "The smallest positive integer not definable in under sixty letters". Why is a “way to encode” necessary for a paradox to be “real”? > So the whole point of going through the encoding is to show that yes, we can encode what a provable statement, and thus the first 'paradox' is actually a crucial flaw in the mathematical theory, whereas the second is a flaw/paradox in human language, but does not mean anything. How can you say something “does not mean anything” simply because it cannot be formalised? Since when is formalisability a prerequisite for meaningfulness?
- woolion 5y ago
  >How can you say something “does not mean anything” simply because it cannot be formalised? Since when is formalisability a prerequisite for meaningfulness? I'm wondering then, what you think is the interest of this theorem? The goal of Gödel was to create a metamathematics. You need to know what is a paradox of the theory or a paradox or not to know if it is correct. If you have a contradiction, you cannot believe anything that the theory proves. So the whole thing is ultimately about separating mathematical paradox from "other types" of paradoxes.
  - skissane 5y ago
    > I'm wondering then, what you think is the interest of this theorem? Well, it was a profound discovery about the limits of consistent formal systems, and of course it is interesting in that light. But, viewing that as profoundly interesting does not require one to adopt your apparent position that only the formalisable is "real". > If you have a contradiction, you cannot believe anything that the theory proves. Only with classical logic. With paraconsistent logic, you can believe things proven from inconsistent axioms. Classical logic includes the principle of explosion (ex contradictione quodlibet, from a contradiction anything follows); so inconsistent theories immediately collapse into trivial ones, and trivial theories are of course utterly useless. But since paraconsistent logic rejects the principle of explosion, inconsistent theories do not collapse into triviality, and thus may be useful in spite of their inconsistency.
    - woolion 5y ago
      Can you explain to me what is the "realness" of Berry's paradox?
      - skissane 5y ago
        Classical logic is a poor model of natural language and informal human reasoning. Paraconsistent logics are much more accurate formal models of informal human reasoning and natural language, and much closer to them in power. One argument for this: material implication is a poor model of how implication works in natural language, as the well-known paradoxes of material implication show. With modal logic, we can introduce strict implication, which performs better, but still falls short as an accurate model of natural language implication, as shown by the paradoxes of strict implication. Relevant logics (aka relevance logics) avoid the paradoxes of strict implication as well. But relevant logics are also paraconsistent. Using an appropriate paraconsistent logic, Berry's paradox can be turned into a formal paradox, and such a formal paradox can be viewed as a straight-forward formalisation of the informal Berry's paradox. Attempts to formalise Berry's paradox using classical logic fail to produce a paradox, because classical logic lacks sufficient self-referential power – classical logic cannot cope with inconsistency, so classical formal systems must have their powers of self-reference neutered – compared to natural language – to prevent self-referential paradoxes – and those restrictions also prevent a formal Berry's paradox from existing. Paraconsistent logic is far better at handling inconsistency, so it does not have to restrict self-reference, and becomes much closer to natural language in power – and Berry's paradox becomes a formal paradox as well as an informal one. So, given the above – in what sense is Berry's paradox not "real"?
- dchftcs 5y ago
  The basic constraint is that if you want to prove something based on purely logical statements, you need to express the problem precisely enough for pure logic, that is without any wiggle room open to vauge human interpretation, and the notions you use have precise meaning. If not, your problem can't be solved by pure logic, but only by more wishy washy handwavy arguments, from which you can't derive any insights with logical certainty. You might be able to derive philosophical or empirical meaning from an interpretation of some non-precise statement, but you shouldn't hope that such an interpretation is a valid mathematical theorem.
  - skissane 5y ago
    > The basic constraint is that if you want to prove something based on purely logical statements, you need to express the problem precisely enough for pure logic, that is without any wiggle room open to vauge human interpretation, and the notions you use have precise meaning. If not, your problem can't be solved by pure logic, but only by more wishy washy handwavy arguments, from which you can't derive any insights with logical certainty. I think when you say "pure", you actually mean "formal" or "symbolic" or "mathematical". Many believe that there is much more to logic than a mere formalism – although that itself is a major point of contention in the philosophy of logic. > You might be able to derive philosophical or empirical meaning from an interpretation of some non-precise statement, but you shouldn't hope that such an interpretation is a valid mathematical theorem. Berry's paradox may not be a mathematical paradox – but that doesn't show it is not a paradox. And, even if it is not a mathematical paradox, it nonetheless made a valuable contribution to mathematics, by inspiring the construction of formal analogues, some of which turned out not to be paradoxical (but nonetheless interesting). However, I don't think it necessarily follows, that just because those formal analogues turned out not to be actual paradoxes, that its natural language version cannot be a real paradox. And, some argue there are formal analogues which are genuine paradoxes – see for example https://ojs.victoria.ac.nz/ajl/article/download/4972/4634/7302 https://ojs.victoria.ac.nz/ajl/article/download/4972/4634/73...
    - mannykannot 5y ago
      > some argue there are formal analogues which are genuine paradoxes... Isn't this getting a bit circular, as it seems to be using the presumed existence of a formal analogue to justify the informal Berry's paradox? If it has a paradoxical formal analogue, then it does not stand as an example of a useful yet unavoidably informal paradox. Also, given that there seem to be more than one plausible formal analogue, not all of which are paradoxes, does the dispute not just re-form around which is the real formal analogue? That's what seems to be happening in the exchange of papers from which your example was taken.
OscarCunningham 5y ago
>>His proof is fairly difficult to understand - it involves prime numbers, factorization, all this number theory. >Actually, the textbook proof itself is not very different from the presentation in this article, so not hard at all. The difficult part is in formalizing that you can write "a program that proves a program halts". To do so you have to encode it into the language of mathematics, and that is the painful part. I think the difficulty of understanding Gödel's proof has changed with the rise of computers. For him the difficult part of the proof was showing that you can represent text as numbers and manipulate it using arithmetic operations. These days we all do that for our day jobs. So you can skip over the part that Gödel thought was difficult in one line, and focus your attention on the clever use of self-reference. Also these days we would probably use a binary encoding instead of Gödel's encoding via prime factorisation, so even if you did want to explain the details of the encoding the amount of number theory would be reduced.
- knome 5y ago
  The prime factorization ensures that every combination of terms creates a unique value. How does binary do so?
  - Strilanc 5y ago
    Typically either with length prefixing (what binary protocols do) or with escaping/quoting (what text protocols do). For example, JSON assigns a unique bit sequence to every possible list of strings by using '"' and ',' as separators and '\' as an escape signal to disable the special meaning of the next character.
- woolion 5y ago
  Gödel's method starting with encoding parentheses, and bound variables, i.e. purely syntactical artifacts. It's a good example where you could do away with this, using e.g. de Bruijn indices -- exactly as you'd suggest switching encoding to binary. It is another layer of (mostly incidental) complexity yet in the end this complexity has to be addressed -- one choice of base does not change the number. When you write programs, you don't prove them correct, and you go down to assembly instructions, which is essentially what Gödel did.

skissane 5y ago

> However the Berry paradox is not a real paradox because there is no way to encode "The smallest positive integer not definable in under sixty letters". Why is a “way to encode” necessary for a paradox to be “real”? > So the whole point of going through the encoding is to show that yes, we can encode what a provable statement, and thus the first 'paradox' is actually a crucial flaw in the mathematical theory, whereas the second is a flaw/paradox in human language, but does not mean anything. How can you say something “does not mean anything” simply because it cannot be formalised? Since when is formalisability a prerequisite for meaningfulness?

woolion 5y ago
>How can you say something “does not mean anything” simply because it cannot be formalised? Since when is formalisability a prerequisite for meaningfulness? I'm wondering then, what you think is the interest of this theorem? The goal of Gödel was to create a metamathematics. You need to know what is a paradox of the theory or a paradox or not to know if it is correct. If you have a contradiction, you cannot believe anything that the theory proves. So the whole thing is ultimately about separating mathematical paradox from "other types" of paradoxes.
- skissane 5y ago
  > I'm wondering then, what you think is the interest of this theorem? Well, it was a profound discovery about the limits of consistent formal systems, and of course it is interesting in that light. But, viewing that as profoundly interesting does not require one to adopt your apparent position that only the formalisable is "real". > If you have a contradiction, you cannot believe anything that the theory proves. Only with classical logic. With paraconsistent logic, you can believe things proven from inconsistent axioms. Classical logic includes the principle of explosion (ex contradictione quodlibet, from a contradiction anything follows); so inconsistent theories immediately collapse into trivial ones, and trivial theories are of course utterly useless. But since paraconsistent logic rejects the principle of explosion, inconsistent theories do not collapse into triviality, and thus may be useful in spite of their inconsistency.
  - woolion 5y ago
    Can you explain to me what is the "realness" of Berry's paradox?
    - skissane 5y ago
      Classical logic is a poor model of natural language and informal human reasoning. Paraconsistent logics are much more accurate formal models of informal human reasoning and natural language, and much closer to them in power. One argument for this: material implication is a poor model of how implication works in natural language, as the well-known paradoxes of material implication show. With modal logic, we can introduce strict implication, which performs better, but still falls short as an accurate model of natural language implication, as shown by the paradoxes of strict implication. Relevant logics (aka relevance logics) avoid the paradoxes of strict implication as well. But relevant logics are also paraconsistent. Using an appropriate paraconsistent logic, Berry's paradox can be turned into a formal paradox, and such a formal paradox can be viewed as a straight-forward formalisation of the informal Berry's paradox. Attempts to formalise Berry's paradox using classical logic fail to produce a paradox, because classical logic lacks sufficient self-referential power – classical logic cannot cope with inconsistency, so classical formal systems must have their powers of self-reference neutered – compared to natural language – to prevent self-referential paradoxes – and those restrictions also prevent a formal Berry's paradox from existing. Paraconsistent logic is far better at handling inconsistency, so it does not have to restrict self-reference, and becomes much closer to natural language in power – and Berry's paradox becomes a formal paradox as well as an informal one. So, given the above – in what sense is Berry's paradox not "real"?
dchftcs 5y ago
The basic constraint is that if you want to prove something based on purely logical statements, you need to express the problem precisely enough for pure logic, that is without any wiggle room open to vauge human interpretation, and the notions you use have precise meaning. If not, your problem can't be solved by pure logic, but only by more wishy washy handwavy arguments, from which you can't derive any insights with logical certainty. You might be able to derive philosophical or empirical meaning from an interpretation of some non-precise statement, but you shouldn't hope that such an interpretation is a valid mathematical theorem.
- skissane 5y ago
  > The basic constraint is that if you want to prove something based on purely logical statements, you need to express the problem precisely enough for pure logic, that is without any wiggle room open to vauge human interpretation, and the notions you use have precise meaning. If not, your problem can't be solved by pure logic, but only by more wishy washy handwavy arguments, from which you can't derive any insights with logical certainty. I think when you say "pure", you actually mean "formal" or "symbolic" or "mathematical". Many believe that there is much more to logic than a mere formalism – although that itself is a major point of contention in the philosophy of logic. > You might be able to derive philosophical or empirical meaning from an interpretation of some non-precise statement, but you shouldn't hope that such an interpretation is a valid mathematical theorem. Berry's paradox may not be a mathematical paradox – but that doesn't show it is not a paradox. And, even if it is not a mathematical paradox, it nonetheless made a valuable contribution to mathematics, by inspiring the construction of formal analogues, some of which turned out not to be paradoxical (but nonetheless interesting). However, I don't think it necessarily follows, that just because those formal analogues turned out not to be actual paradoxes, that its natural language version cannot be a real paradox. And, some argue there are formal analogues which are genuine paradoxes – see for example https://ojs.victoria.ac.nz/ajl/article/download/4972/4634/7302 https://ojs.victoria.ac.nz/ajl/article/download/4972/4634/73...
  - mannykannot 5y ago
    > some argue there are formal analogues which are genuine paradoxes... Isn't this getting a bit circular, as it seems to be using the presumed existence of a formal analogue to justify the informal Berry's paradox? If it has a paradoxical formal analogue, then it does not stand as an example of a useful yet unavoidably informal paradox. Also, given that there seem to be more than one plausible formal analogue, not all of which are paradoxes, does the dispute not just re-form around which is the real formal analogue? That's what seems to be happening in the exchange of papers from which your example was taken.

OscarCunningham 5y ago

>>His proof is fairly difficult to understand - it involves prime numbers, factorization, all this number theory. >Actually, the textbook proof itself is not very different from the presentation in this article, so not hard at all. The difficult part is in formalizing that you can write "a program that proves a program halts". To do so you have to encode it into the language of mathematics, and that is the painful part. I think the difficulty of understanding Gödel's proof has changed with the rise of computers. For him the difficult part of the proof was showing that you can represent text as numbers and manipulate it using arithmetic operations. These days we all do that for our day jobs. So you can skip over the part that Gödel thought was difficult in one line, and focus your attention on the clever use of self-reference. Also these days we would probably use a binary encoding instead of Gödel's encoding via prime factorisation, so even if you did want to explain the details of the encoding the amount of number theory would be reduced.

knome 5y ago
The prime factorization ensures that every combination of terms creates a unique value. How does binary do so?
- Strilanc 5y ago
  Typically either with length prefixing (what binary protocols do) or with escaping/quoting (what text protocols do). For example, JSON assigns a unique bit sequence to every possible list of strings by using '"' and ',' as separators and '\' as an escape signal to disable the special meaning of the next character.
woolion 5y ago
Gödel's method starting with encoding parentheses, and bound variables, i.e. purely syntactical artifacts. It's a good example where you could do away with this, using e.g. de Bruijn indices -- exactly as you'd suggest switching encoding to binary. It is another layer of (mostly incidental) complexity yet in the end this complexity has to be addressed -- one choice of base does not change the number. When you write programs, you don't prove them correct, and you go down to assembly instructions, which is essentially what Gödel did.