Title：Orbit-finite Sets

Speaker：Mikołaj Bojańczyk (Institute of Informatics, University of Warsaw)

Time: 2024/10/22 15:10-18:00

Location: Room 206, Building of Geometry (地学楼), Peking University

Abstract：

I will describe a notion of finiteness, which is called orbit-finiteness. This notion makes sense in the presence of atoms (also known as ur-elements). The idea is that a set is orbit-finite if it has finitely many elements, up to permutations of atoms. For example, the set of all atoms is orbit-finite, because it has only one element up to permutations of atoms. Another example is the set of pairs of atoms, which as two kinds of elements: non-equal pairs, and equal pairs. In this talk, I will describe the theory of orbit-finite sets, with an emphasis on decidability and algorithms.