Theories of arithmetics in finite models. (English) Zbl 1094.03022

Let \(A\) be a first-order structure whose universe is \(\omega\). For each \(n<\omega\), let \(A_n\) denote the (naturally defined) restriction of \(A\) to \(\{0,\dots, n\}\). Let FM\((A)\) be the family of all \(A_n\)’s. Marcin Mostowski introduced the notion of satisfiability in sufficiently large finite models in FM\((A)\). This is the central notion of the paper.
The focus is on decidability and other properties of the suitably defined theory Th(FM\((A))\), and the theory of sufficiently large models sl(FM\((A))\), where \(A\) is one of the standard models of the form \((\omega, +)\), \((\omega, \times)\), \((\omega, \times, \leq)\), or \((\omega, \exp)\). It is a substantial paper, I only list some of the main results.
In Section 4, the authors prove that the set of \(\Sigma_2\) sentences of arithmetic of multiplication which are satisfiable in finite models is \(\Sigma^0_1\)-complete, and the set of those \(\Sigma_2\) sentences which are true in all sufficiently large models is \(\Sigma^0_1\)-hard. Also, for \(A\) being either \((\omega, \times)\) or \((\omega, \exp)\), Th(FM\((A))\) is \(\Pi^0_1\)-complete, and sl(FM\((A))\) is \(\Sigma^0_2\)-complete.
The main result of Section 5 is that the theory of sufficiently large models in FM\((\omega, \times,\leq)\) is decidable and so is the existential theory of the standard model of multiplication and order.
In Section 6 the authors consider the arithmetic of concatenation and show that in finite models it has the same strength as the arithmetic of addition and multiplication.
The FM\((A)\)-spectrum of a sentence \(\varphi\) is the set \(\{n+1: A_n\models \varphi\}\). The spectrum of FM\((A)\) is the set of all FM\((A)\)-spectra of all sentences of the language of FM\((A)\). Section 7 contains several interesting results concerning the spectra of FM\((A)\) for various \(A\). In particular, it is shown that the spectrum of exponentiation is strictly contained in the spectrum of addition and multiplication.


03C13 Model theory of finite structures
03C68 Other classical first-order model theory
03F30 First-order arithmetic and fragments
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
03B25 Decidability of theories and sets of sentences
Full Text: DOI


[1] Metamathematics of first-order arithmetic (1993) · Zbl 0781.03047
[2] Izv. Akad. Nauk SSSR ser. Mat. 47 pp 623– (1983)
[3] Mathematical Journal Quarterly 44 pp 349– (1998)
[4] DOI: 10.2307/2318447 · Zbl 0277.02008
[5] DOI: 10.1002/malq.19600060105 · Zbl 0103.24705
[6] DOI: 10.1016/S0168-0072(97)85376-6 · Zbl 0889.11008
[7] DOI: 10.1016/0022-0000(90)90022-D · Zbl 0719.68023
[8] 14th IEEE Symposium on Logic in Computer Science (LICS) 14 pp 275– (1999)
[9] Elementary methods in number theory (2000) · Zbl 0953.11002
[10] Locally finite theories 51 pp 59– (1986)
[11] Analysis without actual infinity 46 pp 625– (1981)
[12] DOI: 10.1002/malq.200310086 · Zbl 1045.03036
[13] DOI: 10.1007/978-94-017-2612-2_2
[14] DOI: 10.1002/1521-3870(200111)47:4&lt;513::AID-MALQ513&gt;3.0.CO;2-J · Zbl 0992.03043
[15] DOI: 10.1002/malq.200310041 · Zbl 1022.03015
[16] Proceedings of the 5th Conference on Discrete Mathematics and Applications, Blagoevrad pp 91– (1995)
[17] Logical number theory I (1981)
[18] Recursion theory (1993)
[19] Mathematical logic (1994)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.