We study lossy compression of a finite statement source generated in a fixed deductive environment. The source symbols are statements in a knowledge base endowed with a proof system, and reconstruction fidelity is measured by preservation of deductive closure rather than by symbolwise equality. This induces, once the proof system and canonical order are fixed, a decomposition of the source into an irredundant core and redundant stored consequences. Under a natural disjointness condition on zero-distortion reconstruction sets, we show that the minimum zero-distortion rate equals the source mass of the core times the entropy of the source conditioned on that core. For reconstruction alphabets contained in the deductive closure of the source knowledge base, we further prove that the full rate-distortion function depends only on the core, so redundant states are invisible to both rate and distortion. When the decoder is limited to a bounded number of inference steps, we obtain an exact fixed depth rate-delay-distortion characterization. Under an additional order-robustness assumption identifying the chosen core with the order-free essential set, this characterization interpolates between classical symbolwise compression and unconstrained deductive compression. These results formulate deductive compression as a structured source coding problem and quantify how shared inference structure changes the fundamental limits of communication.
翻译:我们研究在固定演绎环境中生成的有限命题信源的有损压缩。信源符号是配备证明系统的知识库中的命题,重构保真度通过演绎闭包的保持而非符号级相等来度量。在证明系统和规范次序固定后,这种度量将信源分解为无冗余核心与冗余存储推论。在零失真重构集满足自然不相交条件时,我们证明最小零失真率等于核心的信源质量乘以信源在核心条件下的熵。当重构字母表包含于信源知识库的演绎闭包时,进一步证明完整率失真函数仅依赖于核心,因此冗余状态对率与失真均不可见。当解码器推理步数受限时,我们得到精确的固定深度率-时延-失真刻画。在附加次序鲁棒性假设(将选定核心等同于无次序本质集)下,该刻画在经典符号级压缩与无约束演绎压缩之间建立插值。这些结论将演绎压缩形式化为结构化信源编码问题,并量化共享推理结构如何改变通信的基本极限。