Lucas and Penrose have argued that Godel's (1st incompleteness) theorem refutes mechanism.
All it shows that for any recursively axiomatizable formal system with Peano arithmetic, we can construct a sentence that is neither provable nor disprovable, but is nonetheless true. Call that sentence G (for Godel). But this is only under the assumption that such a formal system is consistent. If it is not consistent, then every formula is a theorem of the system, and so too is G. The problem is that we cannot prove in the system that such a system is consistent - proved by Godel's 2nd incompleteness theorem. So all we have is that
CONs-->G
which means, if S (some formal arithmetical system) is consistent, then G is true. But we cannot prove CONs, so we cannot infer G. So how do we know that G is true? Because our minds which are not recursively axiomatizable (like formal systems and machines) can see that's true by some other unaxiomatizable means. So while S cannot prove G and so G is not in S (and is thus not a theorem of S, and so isn't true in S), we know it's true. Therefore, Godel's theorem doesn't show that there are things that humans cannot think of, it shows that there are formulas that machines (or formal systems) are incapable of knowing, or proving.
There is a big difference between any formal arithmetical system and "true" arithmetic, for which all arithmetical formulas, including G, are true. "True" arithmetic is complete (but not recursively axiomatizable), while any given formal arithmetical system isn't (proved by G).
All it shows that for any recursively axiomatizable formal system with Peano arithmetic, we can construct a sentence that is neither provable nor disprovable, but is nonetheless true. Call that sentence G (for Godel). But this is only under the assumption that such a formal system is consistent. If it is not consistent, then every formula is a theorem of the system, and so too is G. The problem is that we cannot prove in the system that such a system is consistent - proved by Godel's 2nd incompleteness theorem. So all we have is that
CONs-->G
which means, if S (some formal arithmetical system) is consistent, then G is true. But we cannot prove CONs, so we cannot infer G. So how do we know that G is true? Because our minds which are not recursively axiomatizable (like formal systems and machines) can see that's true by some other unaxiomatizable means. So while S cannot prove G and so G is not in S (and is thus not a theorem of S, and so isn't true in S), we know it's true. Therefore, Godel's theorem doesn't show that there are things that humans cannot think of, it shows that there are formulas that machines (or formal systems) are incapable of knowing, or proving.
There is a big difference between any formal arithmetical system and "true" arithmetic, for which all arithmetical formulas, including G, are true. "True" arithmetic is complete (but not recursively axiomatizable), while any given formal arithmetical system isn't (proved by G).
