I'm quite fond of Wadler's paper The Girard-Reynolds Isomorphism which shows that there is a translation from system $\mathrm{F}$ to and from Second Order Predicate Logic (a version with higher-order types). One direction is "dependency erasure", an important idea in dependent types, and the other is the "parametricity theorem" or theorem-for-free of a type.
Wadler shows that in some conditions, these transformations are inverses of each other.
So to answer your question: the theorems-for-free can be expressed in a form of second-order logic, which is described in the aforementioned paper.