On the decision problem for theories of finite models
Tóm tắt
An infinite extension of the elementary theory of Abelian groups is constructed, which is proved to be decidable, while the elementary theory of its finite models is shown to be undecidable. Tarski’s proof of undecidability for the elementary theory of Abelian cancellation semigroups is presented in detail. Szmielew’s proof of the decidability of the elementary theory of Abelian groups is used to prove the decidability of the elementary theory of finite Abelian groups, and an axiom system for this theory is exhibited. It follows that the elementary theory of Abelian cancellation semigroups, while undecidable, has a decidable theory of finite models.
Tài liệu tham khảo
Cobham, A., 1962, Undecidability in group theory,Amer. Math. Soc. Notices,9, 406.
Eršov, U., 1963, Razrešimost’ èlementarnyh, teorii nekotoryh klassov abelevyh grupp (Decidability of certain classes of Abelian groups).Algebra i Logika Seminar,1, 37–41.
Huber Dyson, V., 1963, A decidable theory for which the theory of finite models is undecidable,Amer. Math. Soc. Notices,10, 453.
Huber Dyson, V., 1963, A decidable theory for which the theory of infinite models is undecidable,Amer. Math. Soc. Notices,10, 491.
Janiczak, A., 1953, Undecidability of some simple formalized theories,Fund Math.,40, 131–139.
Langford, C., 1927, On a type of completeness characterizing the general laws for separation of pointpairs,Trans. Amer. Math. Soc.,29, 96–110.
Mal’cev, A., 1961, Effective inseparability of the set of identically true from the set of finitely refutable formulas of certain elementary theories,Soviet Mathematics,2, 1005–1008. (Original in Russian:Doklady Akadémii Nauk,139, (1961) 802–805).
Szmielew, W., Elementary properties of Abelian groups.Fund. Math.,41 1955, pp. 203–271.
Taiclin, M. Nerazresimost’ èlementarnoi teorii kommutativnyh polygrupp so sokrascenem (Undecidability of the elementary theory of commutative semigroup with cancellation).Sibirskii Matematiceskii Zhurnal,3, (1962), pp. 308–309.
Taiclin, M., 1962, Effektivnaya neotdelimost’ množestva toždestvenno istinnyh i množestva konečno oproveržimyh formul èlementarnoi teorii struktur (Effective inseparability of the set of identically true and the set of finitely refutable formulas of the elementary theory of lattices).Algebra i Logika Seminar,1, 24–38.
Tarski, A., 1949, Arithmetical classes and types of Boolean algebras,Bull. Amer, Math. Soc.,55, 64.
Tarski, A., Robinson, R.M. and Mostowski, A., 1953,Undecidable Theories, North Holland Publ. Co., Amsterdam.
Tarski, A., 1962, Solution of the decision problem for the elementary theory of commutative semigroups,Amer. Math. Soc. Notices,9, 205.
Trahtènbrot, B., 1950, Nevozmožnost’ algorifma dlya problemy razešiomstina konečnyh klassah (Impossibility of an algorithm for the decision problem in finite classes).Doklady Akadémii Nauk, SSSR,70, 569–572.
Vaught, R., 1962, On a theorem of Cobham concerning undecidable theories,Proceedings of the 1960International Congress on Logic, Methodology and Philosophy of Science, Stanford pp. 14–25.