离散线性集成逻辑
Discrete Linear Ensemble Logic
浏览论文内容
中文总结 AI 辅助
针对生物医学知识统一符号层需求，研究自然数上离散集成逻辑$\text{EL}(\text{Nat})$，给出语法语义、嵌入结果、复杂度与表达力结论，并提出相对完备的$\text{HEL}$证明系统。
中文摘要 AI 辅助
我们研究了自然数集上集成逻辑$\boldsymbol{\text{Ensemble Logic}}$（$\text{EL}(\text{Nat})$）的基于离散点的片段，该逻辑结合了位移算子$\boldsymbol{\text{φ}_u}$、带加性界的有界度量模态词$\boldsymbol{\boldBox_t}$与$\boldsymbol{\text{mdiamond}_t}$、布尔连接词以及自然数集上的一阶量化。受构建具备时间、空间、基因组及多模态度量内容的生物医学知识统一符号层的需求驱动，我们建立了该形式体系的离散基础理论。我们给出了其语法与语义，并证明了有限命题集$\boldsymbol{\text{mathcal{P}}}$上的$\text{EL}(\text{Nat})$可向前嵌入一阶一元$\boldsymbol{\text{Presburger}}$算术$\text{FO}(\text{Nat},<,+;\text{mathcal{P}})$。该嵌入给出了解析上界，而通过对带循环控制状态的非确定性两计数器机器的归约，证明了其可满足性问题为$\boldsymbol{\text{Σ}^1_1}$完全的，有效性问题则对偶为$\boldsymbol{\text{Π}^1_1}$完全的。在表达能力方面，$\text{EL}(\text{Nat})$严格扩展了无星$\boldsymbol{\text{ω}}$语言，且与$\boldsymbol{\text{ω}}$正则语言不可比：它可定义非$\text{ω}$正则的计数语言$\boldsymbol{\text{\textbraceleft}a^mb^mc^md^m\boldsymbol{\text{mid}} m\boldsymbol{\text{≥}} 1\text{\textbraceright}·\text{Σ}^ω}$，而根据经典$\text{Presburger}$算术下界，一种有界奇偶语言不在该逻辑的表达范围内。在证明论层面，我们提出了一个可靠的$\boldsymbol{\text{Hilbert}}$系统$\text{HEL}$，并证明了其相对于以一元$\text{Presburger}$有效性为神谕的完备性，同时指出相对于普通$\text{Presburger}$算术的完备性是不可能实现的。
英文摘要
We study the discrete point-based fragment of Ensemble Logic $\EL(\Nat)$ over the natural numbers, a logic combining displacement $φ_u$, bounded metric modalities $\boldBox_t$ and $\mdiamond_t$ with additive bounds, Boolean connectives, and first-order quantification over $\Nat$. Motivated by the need for a unified symbolic layer for biomedical knowledge with temporal, spatial, genomic, and multimodal metric content, we develop the foundational discrete theory of the formalism. We give syntax and semantics, and prove a forward embedding of $\EL(\Nat)$ over a finite proposition set $\mathcal{P}$ into first-order monadic Presburger arithmetic $\FO(\Nat,<,+;\mathcal{P})$. This embedding yields the analytical upper bounds, while a reduction from nondeterministic two-counter machines with recurring control states proves that satisfiability is $Σ^1_1$-complete and validity is dually $Π^1_1$-complete. Expressively, $\EL(\Nat)$ strictly extends the star-free $ω$-languages and is incomparable with the $ω$-regular languages: it defines the non-$ω$-regular counting language $\{a^mb^mc^md^m\mid m\geq 1\}\cdotΣ^ω$, whereas a delimited parity language remains outside the logic by classical Presburger-arithmetic lower bounds. On the proof-theoretic side, we present a sound Hilbert system $\HEL$ and establish completeness relative to monadic Presburger validity as oracle, noting that completeness relative to plain Presburger arithmetic is impossible.
