Spectrum of a sentence

Last updated January 20, 2025

In mathematical logic, the spectrum of a sentence is the set of natural numbers occurring as the size of a finite model in which a given sentence is true. By a result in descriptive complexity, a set of natural numbers is a spectrum if and only if it can be recognized in non-deterministic exponential time.

Definition

Let ψ be a sentence in first-order logic. The spectrum of ψ is the set of natural numbers n such that there is a finite model for ψ with n elements.

If the vocabulary for ψ consists only of relational symbols, then ψ can be regarded as a sentence in existential second-order logic (ESOL) quantified over the relations, over the empty vocabulary. A generalised spectrum is the set of models of a general ESOL sentence.

Examples

The spectrum of the first-order formula

$\exists z,o~\forall a,b,c~\exists d,e$

a+z=a=z+a~\land ~a\cdot z=z=z\cdot a~\land ~a+d=z

\land ~a+b=b+a~\land ~a\cdot (b+c)=a\cdot b+a\cdot c~\land ~(a+b)+c=a+(b+c)

\land ~a\cdot o=a=o\cdot a~\land ~a\cdot e=o~\land ~(a\cdot b)\cdot c=a\cdot (b\cdot c)

is $\{p^{n}\mid p{\text{ prime}},n\in \mathbb {N} \}$ , the set of powers of a prime number. Indeed, with $z$ for $0$ and $o$ for $1$ , this sentence describes the set of fields; the cardinality of a finite field is the power of a prime number.

The spectrum of the monadic second-order logic formula $\exists S,T~\forall x~\left\{x\in S\iff x\not \in T\land ~f(f(x))=x\land ~x\in S\iff f(x)\in T\right\}$ is the set of even numbers. Indeed, $f$ is a bijection between $S$ and $T$ , and $S$ and $T$ are a partition of the universe. Hence the cardinality of the universe is even.
The set of finite and co-finite sets is the set of spectra of first-order logic with the successor relation.
The set of ultimately periodic sets is the set of spectra of monadic second-order logic with a unary function. It is also the set of spectra of monadic second-order logic with the successor function.

Descriptive complexity

Fagin's theorem is a result in descriptive complexity theory that states that the set of all properties expressible in existential second-order logic is precisely the complexity class NP. It is remarkable since it is a characterization of the class NP that does not invoke a model of computation such as a Turing machine. The theorem was proven by Ronald Fagin in 1974 (strictly, in 1973 in his doctoral thesis).

As a corollary, Jones and Selman showed that a set is a spectrum if and only if it is in the complexity class NEXP.^[1]

One direction of the proof is to show that, for every first-order formula $\varphi$ , the problem of determining whether there is a model of the formula of cardinality n is equivalent to the problem of satisfying a formula of size polynomial in n, which is in NP(n) and thus in NEXP of the input to the problem (the number n in binary form, which is a string of size log(n)).

This is done by replacing every existential quantifier in $\varphi$ with disjunction over all the elements in the model and replacing every universal quantifier with conjunction over all the elements in the model. Now every predicate is on elements in the model, and finally every appearance of a predicate on specific elements is replaced by a new propositional variable. Equalities are replaced by their truth values according to their assignments.

For example:

$\forall {x}\forall {y}\left(P(x)\wedge P(y)\right)\rightarrow (x=y)$

For a model of cardinality 2 (i.e. n= 2) is replaced by

${\big (}\left(P(a_{1})\wedge P(a_{1})\right)\rightarrow (a_{1}=a_{1}){\big )}\wedge {\big (}\left(P(a_{1})\wedge P(a_{2})\right)\rightarrow (a_{1}=a_{2}){\big )}\wedge {\big (}\left(P(a_{2})\wedge P(a_{1})\right)\rightarrow (a_{2}=a_{1}){\big )}\wedge {\big (}\left(P(a_{2})\wedge P(a_{2})\right)\rightarrow (a_{2}=a_{2}){\big )}$

Which is then replaced by ${\big (}\left(p_{1}\wedge p_{1}\right)\rightarrow \top {\big )}\wedge {\big (}\left(p_{1}\wedge p_{2}\right)\rightarrow \bot {\big )}\wedge {\big (}\left(p_{2}\wedge p_{1}\right)\rightarrow \bot {\big )}\wedge {\big (}\left(p_{2}\wedge p_{2}\right)\rightarrow \top {\big )}$

where $\top$ is truth, $\bot$ is falsity, and $p_{1}$ , $p_{2}$ are propositional variables. In this particular case, the last formula is equivalent to $\neg (p_{1}\wedge p_{2})$ , which is satisfiable.

The other direction of the proof is to show that, for every set of binary strings accepted by a non-deterministic Turing machine running in exponential time ( $2^{cx}$ for input length x), there is a first-order formula $\varphi$ such that the set of numbers represented by these binary strings are the spectrum of $\varphi$ .

Jones and Selman mention that the spectrum of first-order formulas without equality is just the set of all natural numbers not smaller than some minimal cardinality.

Other properties

The set of spectra of a theory is closed under union, intersection, addition, and multiplication. In full generality, it is not known if the set of spectra of a theory is closed by complementation; this is the so-called Asser's problem. By the result of Jones and Selman, it is equivalent to the problem of whether NEXPTIME = co-NEXPTIME; that is, whether NEXPTIME is closed under complementation.^[2]

Related Research Articles

First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables. Rather than propositions such as "all men are mortal", in first-order logic one can have expressions in the form "for all x, if x is a man, then x is mortal"; where "for all x" is a quantifier, x is a variable, and "... is a man" and "... is mortal" are predicates. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox. Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics. Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated ZFC, where C stands for "choice", and ZF refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded.

Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related. They may be viewed as a family of substructural or modal logics. It is generally, but not universally, called relevant logic by British and, especially, Australian logicians, and relevance logic by American logicians.

A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in propositional logic, it provides a canonical normal form useful in automated theorem proving.

In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all ordinals. Morse–Kelley set theory (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

In formal logic, nonfirstorderizability is the inability of a natural-language statement to be adequately captured by a formula of first-order logic. Specifically, a statement is nonfirstorderizable if there is no formula of first-order logic which is true in a model if and only if the statement holds in that model. Nonfirstorderizable statements are sometimes presented as evidence that first-order logic is not adequate to capture the nuances of meaning in natural language.

In proof theory, the semantic tableau, also called an analytic tableau, truth tree, or simply tree, is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.

Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form $and, where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.$

Circumscription is a non-monotonic logic created by John McCarthy to formalize the common sense assumption that things are as expected unless otherwise specified. Circumscription was later used by McCarthy in an attempt to solve the frame problem. To implement circumscription in its initial formulation, McCarthy augmented first-order logic to allow the minimization of the extension of some predicates, where the extension of a predicate is the set of tuples of values the predicate is true on. This minimization is similar to the closed-world assumption that what is not known to be true is false.

In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering

In theoretical computer science, the modal μ-calculus is an extension of propositional modal logic by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic.

In mathematical logic, Skolem arithmetic is the first-order theory of the natural numbers with multiplication, named in honor of Thoralf Skolem. The signature of Skolem arithmetic contains only the multiplication operation and equality, omitting the addition operation entirely.

In set theory and mathematical logic, the Lévy hierarchy, introduced by Azriel Lévy in 1965, is a hierarchy of formulas in the formal language of the Zermelo–Fraenkel set theory, which is typically called just the language of set theory. This is analogous to the arithmetical hierarchy, which provides a similar classification for sentences of the language of arithmetic.

In modal logic, standard translation is a logic translation that transforms formulas of modal logic into formulas of first-order logic which capture the meaning of the modal formulas. Standard translation is defined inductively on the structure of the formula. In short, atomic formulas are mapped onto unary predicates and the objects in the first-order language are the accessible worlds. The logical connectives from propositional logic remain untouched and the modal operators are transformed into first-order formulas according to their semantics.

In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query languages, in particular to Datalog.

In first-order arithmetic, the induction principles, bounding principles, and least number principles are three related families of first-order principles, which may or may not hold in nonstandard models of arithmetic. These principles are often used in reverse mathematics to calibrate the axiomatic strength of theorems.

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories $are referred to as "the formal theories of ν-times iterated inductive definitions". ID ν extends PA by ν iterated least fixed points of monotone operators.$

References

↑ Jones, Neil D.; Selman, Alan L. (1974). "Turing machines and the spectra of first-order formulas". J. Symb. Log. 39 (1): 139–150. doi:10.2307/2272354. JSTOR 2272354. Zbl 0288.02021.
↑ Szwast, Wiesław (1990). "On the generator problem". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 36 (1): 23–27. doi:10.1002/malq.19900360105. MR 1030536.

Fagin, Ronald (1974). "Generalized First-Order Spectra and Polynomial-Time Recognizable Sets" (PDF). In Karp, Richard M. (ed.). Complexity of Computation. Proc. Syp. App. Math. SIAM-AMS Proceedings. Vol. 7. pp. 27–41. Zbl 0303.68035.
Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer-Verlag. doi:10.1007/3-540-68804-8. ISBN 978-3-540-00428-8. Zbl 1133.03001.
Immerman, Neil (1999). Descriptive Complexity. Graduate Texts in Computer Science. New York: Springer-Verlag. pp. 113–119. ISBN 0-387-98600-6. Zbl 0918.68031.
Durand, Arnaud; Jones, Neil; Markowsky, Johann; More, Malika (2012). "Fifty Years of the Spectrum Problem: Survey and New Results". Bulletin of Symbolic Logic. 18 (4): 505–553. arXiv: 0907.5495 . Bibcode:2009arXiv0907.5495D. doi:10.2178/bsl.1804020. S2CID 9507429.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] Jones, Neil D.; Selman, Alan L. (1974). "Turing machines and the spectra of first-order formulas". J. Symb. Log. 39 (1): 139–150. doi:10.2307/2272354. JSTOR 2272354. Zbl 0288.02021.

[2] Szwast, Wiesław (1990). "On the generator problem". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 36 (1): 23–27. doi:10.1002/malq.19900360105. MR 1030536.

[1]

[2]