Spectrum of a sentence

Last updated November 02, 2022

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.

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.

Properties

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).

Equivalence to Turing machines

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.

Related Research Articles

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—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, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. 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 mathematical logic, model theory is the study of the relationship between formal theories, and their models. The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself. In particular, model theorists also investigate the sets that can be defined in a model of a theory, and the relationship of such definable sets to each other. As a separate discipline, model theory goes back to Alfred Tarski, who first used the term "Theory of Models" in publication in 1954. Since the 1970s, the subject has been shaped decisively by Saharon Shelah's stability theory.

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

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.

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not include the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

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 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 computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.

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.$

In mathematical logic, Heyting arithmetic $is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.$

In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.

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

In model theory and related areas of mathematics, a type is an object that describes how a element or finite collection of elements in a mathematical structure might behave. More precisely, it is a set of first-order formulas in a language L with free variables x₁, x₂,…, x_n that are true of a sequence of elements of an L-structure $. Depending on the context, types can be complete or partial and they may use a fixed set of constants, A, from the structure . The question of which types represent actual elements of leads to the ideas of saturated models and omitting types .$

In modal logic, standard translation is a way of transforming 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, the quantifier rank of a formula is the depth of nesting of its quantifiers. It plays an essential role in model theory.

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.

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.

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.

[mwew] 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.

[1]