2-logics quantify over predicates, 3-logics over predicates of predicates and so on.

Unlike 1-logic where we have nice meta-logical properties of soundness, completeness & effectiveness - these properties fail for higher logics.

But they're reobtained if instead of using full semantics we use Henkin semantics where the quantifiers are bounded. This means they reduce to typed 1-logic.

Consider the statement: Beethoven has all the properties that make for a great musician.

Surely, here one needs to restrict to properties that are applicable to human beings and not say to the moon for example?

Does this mean that typed 1-logic is more natural than just 1-logic? We have nice meta-logic properties, plus the expressibility of higher logics.

For example stating the least upper bound property for the reals is not possible in 1-logic, but it is in 2-logic.

Is there a strong argument for considering 1-logic more fundamental than typed 1-logic?

  • 1
    It's probably not fair to say second-order logic doesn't have "soundness." If you think logics without complete proof systems are still properly called "logics", then second-order logic certainly has a sound proof system. Jun 3, 2013 at 16:13
  • 1
    So 2-logic is incomplete but sound? Jun 3, 2013 at 17:12

3 Answers 3


Henkin semantics is equivalent to first-order logic + comprehension schema in expressive power. So if there's any reason to accept Henkin semantics over first-order logic, it will be insofar as one takes the comprehension schema to be logical truths.

There's a subtlety in the interpretation of these schema, viz. the quantified predicate variables are better thought of as sets as opposed to properties. So for instance, the sentence "Beethoven has all the properties that make for a great musician," if schematized in second-order logic, would say (roughly) "Beethoven is in every set that every great musician is in", or equivalently "Beethoven is in the set of great musicians," which doesn't quite have the intended meaning you suggested.

Perhaps this may make the comprehension schema look more plausible. But even if they're true, that doesn't yet mean they are logically true. Similarly, "Beethoven has all the properties that make for a great musician" doesn't yet give us reason to adopt Henkin semantics over, say, full semantics. For while it's natural to assume these properties are human properties (technically, the quantifiers range over the power set of the set of humans), that may not be something which is determined by our logic. If anything, our logic should be neutral to whether or not these properties being referred to are ones that only apply to humans (surely it's logically possible for the moon to sing, right?). But now, for comprehension schema, if they're true, are they true by virtue of logic? That will depend on your view regarding more fundamental philosophical issues.

  • I can't see how it is logically possible for the moon to sing, but I can see why it is poetically possible for it to do so. Jun 3, 2013 at 17:10
  • 1
    @MoziburUllah If it's not ruled out by the laws of logic, then it's logically possible. It's the broadest sense of possibility typically appealed to.
    – Dennis
    Jun 3, 2013 at 18:10
  • @Dennis: I see what you mean. But - doesn't that depend on what the laws of logic are appealed to? Suppose we add in modal operators of possibility. And situations such as the one above are seen as impossible? Jun 3, 2013 at 20:32
  • @MoziburUllah Yea that's all gonna get cashed out in the "what counts as logic?" debate which I take it you've been encountering.
    – Dennis
    Jun 3, 2013 at 20:50
  • @Dennis: And there I was thinking logic was just syllogisms :). Jun 3, 2013 at 21:02

I asked a similar question on Math-overflow, answered by Andrej Bauer: To quote:

"The undesirable properties of higher-order logic are created by an insufficient notion of model. That is, we cannot have all three, soundness, completeness and effectivness (decidability of proof checking), if we insist that formulas be interpreted in the "standard" set-theoretic way. Henkin semantics does not suffer from this defficiency.

What this says is not that something is wrong with higher-order logic, but that something is wrong with those who refuse to look at semantic models, even when they are right in front of their faces, because these models are "unintended", "philosophically unacceptable", "not what mathematicians think", etc. This phenomenon of refusing to accept new interpretations of old theories is quite persistent, and always very harmful. Didn't someone stall progress in noneuclidean geometry because it was unthinkable that there would be strange new models? Aren't imaginary numbers so called because they were unthinkable and did not "really exist"? Doesn't higher-order classical logic suffer because it is being denied its natural notion of models on the grounds that they are non-standard?"

The following observations are my own from the perspective of mathematical logic in a categorical, geometric & physical mood rather than philosophical logic.

Quine made a couple of observations about higher logics, first that they did not have good meta-logic properties - for example they weren't complete, sound or effective; and secondly they resembled set theory. To him these were good reasons to abandon considering them as logic per-se.

Its possible to turn this on its head and think that set theory is dual to logic. In the same way that in modern theories of geometry - algebra is dual to geometry (this followed from Descartes discovery of coordinatising geometry).

Now, a contemporary move to do this is from Category Theory. It has been observed that Sets have certain categorical properties which defines the category of sets uniquely. It turns out that a nicer theory prevails if we drop a few properties because it then connects up with logic and geometry much more neatly, broadly & deeply. (One could say this is an aesthetic application of Occams Razor). These kinds of categories are called Toposes and from the above perspective are thought of as generalised set theories.

Now, in the usual model theory one interprets logic in set theory. But in this new perspective we have many set theories to choose from. How does this change things?

We wish to get a duality between logics & set theories as alluded to above. This principle then tells us that the natural logic to consider is typed intuitionistic higher order logic and that they are dual to all toposes. This mean we also have a natural model theory context. A choice of this kind of logic tells you exactly which generalised set theory one should interpret it in.

What makes this natural, is that in the natural model context one immediately gets nice meta-logic properties; the ones that failed in the standard higher logic now hold - that is completeness, soundness and effectiveness.

Since, classical higher order logic is a specialisation of the typed intutionistic higher order logic we get nice meta-logic properties for it too. In a sense what is been done is setting Henkin semantics for higher-order logic in a natural context.

Finally, a further feature about toposes that makes them nice to work with is that they are also geometric: The starting point here is manifolds which are traditionally built via atlases - that is local pieces of a manifold (which are easy to define) are patched together. A different perspective is using sheafs, this uses the same idea of patching but also uses Descartes idea of algebra being dual to geometry. Instead of patching local bits of geometry we patch the local algebras defined by each local piece of geometry. That is Toposes are also sheaves.

This means that we can now give geometric interpretations of logic - for example the forcing construction in set theory has a nice geometric interpretation in toposes.

Forcing is important because Cohen showed that the continuum hypothesis was independent of ZFC in mainstream mathematical logic; that a geometric perspective on this is now possible is another piece of evidence that Toposes are a good way to add new perspectives not available in mainstream set theory. This of course is not to dispute the central importance of ZFC.

Further, from a geometric perspective toposes are pointless - this goes with Aristotles observation who argued against the atomists for the continuum to be made up of points, and argued for infinite divisibility. Further, a contemporary movement in mathematical treatments of physics is that the idea of particles as points is being abandoned - the barrier of the planck distance - strings of course are not points and are infinitely divisible - spin foams where the spacetime is discrete but with structure.

So, my answer to my own question is that from a certain philosophical perspective - more mathematical (& physical) than I proposed in my question - that full semantics isn't justified, and new semantics have been found given the hint by Henkin.

Note, I'm saying its an additional perspective and not a replacement.


Henkin semantics is important for higher order logic, but keep in mind that it is not automatically fully specified in every situation. Especially, are there any comprehension axioms at all, and if there are comprehension axioms, should they be predicative (i.e. avoid "inner" quantification over higher order variables) or impredicative (i.e. using arbitrary formulas including quantification over higher order variables as if they were first order variables).

Also note that the comprehension axioms can have a sort of "last word" property, i.e. if you introduce additional non-logical symbols into the language, all additional comprehension axioms enabled by these additional symbols become immediately available. Worse still, consider that the context of the logic can be extended to include Henkin quantifiers, cardinality quantifiers (or "nasty" transfinite quantifiers) or forms of infinitary logic (since we must assume an underlying set theory anyway). But all this additional expressivity of the language is automatically available for the comprehension axioms too. (I'm not so sure about impredicative comprehension axioms here, since they might quickly lead to paradoxes in case the language is extended beyong pure first-order logic.)

On the other hand, consider also the case where quantification over higher order variables is nearly absent, like in pure propositional logic where one just has a formula including propositions, and just want to know whether the formula is satisfiable (corresponding for existential quantification over all propositions), or whether the formula is a tautology (corresponding to universal quantification over all propositions). If we treat unquantified higher order variables in the same way, will standard semantics actually be different from Henkin semantics?

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .