Metrics for Formal Structures, with an Application to Kripke Models and their Dynamics

TL;DR

This paper introduces a family of metrics for pointed Kripke models, exploring their topological properties and showing that common model transformations like product updates are continuous within this framework.

Contribution

It generalizes Hamming distance to semantic structures, analyzes the topological features of these metric spaces, and demonstrates the continuity of model transformations.

Findings

Spaces can be compact, totally disconnected, and Hausdorff under certain conditions.

Product updates induce continuous maps in the metric topology.

Provides a new framework for analyzing Kripke models mathematically.

Abstract

This report introduces and investigates a family of metrics on sets of pointed Kripke models. The metrics are generalizations of the Hamming distance applicable to countably infinite binary strings and, by extension, logical theories or semantic structures. We first study the topological properties of the resulting metric spaces. A key result provides sufficient conditions for spaces having the Stone property, i.e., being compact, totally disconnected and Hausdorff. Second, we turn to mappings, where it is shown that a widely used type of model transformations, product updates, give rise to continuous maps in the induced topology.