Uniform Definability in Propositional Dependence Logic

TL;DR

This paper investigates the expressive capabilities of propositional dependence logic, demonstrating that certain intuitionistic connectives, while translatable, are not uniformly definable within it, highlighting limits of its expressive power.

Contribution

It proves that intuitionistic disjunction and implication are not uniformly definable in propositional dependence logic despite existing translations.

Findings

Non-compositional translations exist for certain intuitionistic connectives.

Intuitionistic disjunction and implication are not uniformly definable.

Propositional dependence logic has expressive limitations.

Abstract

Both propositional dependence logic and inquisitive logic are expressively complete. As a consequence, every formula with intuitionistic disjunction or intuitionistic implication can be translated equivalently into a formula in the language of propositional dependence logic without these two connectives. We show that although such a (non-compositional) translation exists, neither intuitionistic disjunction nor intuitionistic implication is uniformly definable in propositional dependence logic.