On the equivalence of two quantifier elimination tests
Yimu Yin
我们证明了，对于可数语言，两个模型论量词消除测试，一个由J。Shoenfield和L. van den Dries是等价的。
We prove that, for countable languages, two model-theoretic quantifier elimination tests, one proposed by J. R. Shoenfield and the other by L. van den Dries, are equivalent.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Affinization and quantifier-elimination
本文证明若干经典一阶理论的仿射部分具有量词消去性质或模型完备性。
We prove quantifier elimination for the theory of quasi-real closed fields with a compatible valuation. This unifies the same known results for algebraically closed valued fields and real closed valued fields.
In this paper, we give appropriate languages in which the theory of tame fields (of any characteristic) admits (relative) quantifier elimination.
Elimination of quantifiers is shown to fail dramatically for a group of well-known mathematical theories (classically enjoying the property) against a wide range of relevant logical backgrounds. Furthermore, it is suggested that only by moving to more extensional underlying logics can we get the property back.
Quantifier elimination in ordered abelian groups
用适当的语言给出了全序阿贝尔群理论中量词消去的一个新证明。更确切地说，这只是“相对于有序集的量词消除”。群中的每个可定义集合都是一个无量词可定义集合族的并集，其中该族的参数在一个排序中运行于一个可定义（有量词）的集合上，该排序携带一个有序集合的结构，并带有一些额外的一元谓词。作为推论，我们发现序阿贝尔群中的所有可定义函数都是关于n个可定义段的分段仿射线性函数。
Quantifier elimination for lovely pairs of strongly geometric fields
本文研究了强几何域的可爱对理论，证明其在定义扩展下具有可消除性，并作为特殊情况获得了实闭域和p-进闭域理论的可消除性。
Adjoining to the language of rings the function symbols for splitting coefficients, the function symbols for relative $p$-coordinate functions, and the division predicate for a valuation, some theories of pseudo-algebraically closed non-trivially valued fields admit quantifier elimination. It is also shown that in the same language the theory of pseudo-algebraically closed non-trivially valued fields of a given exponent of imperfection does not admit quantifier elimination, due to Galois theoretic obstructions.
Let $R$ be an o-minimal expansion of a group in a language in which $\textrm{Th}(R)$ eliminates quantifiers, and let $C$ be a predicate for a valuational cut in $R$. We identify a condition that implies quantifier elimination for $\textrm{Th}(R,C)$ in the language of $R$ expanded by $C$ and a small number of constants, and which, in turn, is implied by $\textrm{Th}(R,C)$ having quantifier elimination and being universally axiomatizable. The condition applies for example in the case when $C$ is a convex subring of an o-minimal field $R$ and its residue field is o-minimal.
Quantifier elimination and minimality conditions in algebraically closed valued fields
在Hrushovski-Kazhdan积分理论中引入了Basarab-Kuhlmann风格的语言L_RV。代数闭值域的理论ACVF用这种语言表述，允许量词消去。本文利用值域理论中的一些著名事实，给出了这一事实的一个直接证明。我们还表明，ACVF的两个扩展，一个部分的整个RV排序和其他部分的剩余域，承认量词消除。此后，我们表明，在某些极小条件，这三个理论是不同的几何。
Model completeness and quantifier elimination for (ordered) central simple algebras with involution
本文证明实闭域上某些（有序）带对合的中央单代数的理论具有模型完备性或量词消去，并用态射刻画正锥，主要结果归功于Nicolas Daans。
Quantifier Elimination and Invariant Theory: Applications to Quaternions, Octonions, and Other Algebras
本文利用先前方法和不变量理论，实现了四元数、八元数及其他有限维代数的量词消除结果，回答了近期提出的开放问题。
Quantifier Elimination for Valued Fields Equipped with an Automorphism
我们提供公理化和相对量词消除价值领域配备了自同构，在剩余特征零。类似的结果是已知的强假设之间的相互作用的自同构和估值。我们删除这些假设，并提供一般处理。作为结果，我们得到一个公理化的transseries领域（作为一个价值领域的自同构）配备了自同构发送f（x）的f（x+1）。
Some (non-)elimination results for curves in geometric structures
证明了以$\mathbb C$为基础论域、以$\mathbb C^2$的代数子集为基本关系的一阶结构不存在量词消去。由于$\mathbb C ^2$的代数子集需要是$\leq 1$维的或者需要有$\leq 1$维的补集，所以可以将前一个结果重述为平面复代数曲线的量词消去失败。然后，我们证明，消除平面性假设足以恢复量词消除：宇宙$\mathbb C$和谓词的每个代数子集的$\mathbb C^n$维度$\leq 1$的结构具有量词消除。
Almost free algebras: from the word problem to elimination of quantifiers
本文研究近自由代数的多项式时间可解性，包括词问题、同余类基数计算及同构检查等，同时证明其可通过扩展语言实现量词消去。
Relative Quantifier Elimination for Separable-Algebraically Maximal Kaplansky Fields
本文在含角分量与参数化 λ-函数的三种类语言中，证明等特征可分代数极大 Kaplansky 域的公共理论可相对剩余域和值群辉煌消去量词，并导出 NIP Hensel 域及 AKE 原则等结论。
Quantifier elimination in II$_1$ factors
本文证明了不存在任何II$_1$迹von Neumann代数具有可消去量词的理论。
Constructive Quantifier Elimination with a Focus on Matrix Rings
该研究针对模型论结构的量词消去问题，提出了结构间继承量词消去的充分条件，为特定矩阵环的量词消去给出了更简短的构造性算法证明。
We give an algorithm determining whether a hermiticity-preserving superoperator is positive. In our approach we apply techniques of quantifier elimination theory for real numbers. Furthermore, we argue that quantifier elimination theory should play more significant role in quantum information theory and other areas as well.
Monomialization of morphisms and p-adic quantifier elimination
我们给出了一个简短的证明麦金太尔的量词消除的p进数定理，使用单性化的版本，直接从阿布拉莫维奇和卡鲁的弱Toroidization定理（扩展到非封闭领域）。
Projectable reduced $f$-rings admitting elimination of quantifiers
本文在带可除性关系、与极小素谱相关的根关系以及局部可除性关系的格序环语言中，刻画了所有满足第一凸性性质且可消去量词的可投射和可除-可投射约化 $f$-环。
A general approach to asymptotic elimination of aggregation functions and generalized quantifiers
本文提出一种基于局部连续性概念的一般方法，用于渐近消除单位区间真值逻辑中的聚合函数，并间接消除莫斯托夫斯基风格广义量词。
The only C*-algebras that admit elimination of quantifiers in continuous logic are $\mathbb{C}, \mathbb{C}^2$, $C($Cantor space$)$ and $M_2(\mathbb{C})$. We also prove that the theory of C*-algebras does not have model companion and show that the theory of $M_n(\mathcal {O_{n+1}})$ is not $\forall\exists$-axiomatizable for any $n\geq 2$.
Work of Eagle, Farah, Goldbring, Kirchberg, and Vignati shows that the only separable C*-algebras that admit quantifier elimination in continuous logic are $\mathbb{C},$ $\mathbb{C}^2,$ $M_2(\mathbb{C}),$ and the continuous functions on the Cantor set. We show that, among finite dimensional C*-algebras, quantifier elimination does hold if the language is expanded to include two new predicate symbols: One for minimal projections, and one for pairs of unitarily conjugate projections. Both of these predicates are definable, but not quantifier-free definable, in the usual language of C*-algebras. …
Assume that $ACF$ denotes the theory of algebraically closed fields. The renowned theorem of A. Tarski states that $ACF$ admits quantifier elimination. In this paper we give a constructive proof of Tarski's theorem on quantifier elimination in $ACF$. This means that for a given formula $φ$ of the language of fields we construct a quantifier-free formula $φ'$ such that $ACF\vdashφ\leftrightarrowφ'$. We devote the last section of the paper to show some applications of this constructive version in mathematics and physics.
The first-order theory of geometric points of schemes: Chevalley's theorem and quantifier elimination
Chevalley关于概型态射象的定理和代数闭域理论的量词消去原理被广泛理解为同一定理的两个观点。在本文中，我们证明了这两个结果可以很容易地同时证明，使用几何和逻辑技术的混合物。在这样做的时候，我们给逻辑意义的几何点的计划，并提出了态射，在某种程度上让人想起斯宾塞Breiner的逻辑计划。
We describe a new quantifier elimination algorithm for real closed fields based on Thom encoding and sign determination. The complexity of this algorithm is elementary recursive and its proof of correctness is completely algebraic. In particular, the notion of connected components of semialgebraic sets is not used.
The Dual of Quantifier Elimination: Boolean Elimination over C and R
该研究通过证明在C和R上布尔组合的多项式等式和不等式可转换为单变量量词形式，提供了经典量词消除的对偶方法，展示了线性度数界和明确构造。
Assume that $Φ:\mathbb{M}_{n}(\mathbb{C})\rightarrow\mathbb{M}_{n}(\mathbb{C})$ is a superoperator which preserves hermiticity. We give an algorithm determining whether $Φ$ preserves semipositivity (we call $Φ$ positive in this case). Our approach to the problem has a model-theoretic nature, namely, we apply techniques of quantifier elimination theory for real numbers. An approach based on these techniques seems to be the only one that allows to decide whether an arbitrary hermiticity-preserving $Φ$ is positive. Before we go to detailed analysis of the problem, we argue that quantifier elimina…
We investigate the elimination of quantifiers in first-order formulas via Hilbert's epsilon-operator (or -binder), following Bernays' explicit definitions of the existential and the universal quantifier symbol by means of epsilon-terms. This elimination has its first explicit occurrence in the proof of the first epsilon-theorem in Hilbert-Bernays in 1939. We think that there is a lacuna in this proof w.r.t. this elimination, related to the erroneous assumption that explicit definitions always terminate. Surprisingly, to the best of our knowledge, nobody ever proved confluence or termination fo…
We prove elimination of field quantifiers for strongly dependent henselian fields in the Denef-Pas language. This is achieved by proving the result for a class of fields generalizing algebraically maximal Kaplansky fields. We deduce that if $(K,v)$ is strongly dependent then so is its henselization.
These are lecture notes for a course I gave in mid-1990s for MSc students at the University of Bath. It presents an algorithm with singly exponential complexity for the existential theory of the reals, in the spirit of J. Renegar. The aim was to convey the main underlying ideas, so many of the proofs and finer details of algorithms are either missing or just sketched. I changed nothing in the original notes except adding references, bibliography, and correcting obvious typos.
An efficient quantifier elimination procedure for Presburger arithmetic
本文提出一种可在单指数时间内消去存在量词变量块的Presburger算术量词消去过程，纠正了双重指数时间上界为紧的旧有论断，并据此确定了单元可分解性、良拟序判定及Ramsey量词公式等问题的精确复杂度。
Quantifier elimination in quasianalytic structures via non-standard analysis
本文是我们以前的文章，我们开发了一个理论的积极和非积极的无穷小，并打算建立量词消除准解析结构的延续。这篇文章，但是，没有达到充分的一般性，这是指其结果之一，即定理的积极无穷小，发挥了重要作用，在我们的非标准分析。我们随后的预印本中涵盖了一般情况，这构成了本文所述方法的基础。我们还提供了一个quasianalytic阐述的结果rectlinearization的条款和可定义的功能，从我们以前的研究。它将被用来证明一个准解析结构对应的Denjoy-Carleman类，不像经典的分析结构，不承认量词消除语言的限制准解析函数增加的倒数函数。更准确地说，我们构造了一条平面可定义曲线，这表明J. Denef和L. van den Dries和Jasojasiewicz的定理，即每一条次解析曲线都是半解析的，对于拟解析结构不再成立。除了直线性化的条款，我们的建设利用一些定理的权力替代Denjoy-Carleman类和拟解析函数芽的非可拓性。最后一个结果依赖于（LF）-空间的Grothendieck因子分解定理和开映射定理.最后请注意，这篇论文包含了我们在2012年5月关于这个主题的早期预印本。
On logical characterization of henselianity
本文给出了Macintyre语言中允许量词消去的值域是Henselian的充分条件。然后，在没有额外的假设，我们证明了，如果一个值域的特征$(0,0)$有一个$\Z$-组作为其值组，并承认量词消除的Denef-Pas风格的语言$\mathcal{L}_{RRP}$的主排序，那么它是亨氏。事实上，这一证明表明，相当大的一类Denef-Pas风格的语言是自然的henselianity。
Let $X \subset \mathbb{P}^{n}$ be a non-empty closed subscheme over an algebraically closed field $k$, and $\mathrm{J}^{[p]}(X) = \mathrm{J}(X,\mathrm{J}(X,\cdots,\mathrm{J}(X,X)\cdots)$ denote the $p$-fold iterated join of $X$ with itself. In this article, we prove that the restriction homomorphism on cohomology $\mathrm{H}^{i}(\mathbb{P}^{N}) \rightarrow \mathrm{H}^{i}(\mathrm{J}^{[p]}(X))$, with $N = (p+1)(n+1)-1$, is an isomorphism for $0 \leq i < p$, and injective for $i=p$, for any good cohomology theory. We also prove this result in the more general setting of relative joins for $X$ ove…
We introduce a formal logical language, called conditional probability logic (CPL), which extends first-order logic and which can express probabilities, conditional probabilities and which can compare conditional probabilities. Intuitively speaking, although formal details are different, CPL can express the same kind of statements as some languages which have been considered in the artificial intelligence community. We also consider a way of making precise the notion of lifted Bayesian network, where this notion is a type of (lifted) probabilistic graphical model used in machine learning, data…
We generalize Cooper's method of quantifier elimination for classical Presburger arithmetic to give a new proof that all parametric Presburger families (as defined by Kevin Woods) are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f(t) for every polynomial f over the integers. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic with multiplication by scalars from any ring of functions into Z.
A Model Theoretic Perspective on Matrix Rings
本文从模型论角度研究矩阵环，给出量词消去的充要条件，并揭示其与同步共轭问题及不可判定性的关联。
Model theory of valued fields with an endomorphism
本文基于Dor和Halevi的工作，为残特征为零且带非满射自同态的赋值域建立了相对量词消去，并推导出正特征可分闭赋值域上Frobenius作用极限的相对量词消去。
A Model Companion for Abelian Lattice-Ordered Groups with a Valuation
本文引入了两种多排序的阿贝尔格架扩展，通过零集映射展示其等价于赋予格架的谱子空间，并利用经典部分消除量词的结果证明其中一个扩展具有模型伴侣。
We consider an expansion of Presburger arithmetic which allows multiplication by $k$ parameters $t_1,\ldots,t_k$. A formula in this language defines a parametric set $S_\mathbf{t} \subseteq \mathbb{Z}^{d}$ as $\mathbf{t}$ varies in $\mathbb{Z}^k$, and we examine the counting function $|S_\mathbf{t}|$ as a function of $\mathbf{t}$. For a single parameter, it is known that $|S_t|$ can be expressed as an eventual quasi-polynomial (there is a period $m$ such that, for sufficiently large $t$, the function is polynomial on each of the residue classes mod $m$). We show that such a nice expression is …
We study the model theory of the ring of adeles of a number field. We obtain quantifier elimination results in the language of rings and some enrichments. We given consequences for definable subsets of the adeles, and their measures.
The theory ACFA admits a primitive recursive quantifier elimination procedure. It is therefore primitive recursively decidable.
We investigate existentially closed models (of a quite arbitrary theory) equipped which an action of a fixed group G. We embed these structures in a monster model D of some well-rounded theory and describe them as PAC substructures of D. Assuming that the class of these existentially closed models is elementary, we show that, under the assumption of having bounded models, its theory is simple and eliminates quantifiers up to some existential formulas - similar to ACFA. Moreover, it codes finite sets and allows a geometric elimination of imaginaries, but not always a weak elimination of imagina…
From Saturated Embedding Tests to Explicit Algorithms
本文研究如何将证明挖掘方法改造后应用于模型论嵌入检验，从而从非构造性证明中提取显式算法，并以带指定小子群的代数闭域与实闭域理论为例给出具体算法。
We prove some results about the model theory of fields with a derivation of the Frobenius map, especially that the model companion of this theory is axiomatizable by axioms used by Wood in the case of the theory $\operatorname{DCF}_p$ and that it eliminates quantifiers after adding the inverse of the Frobenius map to the language. This strengthens the results from [4]. As a by-product, we get a new geometric axiomatization of this model companion. Along the way we also prove a quantifier elimination result, which holds in a much more general context and we suggest a way of giving "one-dimensio…
In this paper we explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than beta-eta-equivalence, like those induced by parametricity and dinaturality. We show that the Yoneda type isomorphisms yield a rewriting over types, that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We establish some sufficient conditions under w…
We study the model theoretic structure $(\Z,+,P_r)$ where $r>1$ is an irrational number and the elements of $P_r$ are of the form $\floor{nr}$ for some $n\in\Z\setminus\{0\}$. We axiomatize of this structure and prove a quantifier elimination result. As a consequence, we get that definable subsets are not sparse unless they are finite. We also prove that there are no reducts of this structure expanding $(\Z,+)$.
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。