4 ms·

But, that's not what Gödel proved. Not that things are hard, or non-obvious. But, that there are actual limits we won't be able to get past regardless of how mu

But, that's not what Gödel proved. Not that things are hard, or non-obvious. But, that there are actual limits we won't be able to get past regardless of how much time and cleverness we apply to them. The limits might be very large. Might be unlimited for practical purposes. But, they are there waiting for us. I don't understand his theorems well enough to pretend to explain them to this audience. But, this is my understanding of them.

auggierose 3y ago
> But, that there are actual limits we won't be able to get past regardless of how much time and cleverness we apply to them. Nope, all he proved is that there is no automatic and purely formal way of arriving at truth. Doesn't mean that for any particular truth we cannot stumble upon a way to understand it anyway. For example, we cannot write a program (= automatic and purely formal way) to determine in general if an input program halts. But for a particular input program, we might be able to understand whether it halts anyway. There is just no a-priori guarantee that we will.
- trgn 3y ago
  I really don't think that this is the case. Godel proved that some truths cannot be proven. That seems pretty fundamental, and I think that's what made him so impactful, e.g. much more than e.g. the halting problem, which is about computation solely. What Godel also showed was that we can expand our a prioris, e.g. add another truth that "feels" intuitive to the axioms, and then we can understand some theorem or truth (ie. look under the hood, understand its mechanics). But that means expanding the system by some sort of oracle, some sort of "genius intuition". Fair enough, mathematicians will agree by consensus if it's the right think to do, but it's also infinitely regressive. So I'd agree with corysama here "we won't be able to get past regardless of how much time and cleverness we apply to them".
  - auggierose 3y ago
    > Godel proved that some truths cannot be proven. If by proof you mean using a fixed formal axiom system, then yes, you are right. But let's look at one particular such thing that cannot be proven formally within itself: The consistency of Peano arithmetic. But, I don't need a formal proof for that: It's obviously consistent, because the natural numbers form a model for Peano arithmetic. So I just gave you a proof, but it is not a formal one. Yet, I don't see how anyone of sound mind can reject this proof. So Peano arithmetic is obviously something we can assume when proving other, more complicated truths. And nobody can say, not even Gödel, that we will not keep finding similarly obvious truths for the more complicated truth we otherwise care about, but which might not be provable from the currently established axioms. Given that Gödel is a Platonist, he would probably agree with me on that.
    - hnfong 3y ago
      I'm not sure you're responding to the same point by the GP. GP claims some truths cannot be proven. You took one claim that could be proven ( https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof ) and tried to proclaim its truth without referring to the proof. Even the GP's claim is problematic. The Gödel's theorems don't prove that some truths cannot be proven. It only proves either ZF is inconsistent, or some truths in it cannot be proven. Ironically GP's implicit assumption that ZF is indeed consistent mirrors your response in which you claim Peanno is consistent... :D That said, if you somehow proved that "some truths cannot be proven within a fixed formal axiom system (that is sufficiently powerful)", and then you also take into account the Church-Turing thesis, i.e. that Turing machines can fully model our thoughts, then the proof of the claim about "some truths cannot be proven" is more or less complete. Of course you can always posit the existence of some "unknown unknowns" that are outside of our wildest imaginations and thus invalidating whatever we thought we have known. But that's outside of our current ability to reason. I could go on and talk about what I understand about divine inspiration and knowledge, but I suppose those topics are a bit too speculative for the crowd here...
      - trgn 3y ago
        > I could go on and talk about what I understand about divine inspiration and knowledge, but I suppose those topics are a bit too speculative for the crowd here... I'm listening :) !
- corysama 3y ago
  > to determine in general if an input program halts. But for a particular input program, I think we are in violent agreement. This is an example of what I meant by "unlimited for practical purposes, but still there."

auggierose 3y ago

> But, that there are actual limits we won't be able to get past regardless of how much time and cleverness we apply to them. Nope, all he proved is that there is no automatic and purely formal way of arriving at truth. Doesn't mean that for any particular truth we cannot stumble upon a way to understand it anyway. For example, we cannot write a program (= automatic and purely formal way) to determine in general if an input program halts. But for a particular input program, we might be able to understand whether it halts anyway. There is just no a-priori guarantee that we will.

trgn 3y ago
I really don't think that this is the case. Godel proved that some truths cannot be proven. That seems pretty fundamental, and I think that's what made him so impactful, e.g. much more than e.g. the halting problem, which is about computation solely. What Godel also showed was that we can expand our a prioris, e.g. add another truth that "feels" intuitive to the axioms, and then we can understand some theorem or truth (ie. look under the hood, understand its mechanics). But that means expanding the system by some sort of oracle, some sort of "genius intuition". Fair enough, mathematicians will agree by consensus if it's the right think to do, but it's also infinitely regressive. So I'd agree with corysama here "we won't be able to get past regardless of how much time and cleverness we apply to them".
- auggierose 3y ago
  > Godel proved that some truths cannot be proven. If by proof you mean using a fixed formal axiom system, then yes, you are right. But let's look at one particular such thing that cannot be proven formally within itself: The consistency of Peano arithmetic. But, I don't need a formal proof for that: It's obviously consistent, because the natural numbers form a model for Peano arithmetic. So I just gave you a proof, but it is not a formal one. Yet, I don't see how anyone of sound mind can reject this proof. So Peano arithmetic is obviously something we can assume when proving other, more complicated truths. And nobody can say, not even Gödel, that we will not keep finding similarly obvious truths for the more complicated truth we otherwise care about, but which might not be provable from the currently established axioms. Given that Gödel is a Platonist, he would probably agree with me on that.
  - hnfong 3y ago
    I'm not sure you're responding to the same point by the GP. GP claims some truths cannot be proven. You took one claim that could be proven ( https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof ) and tried to proclaim its truth without referring to the proof. Even the GP's claim is problematic. The Gödel's theorems don't prove that some truths cannot be proven. It only proves either ZF is inconsistent, or some truths in it cannot be proven. Ironically GP's implicit assumption that ZF is indeed consistent mirrors your response in which you claim Peanno is consistent... :D That said, if you somehow proved that "some truths cannot be proven within a fixed formal axiom system (that is sufficiently powerful)", and then you also take into account the Church-Turing thesis, i.e. that Turing machines can fully model our thoughts, then the proof of the claim about "some truths cannot be proven" is more or less complete. Of course you can always posit the existence of some "unknown unknowns" that are outside of our wildest imaginations and thus invalidating whatever we thought we have known. But that's outside of our current ability to reason. I could go on and talk about what I understand about divine inspiration and knowledge, but I suppose those topics are a bit too speculative for the crowd here...
    - trgn 3y ago
      > I could go on and talk about what I understand about divine inspiration and knowledge, but I suppose those topics are a bit too speculative for the crowd here... I'm listening :) !
corysama 3y ago
> to determine in general if an input program halts. But for a particular input program, I think we are in violent agreement. This is an example of what I meant by "unlimited for practical purposes, but still there."