Why aren't valid higher order logic sentences recursively enumerable in full semantics?

Question

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?

Answer 1

The standard (aka "full") semantics for higher-order logic is analogous to a semantics for first-order set theory in which you require the power set operator in the object logic to be modelled by the power set operator in the metalogic, which you might also call the "full" semantics for first-order set theory. The usual semantics for set theory corresponds to the non-standard (Henkin) semantics for higher-order logic, in which you just require the power set operator to provide enough subsets to cover everything you can express syntactically.

It is customary to impose the "standard" straitjacket in higher-order logic by default, but not to impose the "full" straitjacket by default in first-order set theory. You can translate a higher-order sentence, $\phi$, to a morally equivalent first-order sentence, $\phi_S$ say, in the language of set theory. Under this translation, $\phi$ will be valid under the standard semantics for higher-order logic iff $\phi_S$ is valid under the full semantics for set theory and the set of such $\phi$ is certainly not r.e. (by Tarski's theorem on the undefinability of truth). On the other hand $\phi$ will be valid under the Henkin semantics iff $\phi_S$ is valid under the usual semantics for first-order logic and the set of these $\phi_S$ is r.e. (by completeness of first-order logic).

In a nutshell, higher-order logic and set theory are (at least morally) isomorphic, but only if you choose to impose the same restrictions on the semantics of the power set operator in both cases.

Answer 2

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.

Answer 3

The set of valid sentences using just equality in second order logic is a very complex set (The analogous set in first order logic is computable and c.e. if non logical symbols are allowed). Using Tarski's theorem on undefinability of truth, you can show that this set is not even analytical (lightface projective) - This is the analogue of the fact the true arithmetic is not arithmetical.

Answer 4

Why can't we simply translate a higher order logic sentence into first order set theory to test it for validity?

I want to focus on this (interesting!) confusion as to why the sentences of second-order arithmetic which are valid w.r.t full semantics need not be recursively enumerable even though everything takes place in a first-order ambient set theory whose provable sentences are recursively enumerable. I'm not an expert, so if anything's unprecise or wrong, or if I in effect repeated the other answers without noting, please tell me.

Given a sentence $\phi$ in second-order arithmetic, its semantic truth in $\textsf{ZFC}$ is expressible as a first-order statement in the language of set theory. Call this statement $\text{true}(\phi)$ and choose $\text{true}(-)$ in such a way that it is computable, and that moreover for any sentence $\psi$ in the language of set theory it is decidable as to whether it is of the form $\text{true}(\phi)$ for some $\phi$ or not, with $\phi$ computable from $\psi$ in case it is. This allows for choosing an arbitrary recursive enumeration of the provable sentences $\psi$ of $\textsf{ZFC}$ and 'printing out' out $\phi$ in case $\psi=\text{true}(\phi)$. All in all this gives - in the finitistic metatheory - a recursive enumeration of some set of sentences of second-order arithmetic that feels like the set of true sentences (sloppyness intended).

Huh?! Isn't this in contradiction with

$\textsf{[ZFC]}$ The set $\textbf{T}$ of true sentences of second-order arithmetic is not recursively enumerable.

To see that it is not, let's first make sure we are not comparing apples and oranges by having the seemingly contradictory statements live in the same formal system, i.e. let us internalize the above discussion in $\textsf{ZFC}$ itself. Then rereading it carefully, it shows that, within $\textsf{ZFC}$, we can enumerate the set $\textbf{S}$ of sentences $\phi$ of second-order arithmetic for which the (internalized) first-order theory $\textsf{ZFC}$ proves $\text{true}(\phi)$. Now, applying (within $\textsf{ZFC}$) Goedel's Completeness Theorem to the first-order theory $\textsf{ZFC}$ shows that these are precisely the sentences of second-order arithmetic which are valid for the natural numbers inside any model of $\textsf{ZFC}$ within $\textsf{ZFC}$.

This is a semantic notion of truth which is different from the natural one used for defining $\textbf{T}$!

For example, if we enhance the ambient theory $\textsf{ZFC}$ by $\neg\ \text{Con}(\textsf{ZFC})$, $\textbf{S}$ consists of all sentences of second-order arithmetic, while (if $\textsf{ZFC}$ and hence also $\textsf{ZFC} + \neg\ \text{Con}(\textsf{ZFC})$ is consistent) this is not true for the set $\textbf{T}$ of true sentences of second-order arithmetic.