JoannaGolińska
THE SPECTRUM PROBLEM FOR THE LANGUAGE WITH HENKIN QUANTIFIERS[1]
Probably under the influence of The Completeness Theorem for first order logic [Gödel 1930] and Gödel’s work [Gödel 1931] proving essential incompleteness of logics for richer languages, logicians focused on semantics for first order logic. This attitude got intensified due to Trachtenbrot’s discovery [Trachtenbrot 1950] that the logic restricted to finite models cannot be axiomatizable except in the case of very pure vocabularies. As a result, until the questions and problems concerning researches on the foundations of computer science arose, most of the mathematicians did not pay too much attention to semantics restricted to finite models. The most extreme example of this is the monograph [Chang – Keisler 1990] reassuming some important stage of the model – theoretic researches. However, apart from the main direction of researches, problems concerning logics restricted to finite models and attempts to solve them arose. The most important of them are the problems of Scholz and Asser. Now we know that these problems are equivalent to crucial problems in foundations of computer science.
In particular, the most important open mathematical problem „does P=NP?” is equivalent to some questions concerning finite model theory. Assuming that the way of a human brain’s work is based on the same rules as the way the machines made by a man work, this problem is also equivalent to a question about the real human cognitive abilities.
Classes of finite models recognizable in real time, that is the ones belonging to the class P, according to our programming experience determine the highest level of practical computation. On the other hand, many practically difficult from the algorithmic point of view problems belong to NP class. The importance of NP lies in the fact that many problems for which efficient algorithms would be highly desirable, but are yet unknown, belong to NP. The travelling salesman problem and the integer-programming problem are two such problems among many others. Therefore the question concerning classification of concepts in finite models can be treated as the crucial problems related to human cognitive abilities in the technological sense and presumable in the absolute sense.
The proof of Trachtenbrot’s theorem stating that there is no algorithm, which would decide for any formula whether it is satisfied in finite models, was presented on a symposium organized by Institut für Mathematische Logik und Grundlagenforschung University in Münster. Heinrich Scholz put there the question about sets of cardinalities of all finite models of first order formulae (called the spectrum). The official formulation of the problem asks about characterization of spectra for first order formulae (including „=” but without function symbols) has been given in [Scholz 1952]. G. Asser in [Asser 1955] has stated the weaker version of this problem „does complement of every spectrum is also a spectrum?”. Later, Scholz problem has been considered for various logics. Thus, the spectrum problem applies to finitely axiomatizable classes of finite models (spectra of these classes are called generalized first order spectra) and to any n – order logics.
The most important and most interesting theorem related to the spectrum problem is Fagin’s theorem. In [Fagin 1974] Fagin considered generalized spectra of existential second order formulae. He proved that any class of finite models closed on isomorphism is a generalized spectrum if and only if it is recognizable by nondeterministic Turing’s machine in polynomial time, i.e., it is in NP. Of course we should restrict our attention to classes of models closed on isomorphism. Blass and Gurevitch [Blass–Gurevitch 1986] showed that the same holds for positive formulae with Henkin quantifiers. These above theorems allows to prove that Asser problem is equivalent to well–known open problem of theory of computational complexity „does NP=co–NP?”. Hence Scholz and Asser problems are still open.
Therefore it seems natural to consider the spectrum problem for simpler case, e.g. logics in empty vocabulary. It is known that in this case generalized spectra and spectra in the sense of Scholz are equivalent. This so because in the case of empty vocabulary, models are uniquely up to isomorphism determined by their cardinalities.
In this paper the spectrum problem for the logic with branched quantifiers in empty vocabulary is considered. Particular attention is devoted to spectra of some syntactically defined sublogics of the logic with all branched quantifiers. The characterization of spectra of these logics would additionally solve the problem whether there is any essentially infinite class of branched quantifiers not equivalent to all Henkin quantifiers. One of the simplest examined essentially infinite classes is the class of quantifiers of the form:
x1y1
......
......
xnyn
The problem whether these quantifiers are equivalent to all Henkin quantifiers is still open. Therefore particular attention is devoted to the logic with these quantifiers.All considered results can be also treated as results about expressive power of certain languages in finite models
This paper does not contain final solutions to the title problem. Even though some of general theorems giving partial characterization of spectra of considered sublogics of the logic with all Henkin quantifiers are formulated, the examples of spectra of mentioned sublogics are presented in the first place.
The paper consists of four sections. In the first section – Henkin Quantifiers – the basic ideas and concepts related to the logic with branched quantifiers are presented. The second section – The spectrum problem. Generalformulation – contains the various versions of formulation of the spectrum problem with special attention concentrated on the logic with branched quantifiers in the empty vocabulary. In the third section – The spectrum problem for languages with Henkin quantifiers – the solution of the spectrum problem for the logic with function quantifiers is presented. This logic is one of the few sublogics of the logic with all Henkin quantifiers L* about which it is known that it is semantically weaker than L*. This solution can be treated as paradigmatic solution to considered version of the spectrum problem presented in the paper. In the last, fourth section – Examples of spectra of formulae withbranched quantifiers – examples of sets of natural numbers being the spectra of formulae with specified branched quantifiers and the partial characterization of spectra for some special class of formulae with branched quantifiers are presented. The paper ends with the summary of received results.
The way of defining of classical logical concepts and formulation of the basic theorems is based on the works [Chang–Keisler 1990], [Adamowicz–Zbierski 1991] and [Krynicki–Mostowski 1995]. This work is based on a portion of the author’s master thesis in Faculty of Philosophy and Sociology of Warsaw University. In the paper only main theorems directly concerning the considered problem are being proved. The proofs of theorems presented earlier in the literature within the limits of logical research on branched quantifiers are substituted with references to literature.
HENKIN QUANTIFIERS
In this section we present basic ideas and concepts related to Henkin quantifiers. Our presentation is based on the survey paper [Krynicki–Mostowski 1995]. Because we are interested mainly in the logic with Henkin quantifiers restricted to finite models, so we skip such semantics as relational or weak. In finite models these two semantics are equivalent to the one given by Henkin in [Henkin 1961].
1.1 Definition (Henkin prefixes as dependency relations)
A Henkin prefix (a branched prefix) is a triple Q = (AQ, EQ, DQ), where AQand EQare disjoint finite sets of variables called respectively universal and existential variables of Q, and DQ is a relation between universal and existential variables of Q (DQAQEQ), called the dependency relation of Q. If (x, y) DQ then we say that the existential variable y depends on the universal variable x in Q.
Logicians use the term quantifier quite ambiguously (see e.g., discussion in [Krynicki–Mostowski 1995a]). Particularly in the case of Henkin quantifiers several concepts are equally well applied to quantifier prefixes and to quantifiers. A quantifier prefix is a quantifier with fixed bound variables. Having any class of quantifier prefixes we define an equivalence relation for prefixes by an isomorphism determined by any permutation of all relevant variables. Then we define a quantifier as an equivalence class of this equivalence relation. Traditionally we define basic concepts parallel for prefixes and quantifiers, using slightly ambiguous terminology (see e.g., [Krynicki–Mostowski 1995]). In this paper notation for prefixes and related quantifiers will be the same.
By Hn we denote a Henkin prefix of the following form:
x1y1
......
......
xnyn
Prefixes of this form we will call a simple Henkin prefix.
By we denote a Henkin prefix of the following form:
x1y1
......
......
xnyn
zzw1
......
zzwk
1.2Definition (Language with branched quantifiers)
Let H be a set of all branched prefixes. We define F(H) – the set of all formulae of vocabulary build up with connectives: ¬, , , , , elementary quantifiers: , , and elements of H as additional quantifiers – in the same way as formulae of elementary logic taking the following additional construction rule:
if QH and is a formula then Q is a formula.
For formulae of the form Q we define: x is a free variable in the formula Q, if x is an element of the set V(Q) = V()\{x1, ..., xn}, where x1, ..., xn are all variables occurring in Q and V() is the set of free variables in .
1.3 Definition (Skolemization of branched prefixes)
Let Q be a Henkin prefix binding universal variables x1, ..., xn and existential variables y1, ..., yk ; let xi be a sequence of the universal variables of Q on which yidepends in Q, for i = 1, ..., k. Then we define a skolemization of Q relative toQ, sk(Q, ), as the results of substituting in of fi(xi) in place yi, for i = 1, ..., k. The function symbols f1, ..., fk introduced in this way have to be new and distinct from one another. They are called the Skolem functions introduced by skolemization of Q relative to Q.
1.4 Definition (Logic with branched quantifiers L*)
We define a logic L* as an assignment to every vocabulary of a pair L= (F(H),╞L), where╞L is an extension of the satisfaction relation for elementary logic by the following condition:
M╞LQ[p] if and only if there are operations F1, ..., Fk defined on the universe of M such that (M, F1, ..., Fk)╞Lxsk(Q, )[p], where F1, ..., Fk interpret the respective Skolem functions introduced by skolemization of Q relative to Q, ’ is the extension of the vocabulary by these Skolema functions, andx is a sequence of all universal variables of Q.
By L(Hn)n, L(A)n, L()n,k we denote respectively logics which are the extensions of the elementary logic by all formulae with quantifiers Hn, A,, for n, k = 2, 3, ...
By a simple positive formula of a given logic with branched quantifiers we will call the formula Q, where is a quantifier free formula and Q is a quantifier prefix.
1.5 Definition (Lformula)
By Lformula (for the fixed vocabulary) we will call any formula, which belongs to the set of formulae of the logic L.
The logic with branched quantifiers is much stronger than the elementary logic. In this logic we can express many of the concepts, which are not expressible in the elementary logic. For example, in the logic L* the concept of infinity is expressible. Thus there is a sentence of the logic L* (called the Ehrenfeucht sentence) true exactly in the infinite models. The Ehrenfeucht sentence has the following form:
x1y1
t [(x1 = x2y1 = y2) ty1]
x2y2
1.1 Theorem ( [Enderton 1970] )
For every second order formula which belongs to the class () there is a L*–formula such that is equivalent to.
1.2 Theorem ( [Enderton 1970] )
For every L*–formula there is a second order formula which belongs to the class such that is equivalent to.
The aforementioned theorems allow to evaluate the semantic power of the logic L*. These theorems show that the logic with branched quantifiers is weaker than the class , but at least so strong as the class of Boolean combinations of . It is known that in infinite models the above inequalities are sharp, while in the case of finite models we cannot even decide whether the class is equivalent to L*.
1.6 Theorem
In any models:
L(Hn)n L(A)nL()n,kL*
Proof
Let K and K’ be classes of quantifiers on the left and right member of any inequalities in our theorem accordingly. Then, any prefix QK is subprefix of some Q’K’. Therefore, the formula of the form Q, where QK, is equivalent to some formula Q’, where Q’K’, and additional variables occurring in Q’ are not free variables in .
Q.E.D.
Still it is not known whether and which of the above inequalities are strict. In particular, is interesting it whether mentioned logics (and which) are equivalent in finite models. Considering the above hierarchy we can put another question: whether quantifiers determine increasing hierarchy relative to k, that is whether L()n L(A)n, for fixed k ?
The weaker version of branched quantifiers is function quantifiers, also called Krynicki quantifiers. It is known that the logic, which is the extension of the elementary logic by all formulae with function quantifiers, is much weaker than the logic L*. For example, the theory of equality in this logic is decidable, whereas it is not decidable in L*. Moreover, the logic with function quantifiers in language with the empty vocabulary is equivalent to the logic with divisibility quantifiers.
The logic with Krynicki quantifiers was defined as sublogic of L*. It is the only sublogic of L* defined by infinite class of quantifiers, about which it is known that is essentially semantically weaker than L* [see Krynicki–Mostowski 1995]. However this logic is not determined by any class of Henkin quantifiers still we do not know any essentially infinite class of Henkin quantifiers X such that L(X) is semantically weaker than L*.
1.6 Definition (Krynicki quantifier)
For any natural number n1 Krynicki quantifier (or functionquantifier) Fn is a quantifier binding 2n variables in one formula and it is defined by the following equivalence:
M╞ Fnx1 ... xny1 ... yn (x1, ..., xn, y1, ..., yn)[p] iff there is a function F : MM such that (M, F)╞ (x1, ..., xn, f(x1), ..., f(xn))[p], where f is interpreted as F.
By L(Fn)n we denote the logic which is the extension of the elementary logic by all formulae with quantifiers Fn, for n = 2, 3, ...
1.7 Definition. (Divisibility quantifier)
For any natural number n1 divisibility quantifierDn is defined by the following equivalence:
Dnx(x) iff card({x : (x)}) is divisible by n or infinite
By L(Dn)n we denote the logic which id the extension of the elementary logic by all formulae with quantifiers Dn, for n = 2, 3, ...
THE SPECTRUM PROBLEM – GENERAL FORMULATION
Actually, the spectrum problem is usually considered in the framework of feasible – descriptive correspondence. In this section we will consider classical model theoretic formulation of the spectrum problem, particularly for the case of empty vocabulary.
2.1Definition (The spectrum of a formula)
Let be any sentence for fixed vocabulary . The spectrumof a formula, Spec(), is the set:
Spec() = df {n : there is a model M such that card(M) = nand M╞ }.
2.2Definition (The spectrum of a logic L)
Let FL be a set of sentences of the logic L for the fixed vocabulary . The spectrum of the logic L, Spec(L), is the set:
Spec(L) =df {Spec() : FL}
If there is a formula of the logic L such that the spectrum of is the set A, we will say that the set A is L–spectrum.
Original versions of the spectrum problem
IGeneralized Scholz problem.
Let L be any logic for the fixed vocabulary . What is Spec(L) ?
IIAsser problem.
Let L be any logic for the fixed vocabulary . Does for every set A , which belongs to Spec(L), complement of A also belongs to Spec(L)?
Of course, the solution of Scholz problem immediately gives the solution of Asser problem.
Weak versions of the spectrum problem
I The spectrum problem for a language in empty vocabulary.
Let L be any logic in the empty vocabulary. What is Spec(L)?
II The spectrum problem for first order language in empty vocabulary.
Let L’ be elementary logic in the empty vocabulary. What is Spec(L’)?
2.1 Theorem
Let L’ be elementary logic in the empty vocabulary. Then:
Spec(L’) = {A : card(A) < } {A : card( \ A) < }.
Proof
() It is obvious.
() Let us assume that there is a set A Spec(L’) such that A is not finite and is not co–finite. Since A Spec(L’) there is a formula of the logic L’ such that Spec() = A. Then and also ¬ have finite models of arbitrary large cardinality. It follows that and ¬ have countable models. Let M be a countable model for , and M¬ a countable model for ¬. Since the logic L’ is in the empty vocabulary M M¬.. Therefore M╞ and M ╞ ¬., so M ╞ and ¬M ╞ . Contradiction.
Q.E.D
The subject of our investigations is the spectrum problem formulated for the logics with branched quantifiers in the empty vocabulary. Particularly we are interested in the characterization of spectra of the logics L*, L(Hn)n, L(A)n, L()n,k.
The weak spectrum problem for languages with Henkin quantifiers.
Let L*, L(Hn)n, L(A)n, L()n,k be the logics in the empty vocabulary defined in section I. What are these :
Spec(L*) = ?
Spec(L(Hn)n)) = ?
Spec(L(A)n) = ?
Spec(L()n,k) = ?
Let us observe that we have the following obvious theorem:
2.2 Theorem
Let L and L’ be logics such that L L’. Then Spec(L) Spec(L’).
Further in the paper we restrict our interest to logics in the empty vocabulary.
THE SPECTRUM PROBLEM FOR LANGUAGES WITH HENKIN QUANTIFIERS
We will start with discussion of the solution for the spectrum problem for the logic with Krynicki quantifiers. There are two reasons for this. Firstly, the solution can be treated as paradigmatic for our case of logics with Henkin quantifiers. Secondly, because the spectrum of the logic with Krynicki quantifiers is a subset of the spectrum of the logic with all Henkin quantifiers.
3.1Definition (The restriction of a formula to a formula)
Let be a formula of the logic with Krynicki quantifiers and (z) any formula with distinguished variable z. We define inductively (z) – the restriction of to relative to z:
1)(z) = , if is a quantifier free formula;
2)((z)) = (z);
3)(12)(z) = (1(z)2(z));
4)(x )(z) = x ((x) (z));
5)[Fnx1 ... xny1 ... yn(x1, ..., xn, y1, ..., yn)](z) = Fnx1... xn y1... yn[(x1) (xn) (y1) .... (yn) ( (x1, ..., xn, y1, ..., yn))(z)].
Let us note that in a case of conflict of bounded variables in we should rename these variables.
3.1 Theorem[2]
For each natural number n>1 the quantifier Dn is definable by the quantifier Fn in the following way:
Dn x(x) Fnx1... xny1... yn {[¬(x1 = y1)] [ij(yi = yjxi = xj)] n(x1, ..., xn, y1, ..., yn) n (x1, ..., xn, y1, ..., yn)}(x)
Where formulae n and n have the following form:
n (x1, ..., xn, y1, ..., yn) = [( yi = xi+1) yn = x1],
n’(x1, ..., xn, y1, ..., yn) = [(yi = xi+1) (yn= x1)],
n (x1, ..., xn, y1, ..., yn) = [(i1, ..., ik) (1, ..., n) k’(xi1, ..., xik, yi1,..., yik)]
3.2 Theorem2
For any natural number n1 a function quantifier Fn is definable by a simple Henkin quantifier Hnin the following way:
Fnx1... xn y1... yn(x1, ..., xn, y1, ..., yn)
Hnx1 ... xny1... yn {(x1, ..., xn, y1, ..., yn) [ij (xi = xjyi= yj)]}.
3.3Theorem ([Krynicki – Mostowski 1992])
The theory of equality in L(Fn)n and the theory of equality in L(Dn)n are recursively equivalent i.e., for every formula of the theory of equality in L(Fn)n there is effectively found semantically equivalent formula of the theory of equality in L(Dn)n.
3.4Theorem ([Mostowski 199?])
Spec(L(Dn)n) = Bool({A : card(A) < } {{x : xa (mod b), ab, a, b}})
3.1 Corollary (from theorem 3.3)
Spec(L(Dn)n) = Spec(L(Fn)n)
3.2 Corollary (from theorem 3.2)
Spec(L(Fn)n) Spec(L(Hn)n)
It is known that the above inclusion is proper (see [Krynicki–Mostowski 1995]).
3.3 Corollary (from theorem 1.5)
Spec(L(Hn)n) Spec(L(A)n) Spec(L()n,k) Spec(L*)