<p>Denotational semantics interpret the theories of various lambda calculi in various (set-theoretic, domain-theoretic, category-theoretic, game...) models. Let <span class="math-container">$T$</span> be the theory of one such lambda calculus <span class="math-container">$\lambda_?$</span>. If I understand correctly, a denotational semantics for <span class="math-container">$\lambda_?$</span> is thus just a model for <span class="math-container">$T$</span>.</p>

<p>The question here is, have applying the tools and methods of model theory to denotational semantics yielded useful results. For example, what does the Löwenheim–Skolem theorem tell us about the denotational semantics of various lambda calculi?</p>

CC BY-SA 4.0
2018-11-25T22:29:23.443Z
@NoahSchweber I also doubt if the Lowenheim-Skolem theorem is useful here. But as you said, if there are countable models, there should be uncountable models as well, so maybe it's interesting to look at what those models are?
xrq
CC BY-SA 4.0
2018-11-26T10:21:09.830Z
@NoahSchweber, in denotational semantics term models is what you want to get away from.
Martin Berger
CC BY-SA 4.0
2018-11-26T10:26:40.763Z
I doubt that traditional model theory can directly be used in models lambda-calculus, because the latter is higher-order, while most model-theory is model theory of first-order logic. For example John Reynolds proved (in his [Polymorphism is not set-theoretic](https://hal.inria.fr/inria-00076261/document)) that there cannot be conventional models of the polymorphic lambda-calculus.
Martin Berger
CC BY-SA 4.0
2018-11-26T13:52:15.960Z
About  Löwenheim–Skolem  in particular, IIRC proving  Löwenheim–Skolem depends on some axiom of choice, so it doesn't really tell you anything interesting, all it says is: if a model $M$ exist, then a *crazy*  model $M'$ of any chosen cardinality exists. But you have no idea what $M'$ looks like, as Choice is not constructive. This says more about ZF's inability to nail down infinities, than about the fine-structure of higher-order computation.
Martin Berger
CC BY-SA 4.0
2018-11-26T14:01:56.337Z
I don't know if you'd consider this denotational semantics, but the way we relate program logics and other semantics is basically (simplifying a bit) *elementary equivalence* from model theory: let's assume you have some program logic (e.g. Hoare triples, or Hennessy–Milner logic). Then you define an equivalence of programs using EE by saying $P \cong Q$ if for all formulae $\phi$ of the logic  we have: $P \models \phi$ iff $Q \models \phi$. Now you want to show that if you have some other equivalence $\equiv$ on programs: $\cong$ and $\equiv$ coincide.
Martin Berger
<lo.logic><denotational-semantics>
Results in denotational semantics from model theory?
xrq
# Results in denotational semantics from model theory?

(Asked by: username_0 on 2018-11-22)

Denotational semantics interpret the theories of various lambda calculi in various (set-theoretic, domain-theoretic, category-theoretic, game...) models. Let $T$ be the theory of one such lambda calculus $\lambda\_?$. If I understand correctly, a denotational semantics for $\lambda\_?$ is thus just a model for $T$.

The question here is, have applying the tools and methods of model theory to denotational semantics yielded useful results. For example, what does the Löwenheim–Skolem theorem tell us about the denotational semantics of various lambda calculi?

**Tags:** lo.logic, denotational-semantics
> **Comments:**
> **username_0**: @NoahSchweber I also doubt if the Lowenheim-Skolem theorem is useful here. But as you said, if there are countable models, there should be uncountable models as well, so maybe it's interesting to look at what those models are?  
> **username_1**: @NoahSchweber, in denotational semantics term models is what you want to get away from.  
> **username_1**: I doubt that traditional model theory can directly be used in models lambda-calculus, because the latter is higher-order, while most model-theory is model theory of first-order logic. For example John Reynolds proved (in his [Polymorphism is not set-theoretic](https://hal.inria.fr/inria-00076261/document)) that there cannot be conventional models of the polymorphic lambda-calculus.  
> **username_1**: About  Löwenheim–Skolem  in particular, IIRC proving  Löwenheim–Skolem depends on some axiom of choice, so it doesn't really tell you anything interesting, all it says is: if a model $M$ exist, then a *crazy*  model $M'$ of any chosen cardinality exists. But you have no idea what $M'$ looks like, as Choice is not constructive. This says more about ZF's inability to nail down infinities, than about the fine-structure of higher-order computation.  
> **username_1**: I don't know if you'd consider this denotational semantics, but the way we relate program logics and other semantics is basically (simplifying a bit) *elementary equivalence* from model theory: let's assume you have some program logic (e.g. Hoare triples, or Hennessy–Milner logic). Then you define an equivalence of programs using EE by saying $P \cong Q$ if for all formulae $\phi$ of the logic  we have: $P \models \phi$ iff $Q \models \phi$. Now you want to show that if you have some other equivalence $\equiv$ on programs: $\cong$ and $\equiv$ coincide.  

---

## 0 answers

