PARADOXICAL CONNECTIVES: PROOF-THEORETIC SEMANTICS, RECURSION, AND FIXED-POINT OPERATORS

Abstract This paper analyses some connectives introduced by Stephen Read, known as ‘Bullet connectives’. From the proof-theoretic semantics perspective, these connectives satisfy the requirement of harmony; however, they allow for the looping derivation of a contradiction. Namely, when the operation of detour reduction is applied to such a derivation, it leads to a non-terminating phenomenon. By appealing to Prawtiz’s notion of validity, we argue that such connectives cannot be considered as logical ones. Still, it is possible to assign a computational meaning to such connectives, as several useful computation properties are induced by their harmonious behaviour. In particular, we show that a fixed point operator can be defined by using the rules of a generalised version of the Bullet connectives. Such a generalisation is an instance of (non-terminating) recursive types. Finally, we show that type-free (i.e., untyped) lambda-calculus is interpretable in simply typed lambda-calculus extended with yet another variant of the Bullet connectives, and that the introduction rules of the Bullet connectives are interpretable by Nakano’s modality in typed lambda-calculus. We conclude that such a computational interpretation of the Bullet connectives is possible only if we separate the notion of types from that of propositions, which are meaningful and assertible linguistic entities (in fact, it is larger). Therefore, the computational interpretation we propose cannot be considered an instance of the Curry–Howard correspondence between propositions and types, and between proofs and programs.