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 formulaAand 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.ewhich is logically unquestionable.Given an absolute proof, the freedom fromCONTRADICTION of classical mathematics is ensured.

Now,if given a general expression,a numeraln, 1+n=n+1 is problematic as Hilbert puts it, it “is from the finitist point of view "(Source:Hilbert's Program (Stanford Encyclopedia of Philosophy))incapable of being negated”

Waiting for your answer.If Hilbert is looking for a contradictory free program, then why he is looking a general expression as problematic?