<div dir="ltr"><div class="gmail_extra">Let me fix some notation for my answer, we'll say that our theory validates some proposition/judgment</div><div class="gmail_extra">P with |- P and that some model M validates a proposition with M |= P. Now, when we define a model there</div><div class="gmail_extra">are two properties which are mainly of interest.</div><div class="gmail_extra"><br></div><div class="gmail_extra"> - Soundness: the most basic property of a model is that if M |= P then |- P.<br></div><div class="gmail_extra"> - Completeness: if |- P then M |= P</div><div class="gmail_extra"><br></div><div class="gmail_extra">Do note that which direction is "soundness" and which direction is "completeness" varies wildly between different</div><div class="gmail_extra">sources. The idea with something like System F is that we'll establish a sound model and, knowing this, it's sufficient</div><div class="gmail_extra">to show that our model validates a given proposition in order to conclude that it holds in System F. In parametricity papers</div><div class="gmail_extra">for instance "P" would be something expressing "this program is contextually equivalent to that program". Now most models</div><div class="gmail_extra">in programming languages fail to complete, meaning that they might not capture every aspect of the theory in question. When</div><div class="gmail_extra">we're discussing mainly equality, this property is called "full abstraction" and is sort of the "holy grail" for a model. Don't let</div><div class="gmail_extra">this suggest that sound but incomplete models aren't useful, to the contrary they are often the only known way to establish certain</div><div class="gmail_extra">equivalence results when it comes to programming languages. Most logical relations (a form of PER model if you like) for general</div><div class="gmail_extra">references are incomplete if we disallow appeals to things like biorthogonality or closure under contextual equivalence.</div><div class="gmail_extra"><br></div><div class="gmail_extra">Your example with groups is sort of canonically the opposite, there you have a complete but unsound model. This direction is useful</div><div class="gmail_extra">for abstract algebra where the goal is to understand the model using the theory. In programming languages we usually have the </div><div class="gmail_extra">opposite problem, we don't understand the theory very well but we have a comparatively strong understanding of the model.</div><div class="gmail_extra"><br></div><div class="gmail_extra">As for why it's a useful trick to construct models in the first place, remember that directly showing the proof is often incredibly difficult.</div><div class="gmail_extra">While it may be in theory possible to circumvent a model it's often the only feasible way of proving something.</div><div class="gmail_extra"><br></div><div class="gmail_extra">Hopefully some of that makes some amount of sense.</div><div class="gmail_extra"><br></div><div class="gmail_extra">Danny</div></div>