Free theorems, where?

I've found this webapp which lets you generate a free theorem for a given type.

The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which theory/logical system? How does this system relate to the equational theory of the language?

• This seems to be a repost of the same question on Stack Overflow, where it was considered off-topic, and garnered only a cursory answer linking to the "Theorems for Free" paper. Again, this link is relevant. – C. A. McCann Jan 8 '13 at 13:06
• Thanks for the reference. I've seen Wadler's paper, but I don't really understand it. He's working with frame semantics, then the relations seem to be between elements in these frames. How does the relations between these elements relate to the equational logic of the language (in Wadler's case, System F)? He instantiates relations with functions, do these functions need to be computable in System F? – user13264 Jan 8 '13 at 13:16
• the web app is down, are there mirrors anywhere? – user833970 Jun 21 '18 at 18:07

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.