I'm wondering whether the following demonstrates that a computer that can only generate "thoughts" which are sentences derivable from some underlying axioms (and therefore can only generate "true" thoughts) is unable to think.

## Advertising

This is based on the fact that a formal system can't understand sentences written down within that formal system (forgive me if I've worded this badly). For example, the expression "3+4" is both equal and not equal to "7" depending on your point of view. If a mathematician was wearing special glasses that mapped every expression into the object represented by that expression, she couldn't possibly make sense of what she was doing. Eg "3+4=7" wouldn't even appear as "7=7", but simply "true". An interesting theorem would be replaced by "true" which is not very interesting! When a mathematician thinks about the expression "3+4=7", there seems to be a duality of perspectives that must be juggled simultaneously. I think this duality is implicit to thinking. It seems to be associated with the relationship between a language and a meta-language. There are some good theorem proving programs around today. The output (and internal trace) of these programs always correspond to true sentences, making them infallible (but only in the sense of never making a mistake). However, every step is based on rules expressed in a meta-language where the underlying mathemetical truth seems to be isolated to the computer scientist who wrote the program. Consider that a computer has a rule "It is a good idea to simplify 3+4 to 7". If this rule is applied to itself the semantics of the rule is changed. Clearly 3+4 is not equal to 7, for the purposes of the meta-language used to represent both the computer's line of reasoning and the rules that it uses to advance its line of reasoning. This suggests that thoughts must be expressed in a meta-language that can't directly be modelled on productions from a set of "true" axioms. Does this demonstrate that any conscious being must be fallible? Consider that we allow an expression to have sub-expressions *quoted* within it? Eg We may write a rule like this It is a good idea to simplify "3+4" to "7" Somehow we would need to support free parameters within quoted expressions. Eg to specify the rule It is a good idea to simplify "x+0" to "x" It is not clear that language reflection can be supported in a completely general way. If it can, does this eliminate the need for a meta-language? How does this relate to the claim above? - David