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 inference-depth budget (a bounded number of iterations of the immediate-consequence operator), we obtain an exact rate-depth-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.

翻译：我们研究在固定演绎环境中生成的有限命题源的有损压缩问题。源符号为配备证明系统的知识库中的陈述，重构保真度通过演绎闭包的保持性而非符号逐位相等来度量。一旦证明系统和规范序固定，这会导致源被分解为无冗余核心与冗余存储推论。在零失真重构集满足自然不交条件时，我们证明最小零失真率等于核心源质量乘以该核心条件下源的熵。当重构字母表包含于源知识库的演绎闭包时，进一步证明完整的率失真函数仅依赖于核心，即冗余状态在率与失真两方面均不可见。当译码器受限于有界推理深度预算（即对直接推论算子的有界迭代次数）时，我们得到精确的率-深度-失真刻画。在附加序鲁棒性假设（将所选核心等同于无序本质集）下，该刻画在经典逐符号压缩与无约束演绎压缩之间建立插值关系。这些结果将演绎压缩形式化为结构化源编码问题，并量化了共享推理结构如何改变通信的基本极限。