Harmony in the Light of Computational Ludics

TL;DR

This paper reformulates the inversion and recovery principles in proof-theoretic semantics within the Computational Ludics framework into a unified harmony condition, revealing their underlying intuitive ideas and equivalences.

Contribution

It introduces a unified harmony condition in Computational Ludics that combines the inversion and recovery principles, clarifying their conceptual relationship.

Findings

Reformulation of principles into a single harmony condition

Identification of containment and converse ideas behind principles

Equivalence of additional conditions to the harmony condition

Abstract

Prawitz formulated the so-called inversion principle as one of the characteristic features of Gentzen's intuitionistic natural deduction. In the literature on proof-theoretic semantics, this principle is often coupled with another that is called the recovery principle. By adopting the Computational Ludics framework, we reformulate these principles into one and the same condition, which we call the harmony condition. We show that this reformulation allows us to reveal two intuitive ideas standing behind these principles: the idea of "containment" present in the inversion principle, and the idea that the recovery principle is the "converse" of the inversion principle. We also formulate two other conditions in the Computational Ludics framework, and we show that each of them is equivalent to the harmony condition.