S.O.S. Mathematics CyberBoard

Hello,

I do hope that someone here is familiar with Hilbert's proof theory!!!
I'm reading an article by W. Sieg which describes Hilbert's attempts to prove the consistency of arithmetics. When Sieg summarises proof theory, he states
- for Hilbert, a proof should only contain , numerals and sentential logical connectives.
- a proof theoretic argument starts with the transformation of a formal proof with a numeric endformula into something that consists only of numeric formulas.

I cannot imagine how this transformation might work for a proof that contains e.g. an expression of the form . Or some other statements that might be used but not expressed with .

Could someone explain this to me, please?