math.LO — Logic

Intuitionistic Compression and Optimal Verification Trees

Contributed by Zhenyu Sun, Jilin Wang

In strict finitistic generation semantics, a formula is assertible at a generation if some stage in its verification tree forces it. We ask when assertibility agrees with intuitionistic truth on the poset of generations. The leaves of the verification trees, ordered by generation extension, form an intuitionistic Kripke model that preserves truth at every leaf, even without atomic prevalence. For a finite bundle, compression to the generations is exact if and only if each fiber of leaves has a greatest intuitionistic theory and the map selecting these theories has the back property. Compression remains exact under every restriction of the generation poset if and only if atomic prevalence holds. Conversely, consider coherent tree representations of a finite Kripke model whose atomic valuation reflects its order. Among representations with atomic prevalence, the minimum numbers of leaves and nodes over $u$ are $h(u)$ and $\delta_C+\sum_{x\preceq u}h(x)$, where $h(x)$ counts saturated paths from minimal worlds to $x$, and $\delta_C$ is $1$ if the comparability component of $u$ has no least element and $0$ otherwise. Saturated-path trees attain both minima simultaneously. Among representations attaining the node minimum at every world, the common root labels in components without a least element determine the representation up to isomorphism over the outer frame. Allowing rooted posets in place of trees can reduce the number of nodes exponentially.