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.

翻译：我们研究了在固定演绎环境中有限语句信源的有损压缩问题。信源符号是配备证明系统的知识库中的语句，重建保真度由演绎闭包的保持性而非符号级等价性来度量。一旦证明系统与规范序固定，这将诱导信源分解为无冗余核心与冗余存储推论两部分。在零失真重建集合满足自然不相交性条件下，我们证明了最小零失真率等于核心信源质量乘以该核心条件下信源的熵。对于包含于信源知识库演绎闭包内的重建字母表，我们进一步证明完整率失真函数仅取决于核心，因此冗余状态对率与失真均不可见。当解码器推理步数受限时，我们获得了精确的固定深度率-延迟-失真刻画。在附加序鲁棒性假设（将所选核心等同于无序本质集）下，该刻画在经典符号级压缩与无约束演绎压缩之间实现了插值。这些结果将演绎压缩形式化为结构化信源编码问题，并量化了共享推理结构如何改变通信的基本极限。