Compactness in sets with atoms

This is another talk about sets with atoms (also known as Fraenkel-Mostowski sets, or nominal sets). Specifically, the topic is the notion of models for formulas of first-order logic. The problem is that a natural definition of a "model" for a formula of first-order logic makes the compactness theorem fail. On a related note, although sets with atoms are a good language to talk finite objects with data (such as data words), the language seems to be less suited to modelling infinite objects. As a solution to these problems, in the talk I will propose a different definition of "model" for first-order logic, together with a sound and complete proof system, which in particular means that the compactness theorem is recovered.