>>13749107>dude we can never know the truth of mathematical statementsGödels result is not that we can't know the truth or provability of all propositions.
He just proves that there are statements, G, that can't be proven nor negated.
As for the discussion of you guys above:
To find the result interesting, it's enough to point out that the result says that there are well-formed propositions G such that neither G nor not(G) can be proven in the system.
Now we can put that in a higher context, but that's just sugar on top:
* Firstly, if we adopt Exclduded Middle in the metalogic, then "G or not(G)" is true, which means that at least one of them is true, which means that there's a proposition K (which is either G or is not(G)) that's unprovable and also true.
* Secondly, people say that the theory (e.g. first-order Peano Arithmetic (PA), in Gödels case) has a model - either in some stronger, material theory (say ZF) or by that we may mean "the Platonic true natural number". In either case, actually Gödels G is the proposition which turns out true in that model. In that sense, we can also say "true but unprovable", but imho that just complicated things.
Similar to the ZF case, we can also consider "True artihmetic", which is the set of true propositions in Peano arithmetic (PA), but to formalize that we also need to go beyond arithmetic
* Thirdly, there's modal logics and ordinal theories which prove PA consistent without in a sense being stronger than PA, and those suggest PA is consistent. (Also PA proves PA consistent w.r.t. finite approximations/number of quantifiers in the arithmetical hierarchy) As PA doesn't prove PA consistent, that's also a "true but (PA) unprovable" statement. But this angle also involves more than just the one theory
