Journal article icon

Journal article

The expressiveness and complexity landscape for evaluating formulas over embedded finite models

Abstract:
We revisit evaluation of logical formulas that allow both uninterpreted relations, constrained to be finite, as well as an interpreted vocabulary over an infinite domain. This formalism was denoted embedded finite model theory in the past. It is clear that the expressiveness and evaluating complexity of formulas of this type depends heavily on the infinite structure. If we embed in a wild structure like the integers with additive and multiplicative arithmetic, logic is extremely expressive and formulas are impossible to evaluate. On the other hand, for some well-known decidable structures, the expressiveness and evaluating complexity are similar to the situation without the additional infrastructure. The latter phenomenon was formalized via the notion of “Restricted Quantifier Collapse”: adding quantification over the infinite structure does not add expressiveness. Beyond these two extremes little was known.
In this work we show that the possibilities for expressiveness and complexity are much wider. We show that we can get almost any possible complexity of evaluation while staying within a decidable structure. We also show that in some decidable structures, there is a disconnect between expressiveness of the logic and complexity, in that we cannot eliminate quantification over the structure, but this is not due to an ability to embed complex relational computation in the logic. 
We show failure of collapse for the theory of finite fields and the related theory of pseudo-finite fields, which will involve coding computation in the logic. As a by-product of this, we establish the first lower bounds for the complexity of decision procedures for several decidable theories of fields, including the theory of finite fields.
Publication status:
Published
Peer review status:
Peer reviewed

Actions

Access Document

Publisher copy:
10.1017/jsl.2026.10195

Authors

More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
University College
Role:
Author
ORCID:
0000-0003-2964-0880
More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Mathematical Institute
Role:
Author
ORCID:
0000-0002-2761-6513


More from this funder
Funder identifier:
https://ror.org/0439y7842
Grant:
EP/T022124/1


Publisher:
Cambridge University Press
Journal:
Journal of Symbolic Logic More from this journal
Publication date:
2026-02-26
Acceptance date:
2026-01-28
DOI:
EISSN:
1943-5886
ISSN:
0022-4812


Language:
English
Keywords:
Pubs id:
2377094
Local pid:
pubs:2377094
Deposit date:
2026-02-17
ARK identifier:

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP