littlebabyjesus
one of Maxwell's demons
What Godel's theorem tells us is that there has to be at least one axiom that is true but cannot be proved to be true within the system. To prove its truth, you would need to add another axiom. So yes, maths is a system of axioms and tautologous statements derived from those axioms (pre-Godel, Wittgenstein's point in the Tractatus was to show that all logic is tautology), but you will never have a system in which all the axioms can be fully justified logically by the system alone.Surely that still means, though, it is a system of axioms and tautologous statements derived from those axioms. I don’t understand what your objection was to my characterisation of maths as being a series of tautologous statements derived logically from axioms. If you’re not saying arithmetic is axiom-free, are you saying it has statements that are neither axiomatic nor derived logically from those axioms?
And that's where Penrose comes in with his idea that there is something outside algorithmic thinking that provides understanding. We have access to this kind of reasoning - but a purely algorithmic calculating machine such as any extant computer does not.
I would perhaps link this to Kant's ideas about analytic and synthetic propositions. Kant contended that arithmetic was purely synthetic - there is no place for experience in arithmetic propositions. But I think Godel shows that this is wrong. There is a need for experience, for an analytic proposition somewhere down the line. An analytic statement gives meanings, and it is meanings that Penrose says are missing from purely algorithmic calculation. The idea of meaning itself involves an analytic statement, I would think. How do you actually define it? There is meaning to the sensation of 'yellow' for instance, to use Jonti's example, but we can't define it: rather, we experience it, we feel it. It cannot be defined synthetically at all.