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.