もう五十年以上前の話だけど、簡単な例を挙げるなら
Peano算術の無矛盾性と順序数ε0までの超限帰納法が
同値だというのは立派な数学的結果。
自然数に関するFermatの最終定理みたいな命題が
選択公理を用いて証明できるなら選択公理を用いないでも証明できる、
みたいなのも数理論理を勉強して初めて分かるようになる。

そもそも証明論はあくまで無矛盾性の強さを研究したりする分野であって
別の分野のために新しい道具を作って提供する分野じゃないから。