[forgotpwtomain]

Thanks for this spark of a comment in an otherwise perturbed discussion. I cannot reply to all the child comments but hopefully I can help elucidate the misconception you are indicating.

> It's a rhetorical trick at best

This is precisely it. It works because 'true' is defined for the formal system but not for the human. It so happens that the humans in question say well 'of course we know what Godel's proposition means and what true is' but that's just because they are familiar with those words in an entirely unrelated sense to the system being described (akin to say the common speech use of 'energy').

Since you need a system at least as powerful to evaluate the propositions of an underlying system and in that more powerful system a similar proposition can be formed.

Anologous to this is Wittgenstein's problem on the irreducibility of rules: that one can always ask for the explanation of a rule, explanation of an explanation an so on ad infinitum. So it is essentially impossible to determine whether a rule is being applied correctly or not. It so happens that we (humans) can stop asking and 'apply'; but I'm not convinced this is something machines cannot do.

[fiatjaf]

Wittgenstein's "problem on the irreducibility of rules" is brainfart at best. Any rule that can be actually _followed_ cannot be logically precise, and vice-versa. If you try to reduce anything from the real-world to pure logic you'll surely end up crazy.

[posterboy]

there are abstract rules and practical laws, principles, whatchamacallit. Laws bind abstract rules to real thingies. The ground truth values are right and wrong en lieu of good and bad - basic emotions that are at the basis of experience. Trying to verbalize (the word logic is related to logos, old greek for tongue, language logic) every basic emotion you will surely go irrationaly crazy. Therefore, context is assumed and language is underspecific.