= Theory of a free bijection
{title2=$T_{\mathbb Z}$}
= Free-bijection theory
{synonym}
The <first-order theory> of a <bijection> $f$ with named inverse $g$ and no finite cycles has <first-order models> consisting of disjoint <integer> orbits. Atomic <logical formulas> reduce to $x_j=f^k(x_i)$ for <integer> $k$. An existential <logical variable> is either fixed by such a <logical equality> or must avoid finitely many points. This proves <quantifier elimination> and completeness. There is one <complete one-type>; the <complete two-types> are the <integer> offsets and the nonprincipal different-orbit <partial type>. There are countably many finite-arity <partial types> but <countable> <first-order models> with different numbers of orbits are not <isomorphic>.
Back to article page
