A modal approach towards substitutions

TL;DR

This paper develops a logical framework to model both single-step and iterative substitutions, analyzing their properties, proof systems, and relationships with existing frameworks, with applications in social opinion dynamics, computation, and game theory.

Contribution

It introduces a novel modal approach that unifies the treatment of single-step and iterative substitutions, providing new insights into their logical properties and connections to existing systems.

Findings

The framework accurately models both types of substitutions.

It establishes formal properties and proof systems for the proposed logic.

Connections to classical and existing iterative substitution frameworks are clarified.

Abstract

Substitutions play a crucial role in a wide range of contexts, from analyzing the dynamics of social opinions and conducting mathematical computations to engaging in game-theoretical analysis. For many situations, considering one-step substitutions is often adequate. Yet, for more complex cases, iterative substitutions become indispensable. In this article, our primary focus is to study logical frameworks that model both single-step and iterative substitutions. We explore a number of properties of these logics, including their expressive strength, Hilbert-style proof systems, and satisfiability problems. Additionally, we establish connections between our proposed frameworks and relevant existing ones in the literature. For instance, we precisely delineate the relationship between single-step substitutions and the standard syntactic replacements commonly found in many classical logics. Moreover, special emphasis is placed on iterative substitutions. In this context, we compare our proposed framework with existing ones involving iterative reasoning, thereby highlighting the advantages of our proposal.