6 ms·

> That’s a lovely fantasy, but Gödel shows that there are fundamental epistemic limits to the universe, things that no genius will help us to know, no alien rac

> That’s a lovely fantasy, but Gödel shows that there are fundamental epistemic limits to the universe, things that no genius will help us to know, no alien race could teach us, no machine could be built to solve, and no new kinds of mathematics will uncover. That's not quite true. As an example, take differential calculus. It is hard to see how that would have been an idea to arrive at automatically by an algorithm, but a few geniuses (Newton/Leibniz) got there anyway. Similarly, even when a theorem doesn't follow from the usual axioms (and neither does its negation), maybe another genius comes along with an axiom that is quite obvious, and allows us to prove the theorem (just like peano axioms are axioms we would just accept as being obvious). So it is not that we cannot know everything, it's just that there is no guarantee and no obvious way of doing so.

corysama 3y ago
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...
anthk 3y ago
The Greeks were very close to Calculus.
- kragen 3y ago
  i'm pretty sure lots of greek people know calculus, learning latin isn't that hard, and there are actual calculus textbooks in greek now anyway if, on the other hand, you mean classical athens (platon and sokrates and all those dudes) then, no, they weren't, archimedes wasn't even born until like 180 years later

corysama 3y ago

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...

anthk 3y ago

The Greeks were very close to Calculus.

kragen 3y ago
i'm pretty sure lots of greek people know calculus, learning latin isn't that hard, and there are actual calculus textbooks in greek now anyway if, on the other hand, you mean classical athens (platon and sokrates and all those dudes) then, no, they weren't, archimedes wasn't even born until like 180 years later