Structure with fast elimination of quantifiers. (English) Zbl 1100.03018

Summary: A structure of finite signature is constructed so that: for all existential formulas \(\exists\vec y\) \(\varphi(\vec x,\vec y)\) and for all tuples of elements \(\vec u\) of the same length as the tuple \(\vec x\), one can decide in a quadratic time depending only on the length of the formula, whether \(\exists\vec y\) \(\varphi(\vec u,\vec y)\) holds in the structure. In other words, the structure satisfies the relativized model-theoretic version of \(\text{P}=\text{NP}\) in the sense of B. Poizat [Les petits cailloux. Lyon: Aléas (1995; Zbl 0832.68044)]. This is a model-theoretical approach to results of Hemmerling and Gaßner.


03C10 Quantifier elimination, model completeness, and related topics
03B25 Decidability of theories and sets of sentences
03D15 Complexity of computation (including implicit computational complexity)
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)


Zbl 0832.68044
Full Text: DOI


[1] DOI: 10.1002/1521-3870(200111)47:4&lt;557::AID-MALQ557&gt;3.0.CO;2-O · Zbl 0992.03042 · doi:10.1002/1521-3870(200111)47:4<557::AID-MALQ557>3.0.CO;2-O
[2] Les petits cailloux (1995)
[3] A structure of finite signature with identity relation and with P = NP–A formal proof (2004)
[4] DOI: 10.1016/j.jco.2005.02.001 · Zbl 1101.68034 · doi:10.1016/j.jco.2005.02.001
[5] DOI: 10.2307/2024634 · Zbl 0952.03513 · doi:10.2307/2024634
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.