Post #2728849

I have a question about models of second order theories. Suppose we have a theory with a single sort Tm and two operations, app : Tm -> Tm -> Tm and lam : (Tm -> Tm) -> Tm possibly also satisfying the equation app (lam u) v = u v. We would like to say that a model of this theory is a type 𝑀, equipped with functions app_M and lam_M of the appropriate type. With this setup, is it the case that we don't necessarily have an interpretation function [| _ |] : Tm -> M? By induction on Tm, we can obviously define [| app u v |] = app_M [| u |] [| v |]. However, when we try to define [| lam f |] = lam_M λx. [| f ? x |], we get stuck, since f expects something of type Tm, while we only have x of type M. Now, do there genuinely exist terms that we can construct in the free model but that we cannot translate into an arbitrary model, or is this only a problem with the setup? Stepping back, this second order theory is supposed to be a representation of the untyped lambda calculus. If this interpretation function doesn't exist, does that mean that not every model of this second order theory as I've defined it is a model of the untyped lambda calculus in the usual sense?