A Simple Logic of Functional Dependence

TL;DR

This paper introduces LFD, a simple decidable logic for functional dependence, extending propositional logic with dependence atoms and quantifiers, exploring its properties, extensions, and applications in various mathematical and dynamic contexts.

Contribution

It presents a new decidable logic of functional dependence with a complete proof calculus and explores its extensions and applications in diverse settings.

Findings

LFD is a decidable logic with complete proof calculus.

Extensions include undecidable modal and dynamic logics.

Applications cover topological, vector space, and temporal dependence.

Abstract

This paper presents a simple decidable logic of functional dependence LFD, based on an extension of classical propositional logic with dependence atoms plus dependence quantifiers treated as modalities, within the setting of generalized assignment semantics for first order logic. The expressive strength, complete proof calculus and meta-properties of LFD are explored. Various language extensions are presented as well, up to undecidable modal-style logics for independence and dynamic logics of changing dependence models. Finally, more concrete settings for dependence are discussed: continuous dependence in topological models, linear dependence in vector spaces, and temporal dependence in dynamical systems and games.