Deducibility of Identicals, Reflection Principle and Synthetic Connectives
Yuki Nishimuta
TL;DR
The paper addresses how the deducibility of identicals (DoI) condition relates to Sambin et al.'s reflection principle, proving their equivalence once the main step of cut elimination is assumed. It further shows that a connective satisfies the reflection principle if and only if it is a Girard's synthetic connective, and that solvability of associated definitional equations hinges on a singleton, non-context-changing formation rule with visibility. By reframing the reflection principle and exploring presentation dependence, the authors extend the analysis to n-ary connectives and clarify the boundary between solvable and unsolvable definitional equations. The results sharpen the understanding of when reflection-based definitions yield well-behaved connectives and illuminate the structural requirements for equivalence with DoI, with potential implications for the design of uniform logical frameworks. Overall, this work connects foundational criteria for connectives with a precise characterization of synthetic connectives in a unified setting.
Abstract
Sambin et al. (2000) introduced Basic Logic as a uniform framework for various logics. At the same time, they also introduced the principle of reflection as a criterion for being a connective in Basic Logic. In this paper, we make explicit the relationship between Hacking's deducibility of identicals condition (Hacking, 1979) and the principle of reflection by proving their equivalence. Moreover, despite Sambin et al.'s conjecture that only six connectives satisfy the principle of reflection, we show that a logical connective satisfies the principle of reflection if and only if it is Girard's synthetic connective.