In the setting of model checking, the concept of symmetry reduction is quite straightforward; to obtain a reduced model, we can put symmetric states together. However, there are several nuances that have to be spelled out. Which structures are used to define our model? What is a state? And what precisely is a symmetry? The latter is the main topic of this talk. We work towards a definition of symmetry for predicate formulas, that is built up using some notions in group theory. Also, we briefly show how we can extend this definition of symmetries for predicate formulas to the theory of PBESs and their solutions.