However, there is more to it for us than a philosophical controversy
in the foundations of mathematics. If QED is to succeed, then informal
mathematical arguments have to be translatable into QED. My opinion
is that many of these arguments when formalized in logic will actually
concern the relation of formulas to models, i.e. wil involve truth as
a concept.
I think philosophers know this but can call this informal use of the word
truth just a manner of speaking, translatable (in principle) back into
arguments about formulas. However, if one decides in advance to work
only in terms of formulas, one will be working with one hand behind one's
back. The translations will be much longer than the original arguments
that we might have allowed but don't for reasons of philosophical purity.