Hello,
Source Hilbert's Program (Stanford Encyclopedia of Philosophy)
It has been clearly mentioned : "The goal of Hilbert's program is then to give a contentual, metamathematical proof that there can be no derivation of a contradiction, i.e., no formal derivations of a formula A and of its negation ¬A."
We can clearly understand that the central idea of Hilbert's program was to provide the consistency of classical mathematics by finitary means i.e which is logically unquestionable. Given an absolute proof, the freedom from CONTRADICTION of classical mathematics is ensured.
Now,if given a general expression,a numeral n, 1+n = n+1 is problematic as Hilbert puts it, it “is from the finitist point of view "incapable of being negated” (Source:Hilbert's Program (Stanford Encyclopedia of Philosophy))
If Hilbert is looking for a contradictory free program, then why he is looking a general expression as problematic?
Waiting for your answer.