Deducibility of Identicals, Reflection Principle and Synthetic Connectives
Yuki Nishimuta

TL;DR
This paper explores the relationship between Hacking's deducibility of identicals and the reflection principle in Basic Logic, proving their equivalence and characterizing connectives satisfying reflection as Girard's synthetic connectives.
Contribution
It explicitly establishes the equivalence between deducibility of identicals and the reflection principle, and characterizes all connectives satisfying reflection as Girard's synthetic connectives.
Findings
Proves the equivalence of Hacking's deducibility of identicals and the reflection principle.
Shows that connectives satisfying reflection are exactly Girard's synthetic connectives.
Refutes the conjecture that only six connectives satisfy the reflection principle.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
