Dissatisfaction with second-order logic

[Hurkyl]

Or, formal logic not a model theory?

(Sorry about the puns! Well, not really... )

For a while I've suspected what I consider to be a flaw in second-order logic (at least its interpretation), and it's recently been confirmed.

From Mathematical Logic by H.-D. Ebbinghaus, J. Flum, and W. Thomas, we have part of the definition of "satisfaction" for a second-order assignment $\gamma$ with $\mathcal{J} = (\mathcal{U}, \gamma)$:

For n-ary X:
$\mathcal{J} \models \exists X \varphi$   iff   there is a $C \subset A^n$ such that $\mathcal{J} \frac{C}{X} \models \varphi$


In other words, assuming I follow it correctly, the statement $\exists X: \varphi$ (where X is a variable denoting an n-ary relation on A) is satisfied by a second-order assignment if and only if we can map X to some subset of $A^n$ such that the result will be a model of $\varphi$.


This is a nice and dandy definition. I just think it's got the wrong idea.

The important problem, I think, is that the existential quantifer is interpreted as ranging over all set-theoretic relations. In essence, I get the feeling that it's slipping ZFC into the theory under consideration through the "back-door", and suspect that all of the not-nice things about second-order logic (such as failing the compactness theorem) arise from this.


But let's step aside and consider one of my favorite examples: the theory of real closed fields.

There are several equivalent characterizations of a real closed field. IMHO, the simplest is that R is a real closed field iff it is an ordered field, and R (= $R[x]/(x^2+1)$) is algebraically closed. Examples are the real algebraic numbers, the real numbers themselves, and IIRC, the set of real formal Puiseaux series. (Formal Laurent series in a k-th root of x. I think we consider x to be infinitessimal)

As we all know, the real numbers R form the only complete ordered field. But in some sense, all real closed fields are complete ordered fields. Consider the following theorem:

Theorem: Let R be a real closed field. Let $\phi$ and $\psi$ be unary relations on R in the (first-order) language of real closed fields such that neither is identically false, and $\phi(x) \wedge \psi(y) \implies x \leq y$. Then, $\exists y: \forall x: (\phi(x) \implies x \leq y) \wedge (\psi(x) \implies x \geq y)$.

If we let $\phi$ and $\psi$ range over all subsets of R, then this theorem would simply be stating that R is Dedekind complete, and would be false in general. But, by restricting ourselves only to the subsets of R that can be defined in the theory of real closed fields, we are able to prove Dedekind completeness!


By restricting ourselves to "internal" subsets like this -- that is, subsets that can be defined as relations in the language of the theory -- we can sometimes to useful things. For example, for any real closed field R, $R^n$ has a beautiful geometric structure... as long as you pretend that only semi-algebraic sets exist! (sets defined by equations and inequalities)


Now back to my criticism of second-order logic: in light of the above, it seems that the theorem I quoted above about the "Dedekind completeness" of any real closed field ought to be a theorem in the second-order theory of real closed fields, because it's a statement about all first-order relations.

But, due to the way second-order logic is done, the universal quantifier is allowed to run over all set-theoretic relations (i.e. all subsets), and not just the internal relations that can be defined in the first-order theory (i.e. semi-algebraic subsets)


So this prompts a question: is there a currently developed theory that remedies this "problem"? I imagine that would merely require that an interpretation of a second-order theory to explicitly specify the domain of any relation variables, rather than assuming the domain to be the collection of all set-theoretic relations. I would like to not have to rediscover it, if it exists already.

 

[zmike]

To answer your question, formal logic is not a model theory in the sense that it allows the universal quantifier to range over all set-theoretic relations, and not just the ones internally defined in the theory.

 

[tacman]

Thank you for sharing your thoughts on dissatisfaction with second-order logic. I can understand your concerns about the interpretation of the existential quantifier and its potential for introducing set-theoretic concepts into the theory. It does seem like this can lead to some inconsistencies and difficulties in certain applications, such as with the example of real closed fields.

I am not familiar with any currently developed theory that specifically addresses this issue, but it does seem like a valid concern to consider when working with second-order logic. Perhaps further exploration and development of the theory could help to clarify and resolve some of these issues. In the meantime, it is important to be aware of the potential limitations and pitfalls of using second-order logic in certain contexts.