Orbit-finite dimensional vector spaces, and orbit-finite systems of linear equations

Here is some naive questions that came to one’s mind when considering vector spaces where the dimension is not finite but orbit-finite: under a reasonable assumption on atoms , say -categoricity,

— is it true that every vector subspace of an orbit-finite dimensional vector space is orbit-finite dimensional?

— is it true that the set of solutions of an orbit-finite  system of linear equations is orbit-finite dimensional?

Continue reading

Fraisse and Completeness from Baire Categoricity

In this post, we present the proofs of the following two theorems, using Baire’s categoricity theorem.

Theorem (Fraisse, 1954). Let be a countable class of relational structures over a finite relational signature, which is closed under induced substructures and under amalgamation. Then there is a homogeneous structure with age .

We note that this is not the most general version of the theorem.

Theorem (Completeness; Godel, 1929). Let be a theory such that . Then has a countable model.

The standard proofs of these theorems involve some sort of constructions which proceed in stages, in each stage satisfying some requests which appeared in the previous stages. The proofs presented below rely on the following.

Theorem (Categoricity; Baire, 1899). Let be a complete metric space, and let be a family of open and dense subsets of . Then is dense in .

The first proof of Godel’s completeness theorem using Baire’s categoricity theorem appeared in Mathematics of Metamathematics (1963) by Helena Rasiowa (my great-great-phd-grand-mother) and Roman Sikorski. I don’t know who was the first to prove Fraisse’s result using Baire’s categoricity; definitely it is not new in this post (see e.g.  W. Kubiś, Fraisse sequences: category-theoretic approach to universal homogeneous structures). Other applications of Baire’s categoricity theorem in logic include the Omitting Type’s theorem and Forcing.

Continue reading

Least supports and weak elimination of imaginaries

We show that a property known from model theory as weak elimination of imaginaries corresponds to the property of admitting least algebraically closed supports, and is a generalization of admitting least supports in many contexts. In particular, we show that an ω-categorical structure admits least supports if and only if it has no algebraicity and has weak elimination of imaginaries.

Continue reading

The Rado graph admits only one oligomorphic action of its automorphism group

Let denote the Rado graph and its automorphism group. We show that any action of  on  by automorphisms which has finitely many orbits is isomorphic to the natural action. Therefore, in a sense, every interpretation of the Rado graph in itself without parameters is trivial. The proof uses a counting argument. As a corollary, every interpretation of the Rado graph in itself without parameters is definably isomorphic or anti-isomorphic to the Rado graph. Also, there is no interpretation of – the Rado graph with a constant – in which does not use parameters.

Continue reading

Least supports and non-interpretability

In this post, we give a proof that does not interpret (without parameters) in the homogeneous poset nor in the random graph . The idea is to first show that every continuous action of  or on a set is faithful or trivial. We show this by using the fact that and  have least supports. Since and have an automorphism of order two and does not, this proves that there is no nontrivial continuous action of nor on .

Continue reading

Automorphism groups of definable structures

We consider equality atoms , i.e., is a countable set with the equality relation. Recall that by definable set we mean a structure which can be defined (in a possibly nested fashion) from using finite unions, finite tuples, and set-builder expressions with first-order formulas ranging over , e.g. is definable using the parameter . A definable relational structure is a relational structure  where and each relation is a definable set. Up to isomorphism, definable structures are the same as structures which interpret in , using first-order interpretations (this correspondence preserves parameters), but sometimes using definable sets makes constructions easier.

The problem described in the previous post is to determine isomorphism between two definable structures. In this post, we describe this problem in terms of automorphism groups. This post is based on discussions with Manuel Bodirsky and Antoine Mottet.

Continue reading

Graph isomorphism

Fix an -categorical structure . The simplest, and already interesting case is , the pure countable set.

We consider the definable graph isomorphism problem for graphs which are definable (equivalently, interpret in) :

Problem: DefGraphIso

Input: Two definable graphs

Output: Yes, if and are isomorphic, No otherwise.

Below we make some very basic observations concerning this problem.

Continue reading

System of equations over sets of integers

Consider system of equations of the form

where variables are interpreted as sets of integers, and are expressions built from variables , constants sets , addition (interpreted element-wise as , union ,  and a restricted form of intersection. Namely, we allow expressions of the form  with and expression and a constant denoting a semilinear subset of .

(The study of such systems of equations stems from the analysis of pushdown automata over timed atoms [1], where equations in the form above are used to represent the delays of the timestamps of stack symbols between the time of push and the time of the corresponding pop.)

A solution is an assignment of a subset of integers to each variable . We are interested in the emptiness problem: is empty in the least solution of a given system of equations as above? For example, natural numbers are the least solution to and even integers are the least solution to . Finite sets of constants like can be succinctly expressed by small equations using their binary expansion.

Note that the use of intersection in  is severely restricted. If intersections of the form for two variables are allowed, then the emptiness problem is equivalent to the emptiness problem of conjunctive grammars, and the latter problem is undecidable  [2].

On the other hand, emptiness is in PTIME if no intersection is allowed: By interpreting the commutative as the noncommutative language concatenation  (which preserves emptiness in the absence of intersections), we reduce to a context-free grammar—whose emptiness problem is solvable in PTIME.

Not all decision problems need be computationally simple, even in the absence of intersections. The -membership problem, which asks whether  (i.e., a word with the same number of ‘s and ‘s in the noncommutative view) is in the least solution, is NP-complete. This is an interesting example where parsing is harder than emptiness—it is usually the other way around, e.g., for conjunctive grammars emptiness is undecidable, while parsing is decidable (even in PTIME [2]).

Emptiness for equations where only intersections with finite are allowed, is NP-complete too. This can be shown by a simple iterative algorithm computing coarser and coarser under-approximations of the least solution, using at each step an oracle for the -membership problem for intersection-less equations.

The general case of intersections with semilinear is open. The emptiness problem in this case is equivalent to the emptiness problem for the class of timed poshdown automata [1]. We conjecture that the problem decidable in this case, and that, moreover, the least solution is semilinear.


[1] L. Clemente and S. Lasota, “Timed Pushdown Automata”, LICS’15.

[2] A. Jez and A. Okhotin, “Conjunctive grammars over a unary alphabet: Undecidability and unbounded growth,” Theory Comput. Syst., vol. 46, no. 1, pp. 27–58, 2010.