This is something that has left me puzzled for years. My understanding is that a model is a concrete realization of an abstract structure in terms of some other mathematical structure, such that all the laws from the first are satisfied in the latter. A simple example might be the abstract (algebraic) structure "group" and a concrete realization e.g. the integers with addition. Finding models for abstract theories is certainly useful, for instance it shows that the theory is actually 'inhabited'; it may also shed light on the theory and give us ideas about new theorems that might generalize to the abstract setting. However, nobody would claim that from a theorem about integers I can deduce one for abstract groups in general. But exactly this kind of reasoning appears to be valid when proving things about e.g. the polymorphic lambda calculus (aka System F). For instance, in the famous "free theorems" paper by Wadler, the free theorems appear as a consequence of modeling types in system F as relations (this is most probably oversimplified, i can't remember the details but I think they are not important here). The question is: How can that imply anything about system F itself? Wouldn't it be necessary to prove that these free theorems hold for /all/ models of System F, not just one particular? Besides, if such proofs using a suitable model are really valid, why does it seem to be impossible to 'translate the proof back' from the model to the original system and thus arrive at a direct proof? I am sure there is something wrong with my understanding of these things but I can't figure out what. Cheers Ben