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?
The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism. 

The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism.