A Propositional Metric Logic with Fixed Finite Ranges

Abstract

The aim of this article is developing a formal system suitable for reasoning about the distance between propositional formulas. We introduce and study a formal language which is the extension of the classical propositional language obtained by adding new binary operators D≤s and D≥s, s Range, where Range is a fixed finite set. In our language it is allowed to make formulas of the form D≤s(α β) with the intended meaning 'distance between formulas α and β is less than or equal to s'. The semantics of the proposed language consists of possible worlds with a distance function defined between sets of worlds.