What are Henkin models

Question

What is exactly called a Henkin model? Is this notion tied to 2nd order logic? How it differs from other non-Henkin's models?

Answer 1

There are two things one could plausibly mean by the phrase "Henkin model." The first is the sort of structure that emerges during the usual proof of Godel's Completeness Theorem (no, that's not a typo): a structure whose terms in a language mod provable equality in some theory. This is also called a "term model."

---

I suspect, however, that you're looking for the other meaning, based on your comment about second-order logic. The issue here is that there are two different ways we can approach second-order logic semantically:

• We can think of a second-order structure as a first-order structure $\mathfrak{M}=(M; \mathcal{I})$ - with underlying set $M$, and "interpretation" $\mathcal{I}$ - together with a family $\mathbb{S}$ of subsets of/relations on/functions on the domain $M$ which our second-order quantifiers range over; and we demand that $\mathbb{S}$ be closed under "basic operations" so that things aren't silly (I'll leave this vague for now). This idea gives us two degrees of freedom in constructing a second-order structure: the choice of first-order part, and the separate (constrained, but not totally determined) choice of second-order part. This is the Henkin semantics, and a structure of the type above is a Henkin model.

• Alternately, we can demand that second-order quantifiers really range over all the subsets of/relations on/functions on the domain $M$, so that the second-order part of a structure is completely determined by the first-order part (hence, even though our structures are more complicated, we still only have one degree of freedom in describing them). This is the standard semantics, and is the more commonly used semantics to my understanding (outside of computer science).

These two notions of semantics behave fundamentally differently. Henkin semantics is essentially first-order logic all over again, whereas the standard semantics is fundamentally different (and it's the standard semantics that people are referring to when they say e.g. "second-order logic is not compact" or similar). The standard semantics runs into serious set-theoretic difficulties right out the gate, which are detailed at many locations on this site and mathoverflow (see e.g. here, here, or here); on the other hand, we can also interpret this as saying that the standard semantics captures something fundamentally new, whereas the Henkin semantics is just clever language.