From Focalization of Logic to the Logic of Focalization

AbstractAndreoli originally discovered focalization as a concrete proof search strategy in proof theory of linear logic, putting to the foreground the role of polarity in logic.The aim of the present paper is to give a more abstract account on focalization in the framework of ludics. We describe focalization as a map (embodied by an untyped proof/design) from an unsynthesized to a synthesized type/behaviour. The map turns out to be a retraction of another map, that is related to invertibility of negative connectives. In this way we formalize the common intuition that focalization of positive connectives is dual to invertibility of negative ones