Structural focalization

TL;DR

This paper introduces a concise focused sequent calculus for propositional intuitionistic logic, proving the focalization property and establishing internal soundness and completeness with a novel identity expansion proof.

Contribution

It presents a new, streamlined proof of focalization for intuitionistic logic, emphasizing internal completeness through a novel identity expansion argument.

Findings

Focalization property is established for propositional intuitionistic logic.

The proof relies on structural induction, avoiding complex invertibility lemmas.

Internal soundness and completeness are verified, with a novel identity expansion proof.

Abstract

Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic, defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and grouping sequences of non-invertible rules. A focused sequent calculus is defined relative to some non-focused sequent calculus; focalization is the property that every non-focused derivation can be transformed into a focused derivation. In this paper, we present a focused sequent calculus for propositional intuitionistic logic and prove the focalization property relative to a standard presentation of propositional intuitionistic logic. Compared to existing approaches, the proof is quite concise, depending only on the internal soundness and completeness of the focused logic. In turn, both of these properties can be established (and mechanically verified) by structural induction in the style of Pfenning's structural cut elimination without the need for any tedious and repetitious invertibility lemmas. The proof of cut admissibility for the focused system, which establishes internal soundness, is not particularly novel. The proof of identity expansion, which establishes internal completeness, is a major contribution of this work.