The relationship between classical and constructive logics has long been illuminated by a series of conservation results, beginning with Kolmogorov’s negative translation and Glivenko’s double negation theorem, and later extended by Kuroda and Segerberg to first-order and minimal logics respectively. These results reveal how certain classical principles can be interpreted or recovered within weaker constructive frameworks, either via translations or through minimal extensions that satisfy specific logical properties. In this paper, we propose a unifying generalisation of these conservation theorems, that consolidates and expands the abstract methods introduced in earlier studies, offering a unified perspective on the interplay between classical provability and constructive reasoning.

Abstract In this paper, we introduce a general-purpose model to categorize, quantify and analyse the impact of public interest communication on target audiences. The model maps the central elements of a communication campaign such as the information flow it generates and the interaction with the beliefs, values and expectations of its target audiences. Since communication campaigns are based on arguments, we leverage on formal argumentation to specify its main ingredients and to understand the multifaceted ways a campaign can impact the beliefs of a target audience. As its main contribution, this work introduces a novel quantitative framework for value-based argumentation, in line with mainstream theories of human values, where vectors are employed to represent a multi-dimensional spectrum of values influencing audience perception and response.

Abstract A terminating sequent calculus for intuitionistic propositional logic is obtained by modifying the R $\supset $ rule of the labelled sequent calculus $\mathbf {G3I}$ . This is done by adding a variant of the principle of a fortiori in the left-hand side of the premiss of the rule. In the resulting calculus, called ${\mathbf {G3I}}_{\mathbf {t}}$ , derivability of any given sequent is directly decidable by root-first proof search, without any extra device such as loop-checking. In the negative case, the failed proof search gives a finite countermodel to the sequent on a reflexive, transitive, and Noetherian Kripke frame. As a byproduct, a direct proof of faithfulness of the embedding of intuitionistic logic into Grzegorcyk logic is obtained.