4 ms·

(...) Gödel-unprovable results are provable by humans. Are they? Certainly humans can recognise the undedicability of a "barber's paradox", like "this sentence

(...) Gödel-unprovable results are provable by humans. Are they? Certainly humans can recognise the undedicability of a "barber's paradox", like "this sentence is false", but that doesn't mean we can actually decide its truth value. We can spot undecidability, but not resolve it. Right? So what do you mean?

mannykannot 4y ago
I'm just being lazy and quoting a claim from Wikipedia's entry on the Penrose-Lucas argument, allegedly referencing "The Emperor's New Mind", but without any specific location within that book. It has been a while since I read it, and I may attempt to find a more precise summary of Penrose's claim (he has written about it extensively elsewhere, and so have many other people) but I can't do that immediately.
- benlivengood 4y ago
  I think that Penrose basically thinks it's useful that humans can heuristically step up from a logic system S to S+"statement X is true" in an almost-grounded way, but in reality we are all actually constrained by Godel, Tarski, etc. We just trick ourselves into assuming we can inductively keep stepping up from S+"X is true" indefinitely for any practical problem we encounter, but that is actually an ungrounded assumption. What seems like an even better formal solution is something like logical induction[0] that works over something like probabilities instead of truth/falsehood. It has an existence proof but not a constructive formalization, afaik, but maybe some recent progress has been made. 0: https://arxiv.org/abs/1609.03543 https://arxiv.org/abs/1609.03543
  - YeGoblynQueenne 4y ago
    Thanks for the paper, I need to read that. Much of my work is on inductive logic. >> I think that Penrose basically thinks it's useful that humans can heuristically step up from a logic system S to S+"statement X is true" in an almost-grounded way, but in reality we are all actually constrained by Godel, Tarski, etc. We just trick ourselves into assuming we can inductively keep stepping up from S+"X is true" indefinitely for any practical problem we encounter, but that is actually an ungrounded assumption. What you describe sounds to me more like logical abduction, rather than induction. Unfortunately, it's difficult to find simple explanations of what abduction is. One very rough and operational categorisation of modes of inference, as deductive, inductive or abductive, is as follows. Deduction is reasoning (as in automated theorem proving or rule-based systems), induction is learning (as in machine learning) and abduction is reasoning under uncertainty (as in probabilistic inference). There's a lot of confusion between what is abduction and what is induction, and the definitions of those in terms of "facts" and "rules" (coming from Peirce, who originally named "abduction" at least) is, for me, not very helpful. Another colloquial explanation is that abduction is a form of drawing conclusions from observations that isn't sound, so that conclusions are not necessarily true. I think that's where the association with probabilistic reasoning comes from, and that's why I think it describes better the kind of induction the linked paper is talking about. Anyway I'll have to read that, thanks.
- YeGoblynQueenne 4y ago
  Thanks for clarifying! Sorry for pouncing on that one little detail in your comment btw. Incompleteness vs. human reasoning is just something I think about on and off and your turn of phrase caught my attention.
mannykannot 4y ago
Update: One of the things I overlooked when using that quote is that it appears to say that we can prove the truth of any undecidable sentence, but Penrose's argument is made only with respect to the formalization, in a consistent and sufficiently strong [1] system S, of the sentence "the truth of this sentence is not provable in S". Both Lucas and Penrose claim that we will see that it is true (but, as it asserts, not provable in S) as the alternative leads to contradiction. This depends on S being consistent. Lucas and Penrose apparently suppose that any proposal for explaining thinking as a computational process would, ipso facto, cast a mind as a concrete instantiation of a consistent formal system. [2] Putting aside any thoughts of whether this is persuasive, I think this seems to be a case of Lucas and Penrose doing what they claim is uniquely human: thinking outside of the box of formal proof. More generally, almost none of human knowledge is couched as a formal proof of something or other, and almost none of it has been acquired that way. [1] More precisely, one in which a “moderate amount of number theory” can be proven. [2] J.R.Lucas, "Minds, Machines and Gödel", 1961.
- YeGoblynQueenne 4y ago
  >> Putting aside any thoughts of whether this is persuasive, I think this seems to be a case of Lucas and Penrose doing what they claim is uniquely human: thinking outside of the box of formal proof. More generally, almost none of human knowledge is couched as a formal proof of something or other, and almost none of it has been acquired that way. Well, except for all of mathematics :P Then again, it's useful to wonder what, exactly, is a formal proof, when derived by a human. My understanding of proofs (after having had to come up with several for my PhD research) is that the purpose of a proof is to convince a human that what the associated theorem states, is true. The human is first of all the person stating the theorem, so for example these days at least when I write down a theorem, the next thing I do is ask myself out loud "why do I think this is true?". Then I try to write it down in simple English, and then I try to put it in the standard format of an inductive proof, or a proof by refutation- and I do that only because those are proof structures that are well understood and they will cause the least confusion about what I mean. Even so I've got proofs wrong and I had reviewers pick out my mistakes and help me correct them, which is a bit of a "phew, dodged a bullet" (worst case is you get your erroneous proof published and look like an idiot for eternity). Btw, I picked up that idea that the purpose of proofs is to convince others (other mathematicians) from some article or paper I read about proofs in mathematics, but I have no idea which one it was now. Anyway it's not my own idea, I just found it somewhere and it made a lot of sense, and still does. Then there's the proofs you can construct with an automated theorem prover. I wonder if that's more the kind of proof that Penrose is talking about? In a sense, I don't think any human can really really construct an entire proof. All the proofs I've seen (and all the ones I've written) are more correctly proof sketches. That's why I think their point is only to convince others that what you say is true, and not to uncover some fundamental truth about the nature of the universe. Humans don't do that. I don't think we can do that. Formal systems like arithmetic or logic try to capture what is our ideal reasoning procedure, but not what we do in practice. I think so anyway. >> This depends on S being consistent. Lucas and Penrose apparently suppose that any proposal for explaining thinking as a computational process would, ipso facto, cast a mind as a concrete instantiation of a consistent formal system. I haven't read Lucas' and Penrose's work but I would find it very hard to be convinced about the truth of that. I don't understand how humans reason. I can see what I do, and what others do, but after a certain point all models seem to break down and minds seem capable of just jumping to conclusions because they like them. It's such a huge question how our minds work, exactly. I will probably never know.

mannykannot 4y ago

I'm just being lazy and quoting a claim from Wikipedia's entry on the Penrose-Lucas argument, allegedly referencing "The Emperor's New Mind", but without any specific location within that book. It has been a while since I read it, and I may attempt to find a more precise summary of Penrose's claim (he has written about it extensively elsewhere, and so have many other people) but I can't do that immediately.

benlivengood 4y ago
I think that Penrose basically thinks it's useful that humans can heuristically step up from a logic system S to S+"statement X is true" in an almost-grounded way, but in reality we are all actually constrained by Godel, Tarski, etc. We just trick ourselves into assuming we can inductively keep stepping up from S+"X is true" indefinitely for any practical problem we encounter, but that is actually an ungrounded assumption. What seems like an even better formal solution is something like logical induction[0] that works over something like probabilities instead of truth/falsehood. It has an existence proof but not a constructive formalization, afaik, but maybe some recent progress has been made. 0: https://arxiv.org/abs/1609.03543 https://arxiv.org/abs/1609.03543
- YeGoblynQueenne 4y ago
  Thanks for the paper, I need to read that. Much of my work is on inductive logic. >> I think that Penrose basically thinks it's useful that humans can heuristically step up from a logic system S to S+"statement X is true" in an almost-grounded way, but in reality we are all actually constrained by Godel, Tarski, etc. We just trick ourselves into assuming we can inductively keep stepping up from S+"X is true" indefinitely for any practical problem we encounter, but that is actually an ungrounded assumption. What you describe sounds to me more like logical abduction, rather than induction. Unfortunately, it's difficult to find simple explanations of what abduction is. One very rough and operational categorisation of modes of inference, as deductive, inductive or abductive, is as follows. Deduction is reasoning (as in automated theorem proving or rule-based systems), induction is learning (as in machine learning) and abduction is reasoning under uncertainty (as in probabilistic inference). There's a lot of confusion between what is abduction and what is induction, and the definitions of those in terms of "facts" and "rules" (coming from Peirce, who originally named "abduction" at least) is, for me, not very helpful. Another colloquial explanation is that abduction is a form of drawing conclusions from observations that isn't sound, so that conclusions are not necessarily true. I think that's where the association with probabilistic reasoning comes from, and that's why I think it describes better the kind of induction the linked paper is talking about. Anyway I'll have to read that, thanks.
YeGoblynQueenne 4y ago
Thanks for clarifying! Sorry for pouncing on that one little detail in your comment btw. Incompleteness vs. human reasoning is just something I think about on and off and your turn of phrase caught my attention.

mannykannot 4y ago

Update: One of the things I overlooked when using that quote is that it appears to say that we can prove the truth of any undecidable sentence, but Penrose's argument is made only with respect to the formalization, in a consistent and sufficiently strong [1] system S, of the sentence "the truth of this sentence is not provable in S". Both Lucas and Penrose claim that we will see that it is true (but, as it asserts, not provable in S) as the alternative leads to contradiction. This depends on S being consistent. Lucas and Penrose apparently suppose that any proposal for explaining thinking as a computational process would, ipso facto, cast a mind as a concrete instantiation of a consistent formal system. [2] Putting aside any thoughts of whether this is persuasive, I think this seems to be a case of Lucas and Penrose doing what they claim is uniquely human: thinking outside of the box of formal proof. More generally, almost none of human knowledge is couched as a formal proof of something or other, and almost none of it has been acquired that way. [1] More precisely, one in which a “moderate amount of number theory” can be proven. [2] J.R.Lucas, "Minds, Machines and Gödel", 1961.

YeGoblynQueenne 4y ago
>> Putting aside any thoughts of whether this is persuasive, I think this seems to be a case of Lucas and Penrose doing what they claim is uniquely human: thinking outside of the box of formal proof. More generally, almost none of human knowledge is couched as a formal proof of something or other, and almost none of it has been acquired that way. Well, except for all of mathematics :P Then again, it's useful to wonder what, exactly, is a formal proof, when derived by a human. My understanding of proofs (after having had to come up with several for my PhD research) is that the purpose of a proof is to convince a human that what the associated theorem states, is true. The human is first of all the person stating the theorem, so for example these days at least when I write down a theorem, the next thing I do is ask myself out loud "why do I think this is true?". Then I try to write it down in simple English, and then I try to put it in the standard format of an inductive proof, or a proof by refutation- and I do that only because those are proof structures that are well understood and they will cause the least confusion about what I mean. Even so I've got proofs wrong and I had reviewers pick out my mistakes and help me correct them, which is a bit of a "phew, dodged a bullet" (worst case is you get your erroneous proof published and look like an idiot for eternity). Btw, I picked up that idea that the purpose of proofs is to convince others (other mathematicians) from some article or paper I read about proofs in mathematics, but I have no idea which one it was now. Anyway it's not my own idea, I just found it somewhere and it made a lot of sense, and still does. Then there's the proofs you can construct with an automated theorem prover. I wonder if that's more the kind of proof that Penrose is talking about? In a sense, I don't think any human can really really construct an entire proof. All the proofs I've seen (and all the ones I've written) are more correctly proof sketches. That's why I think their point is only to convince others that what you say is true, and not to uncover some fundamental truth about the nature of the universe. Humans don't do that. I don't think we can do that. Formal systems like arithmetic or logic try to capture what is our ideal reasoning procedure, but not what we do in practice. I think so anyway. >> This depends on S being consistent. Lucas and Penrose apparently suppose that any proposal for explaining thinking as a computational process would, ipso facto, cast a mind as a concrete instantiation of a consistent formal system. I haven't read Lucas' and Penrose's work but I would find it very hard to be convinced about the truth of that. I don't understand how humans reason. I can see what I do, and what others do, but after a certain point all models seem to break down and minds seem capable of just jumping to conclusions because they like them. It's such a huge question how our minds work, exactly. I will probably never know.