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.
