> But isn't something defined as true in a system iff it can be proven in said system? No. You can build a really trivial system and know things about it "from

> But isn't something defined as true in a system iff it can be proven in said system? No. You can build a really trivial system and know things about it "from the outside", so to speak, even if they can't be proved within the system itself. Godel's work is exactly about showing the difference between something being actually true, and something being provable within a system. Let's take a not-real example: we know there are infinitely many primes. If you define arithmetic formally, you can fairly easily prove that there are infinitely many primes. But, in theory, it could be something that isn't provable, but is still true; true because you can always actually generate more primes, but unprovable because there is no way to build a proof out of the axioms of arithmetic to show this. Now, this isn't true about the infinitude of primes, because it can be proved within arithmetic. But there are lots of other statements that we have't proved yet - and theoretically, any one of them could end up being unprovable. E.g. Goldbach's conjecture or the 3n+1 theorem - they might be actually true but something we can't prove within the way we've defined arithmetic.