It's said (proven in some reduction to the Gödel–Rosser theorem?) that second order logic and higher fails to be complete for full semantics; that is there isn't any semi-algorithm for determining if a sentence is valid in full semantics. Yet full semantics I understand is reducible to set theory, and set theory is expressible as a first order theory and so it's theorems are recursively enumerable.
Why can't we simply translate a higher order logic sentence into first order set theory to test it for validity? Does this not work? Or does this only work for sentences in set theory but not for some sentences in higher order logic that are 'true but unprovable' in full semantics?
Does this mean higher order logic and set theory aren't isomorphic?
Best Answer
Full semantics for higher-order logic is expressed at the meta-level: it says that we only consider models in which the higher-order variables range over all objects of the appropriate sort.
The error in the second paragraph of the post is that second-order logic with full semantics is not reducible to set-theory with first-order (Henkin) semantics in the way that paragraph claims. For example, every model of the second-order Peano axioms in full semantics satisfies the sentence Con(ZFC), but not every model of ZFC does. So the set of arithmetical logical consequences of the second-order Peano axioms in full semantics is a strictly larger set than the set of arithmetical consequences of the ZFC axioms.
There is no effective object theory whatsoever, in first-order (Henkin) semantics, that can achieve the restriction of full semantics. We have to make the restriction for full semantics at the metatheoretic level.
What is true is that, within each model of set theory, we have a "toy model" of full semantics: within a model $M$ of set theory, we can look at Henkin models for higher-order logic that appear to be full, from the viewpoint of $M$. We can use these "toy models" to understand how full semantics works. These "toy models" do help us understand just how strong second-order semantics are.
There is a vague analogy here with the fact that the intended model of ZFC consists of all sets, but no model in the usual first-order sense can contain all sets. So when we look at set models of ZFC, we get a sense of how the intended interpretation should work, but we don't actually see the intended interpretation. Similarly, if we try to formalize full semantics within a first-order set theory, we get a sense of how they work, but we can't capture their full strength.
The preceding paragraphs are written from what I view as the "classical" perspective on full semantics. Let me say, without taking a position, that there is another very tempting position for full semantics: that they are only defined relative to a given model of set theory. Thus, just as there are many models of set theory, there are many models of "full semantics". The benefit of this point of view is that it emphasizes more explicitly the assumptions about set existence that are presupposed by full semantics. But those who advocate the classical perspective might say that this other perspective misses the point, which is simply (from their POV) to require that the higher-order variables range over all objects of the appropriate sort.