 Theorem 2.2  highlights the fundamental role of definability of finite elements in the fully abstract model of PCF, an aspect that has been stressed in Curien 2007. As a smooth transition to the formalisms based on games, and partly following the historical development of the subject, we pause shortly to examine another aspect of definability that arises at the border between computation and the proof theory of constructive logical systems. It has been a remarkable discovery that the structure of natural deduction proofs for, say, the implicative fragment of intuitionistic propositional calculus is completely described by terms of the simply typed \(\lambda\)-calculus, where a provable propositional formula of the form \(\sigma \to \tau\) is read as the type of the terms representing its proofs. This is the propositions-as-types correspondence, to be attributed to Curry, de Bruijn, Scott, Läuchli, Lawvere and Howard, which extends to much richer formal systems (for a history of this correspondence see Cardone &amp; Hindley 2009: sec. 8.1.4).