- 14,922
- 28
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 [itex]\gamma[/itex] with [itex]\mathcal{J} = (\mathcal{U}, \gamma)[/itex]:
For n-ary X:
[itex]\mathcal{J} \models \exists X \varphi[/itex] iff there is a [itex]C \subset A^n[/itex] such that [itex]\mathcal{J} \frac{C}{X} \models \varphi[/itex]
In other words, assuming I follow it correctly, the statement [itex]\exists X: \varphi[/itex] (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 [itex]A^n[/itex] such that the result will be a model of [itex]\varphi[/itex].
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 (= [itex]R[x]/(x^2+1)[/itex]) 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 [itex]\phi[/itex] and [itex]\psi[/itex] be unary relations on R in the (first-order) language of real closed fields such that neither is identically false, and [itex]\phi(x) \wedge \psi(y) \implies x \leq y[/itex]. Then, [itex]\exists y: \forall x: (\phi(x) \implies x \leq y) \wedge (\psi(x) \implies x \geq y)[/itex].
If we let [itex]\phi[/itex] and [itex]\psi[/itex] 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, [itex]R^n[/itex] 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.
(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 [itex]\gamma[/itex] with [itex]\mathcal{J} = (\mathcal{U}, \gamma)[/itex]:
For n-ary X:
[itex]\mathcal{J} \models \exists X \varphi[/itex] iff there is a [itex]C \subset A^n[/itex] such that [itex]\mathcal{J} \frac{C}{X} \models \varphi[/itex]
In other words, assuming I follow it correctly, the statement [itex]\exists X: \varphi[/itex] (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 [itex]A^n[/itex] such that the result will be a model of [itex]\varphi[/itex].
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 (= [itex]R[x]/(x^2+1)[/itex]) 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 [itex]\phi[/itex] and [itex]\psi[/itex] be unary relations on R in the (first-order) language of real closed fields such that neither is identically false, and [itex]\phi(x) \wedge \psi(y) \implies x \leq y[/itex]. Then, [itex]\exists y: \forall x: (\phi(x) \implies x \leq y) \wedge (\psi(x) \implies x \geq y)[/itex].
If we let [itex]\phi[/itex] and [itex]\psi[/itex] 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, [itex]R^n[/itex] 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.