Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Structural focalization

Robert J. Simmons

TL;DR

A focused sequent calculus for propositional intuitionistic logic is presented and the proof of identity expansion, which establishes internal completeness, is a major contribution of this work.

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.

Structural focalization

TL;DR

A focused sequent calculus for propositional intuitionistic logic is presented and the proof of identity expansion, which establishes internal completeness, is a major contribution of this work.

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.

Paper Structure

This paper contains 22 sections, 8 theorems, 81 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Outline
  3. Polarized logic
  4. Sequent calculus
  5. Suspended propositions
  6. Erasure and focalization
  7. Proof terms
  8. De-focalization
  9. Cut admissibility
  10. Identity expansion
  11. Focalization
  12. Unfocused admissibility
  13. Initial rules
  14. Disjunction
  15. Positive conjunction
  16. ...and 7 more sections

Key Result

Theorem 1

If ${\Gamma}; {L} \vdash {U}$, then ${(\Gamma)^\circledast; (L)^\circledast} \longrightarrow {(U)^\circledast} \mathstrut$

Figures (9)

  • Figure 1: Sequent calculus for intuitionistic logic.
  • Figure 2: Theorems and their dependencies.
  • Figure 3: Erasure of polarized propositions.
  • Figure 4: Focused sequent calculus for polarized intuitionistic logic (sans suspended propositions).
  • Figure 5: Focused sequent calculus, extended with suspended propositions
  • ...and 4 more figures

Theorems & Definitions (15)

  • Theorem 1: De-focalization
  • proof
  • Theorem 2: Cut admissibility
  • proof
  • Theorem 3: Identity expansion
  • proof
  • Lemma 1: Shift removal (positive)
  • Lemma 2: Shift removal (negative)
  • proof
  • Theorem 4: Focalization
  • ...and 5 more