Rate-Distortion Theory for Deductive Sources under Closure Fidelity

TL;DR

This paper develops a rate-distortion framework for compressing deductive sources, where fidelity is measured by preserving deductive closure rather than symbol accuracy, revealing how inference structure influences compression limits.

Contribution

It introduces a novel deductive compression model, deriving explicit rate-distortion formulas that incorporate proof systems and inference constraints, bridging classical and deductive source coding.

Findings

Minimum zero-distortion rate equals core mass times conditioned entropy.

Full rate-distortion depends only on the core for certain alphabets.

Exact rate-depth-distortion characterization under inference-depth limits.

Abstract

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.