正有界逻辑中抽象空间的逻辑元定理II：度量空间与模型论一致性原理
Logical Metatheorems for Abstract Spaces axiomatized in Positive Bounded Logic II: Metric spaces and the model-theoretic uniformity principle
浏览论文内容
中文总结 AI 辅助
该研究将正有界逻辑中赋范结构的统一界提取证明论处理扩展到抽象度量结构，为特定\(\forall\exists\)语句建立提取定理，解释了相关非标准证明中提取统一界成功的原因，并为群稳定子集结构定理提供新显式界。
中文摘要 AI 辅助
我们将在正有界逻辑中对赋范结构（如为巴拿赫空间模型理论所发展的那样）进行的从范数结构中统一界提取的证明论处理扩展到抽象度量结构的更一般情形，包括视为经典一阶模型的离散结构。特别地，我们为广义框架建立了统一界提取定理，该框架针对矩阵为正有界逻辑中公式（嵌入）之否定的\(\forall\exists\)语句，其证明使用饱和性。这样，我们为[《数学进展》，343:567 - 623, 2019]中从非标准证明中提取统一界的成功提供了形式解释，其非正式地遵循了单调函数解释的观点。作为我们所发展的形式框架的一个应用，我们为[《剑桥哲学学会数学学报》，168(2):405 - 413, 2020]中给出的群的稳定子集的一个结构定理提供了新的显式界。
英文摘要
We extend the proof-theoretic treatment of uniform bound extraction from normed structures axiomatized in positive bounded logic [Advances in Mathematics, 290:503-551, 2016] (as developed for the model theory of Banach spaces) to the more general setting of abstract metric structures, including discrete structures viewed as classical first-order models. In particular, we establish uniform bound extraction theorems for our generalized framework for $\forall\exists$-sentences whose matrix is the negation of (an embedding of) a formula in positive bounded logic, whose proofs use saturation. In this way, we provide a formal explanation for the successes in the extraction of uniform bounds from nonstandard proofs given in [Advances in Mathematics, 343:567-623, 2019], which had informally followed the perspective of the monotone functional interpretation. As an application of the formal framework we develop, we provide novel explicit bounds for a structural theorem for stable subsets of groups given in [Mathematical Proceedings of the Cambridge Philosophical Society, 168(2):405-413, 2020].
