Shininess, strong politeness, and unicorns

TL;DR

This paper refines the understanding of theory combination properties by proving that shiny theories are decidable and always strongly polite, while also identifying strongly polite theories that are not shiny, thus completing the classification of these properties.

Contribution

It establishes the decidability of shiny theories, shows their equivalence to strongly polite theories, and demonstrates the existence of strongly polite but non-shiny theories, completing the classification of theory combination properties.

Findings

Shiny theories are always decidable.

Decidable theories are strongly polite.

Existence of strongly polite theories that are not shiny.

Abstract

Shininess and strong politeness are properties related to theory combination procedures. In a paper titled "Many-sorted equivalence of shiny and strongly polite theories", Casal and Rasga proved that for decidable theories, these properties are equivalent. We refine their result by showing that: (i) shiny theories are always decidable, and therefore strongly polite; and (ii) there are (undecidable) strongly polite theories that are not shiny. This line of research is tightly related to a recent series of papers that have sought to classify all the relations between theory combination properties. We finally complete this project, resolving all of the remaining problems that were previously left open.