Expressive completeness failure in branching time structures

摘要

A propositional logic is expressively complete if there is a finite set of connectives which define all truth tables. Kamp, Stavi, and Gabbay proved that all tense logics over linear time are expressively complete. Amir and Gabbay brought examples of expressively complete non-linear time structures. Gabbay showed that the general time structure is not expressively complete. Here we narrow the gap and prove that for branching time, if the model is an infinite tree with an unbounded branching factor then there is no expressive completeness.