Hyperformalism for Bunched Natural Deduction Systems

TL;DR

This paper explores advanced hyperformalism in bunched natural deduction systems, showing how it can capture extensive intensional content and proof structures, expanding the scope of hyperformal logic studies.

Contribution

It extends hyperformalism to encompass all intensional content in bunched natural deduction systems and includes proof structures, broadening the understanding of hyperformal logic.

Findings

Demonstrates hyperformalism in relevant logic B after modifications.

Shows hyperformalism can include proof structures, not just provability.

Expands the theoretical framework for hyperformal logic.

Abstract

Logics closed under classes of substitutions broader than class of uniform substitutions are known as hyperformal logics. This paper extends known results about hyperformal logics in two ways. First: we examine a very powerful form of hyperformalism that tracks, for bunched natural deduction systems, essentially all the intensional content that can possibly be tracked. We demonstrate that, after a few tweaks, the well-known relevant logic $\mathbf{B}$ exhibits this form of hyperformalism. Second: we demonstrate that not only can hyperformalism be extended along these lines, it can also be extended to accommodate not just what is proved in a given logic but the proofs themselves. Altogether, the paper demonstrates that the space of possibilities for the study of hyperformalism is much larger than might have been expected.