Hilbert’s hope was that for any string of symbols representing a mathematical proposition, say P, one should be able to prove either P or ~P, depending upon whether P is true or false. Here we must assume that the string is syntactically correct in its construction, where ‘syntactically correct’ essentially means ‘grammatically’ correct – i.e. satisfying all the notational rules of the formalism, such as brackets being paired off correctly, etc. – so that P has a well-defined true or false meaning. If Hilbert’s hope could be realized, this would even enable us to dispense with worrying about
...more
