Thanks Dan for raising this interesting objection.
“Defining ‘the mind of Dan Eastwood’ in a symbolic system” isn’t any more possible than “defining ‘the mind of God’ in a symbolic system.
How do you prove the existence of Dan Eastwood’s mind? On the basis of the existence of speech or written text we identify as contents of such a mind, like for instance the comments you have posted in this thread.
The existence of a ‘yes’ or ‘no’ answer to the question of whether there is or not a largest perfect number implies the existence of a mind that contains such an answer. However, at present no human mind contains it. Therefore, there is a non-human mind containing this answer.
On the other hand, to solve a problem human mind has to discover the fitting algorithm (a finite set of symbolic operations). This way of working implies Turing’s and Gödel’s theorem: At any time T of history there will be unsolved problems in arithmetic’s whose solution exists and has to be contained in a mind. This omniscient non-human mind is what I define as God.
To this extent this reasoning does not invoke any content of religious faith or revelation, but only the principle that certain achievements require intelligent authors.
It’s one thing to say that the existence of any mind is “an un-provable proposition in ANY symbolic system”, it’s another thing to say that the existence of any mind is not provable at all.
In summary: If you deny the existence of a mind containing the answers to all unsolved solvable problems in arithmetic you can as well deny the existence of Dan Eastwood’s mind.