Institut für Mathematik


Modul:   MAT591  Discrete mathematics

First-order logic for permutations

Vortrag von Prof. Dr. Mathilde Bouvel

Datum: 07.05.18  Zeit: 14.00 - 14.45  Raum: Y27H26

In the combinatorics literature, there are two different ways of defining a permutation (say, of size \(n\)). One is as a bijection from \(\{1,2, \cdots, n\}\) to itself, or as an element of the permutation group \(S_n\). The other is as a word containing exactly once each letter in \(\{1,2, \cdots, n\}\), or as a diagram (i.e., an \(n \times n\) grid containing one element per row and per column). Depending on the definition that is chosen, the results that are proved are usually of different nature, and these two points of view are believed to be rather opposite. The purpose of this talk is to provide mathematical evidence of this ``belief''.

For each of these points of view, we define a first-order logical theory, whose models are the permutations seen as bijections in one case, as words in the other case. We then investigate which properties of permutations are expressible in each of these theories. It is no surprise that the theory associated with permutations seen as bijections (called TOOB -- the Theory Of One Bijection) can express statements about the cycle decomposition of permutations, while the theory associated with permutations seen as words (called TOTO -- the Theory Of Two Orders) is designed to express pattern-related concepts. This can be illustrated with many examples.

But we are also interested in describing which properties are \(\textbf{not}\) expressible in each of these theories. For instance, we prove that TOTO cannot express that an element of a permutation is a fixed point, while TOOB cannot express that a permutation contains the pattern 231.

The result that we put forward in the talk is that we completely characterize the properties that are expressible in both theories. As ``expected'' based on the ``belief'' explained earlier, these properties are trivial in some sense. More precisely, such a property is either identically true on all permutations of sufficiently large support, or identically false on all permutations of sufficiently large support. In the proofs, a key tool that we use is the theory of Ehrenfeucht-Fraïssé games.

Additional results that we provide are a characterization of permutation classes where TOTO can express (unlike in the general case) some information on the cycle-types, and a proof that TOTO is more suited than excluded patterns to express sortability by stacks in the sense of West.

The talk is based on a joint work with Michael Albert and Valentin Feray.