On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems

TL;DR

This paper presents a method to derive nested calculi from labelled calculi for propositional and first-order intuitionistic logic, linking semantic systems with formal proof systems and preserving proof-theoretic properties.

Contribution

It introduces a systematic approach to extract nested calculi from labelled calculi for intuitionistic logics, enhancing the connection between semantic and proof-theoretic frameworks.

Findings

Nested calculi inherit proof-theoretic properties from labelled calculi

Extraction process involves elimination of structural rules

Method applies to propositional and first-order intuitionistic logic

Abstract

This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated labelled calculus.