97-05: On linear ordering finitely-branching graphs and non-well-founded sets

DIMACS TR: 97-05

On linear ordering finitely-branching graphs and non-well-founded sets

Authors: Alexei Lisitsa and Vladimir Sazonov

ABSTRACT
Definability of a linear order in finite structures of some given class by logical means is an important issue of finite model theory and descriptive complexity theory. For example, first-order logic extended by least fixed point operator (FO+LFP) describes exactly PTIME-computability over finite linear ordered structures \cite{Imm82,Var82,Imm86}. If the structures considered are not linearly ordered in advance, but some order may be uniformly definable in FO+LFP then the same result holds for this class of structures, as well.

We will show in this paper that this is the case for the class of finite strongly extensional (SE) graphs (i.e. arbitrary graphs considered up to bisimulation equivalence relation). The vertices of such graphs serve as a faithful representation of hereditarily-finite non-well-founded sets HFA (with finite transitive closure). Actually, we define in FO+IFP a linear ordering on arbitrary SE finitely branching graphs which may be infinite and so represent a more general class of hereditarily-finite non-well-founded sets HFA^{\infty} (with infinite transitive closure).

Our interest to these questions arose from our work on characterizing the complexity classes of computable set-theoretic operations by some bounded set-theory (BST) languages \cite{Saz87,Saz93,Saz95,SaLi95, LiSa97}. So, definability in the language $\Delta_{D}$ considered in \cite{Saz95} over HFA-sets was characterised in terms of definablity in FO+LFP over finite graphs of the abovementioned kind.

Now, having definable linear ordering, we answer affirmatively the question in op. cit. on coincidence of $\Delta_{D}$-definability with PTIME-computability over HFA.

We propose two different definitions of linear ordering, one of which is an application of the method of A.Dawar, S.Lindell and S.Weinstein to the case of SE graphs and give a comparison of both approaches in terms of coherence of the orders on different graphs.

-------------------

Both authors from Program Systems Institute of Russian Acad. of Sci., Pereslavl-Zalessky, 152140, Russia.

e-mail: sazonov@logic.botik.ru lisitsa@logic.botik.ru

phones: +7-08535-98945 and 98942, fax: +7-08535-20566.

Supported by RBRF (project 96-01-01717).

The work on this paper was started when the second author visited Princeton and Rutgers Universities (DIMACS) in 1996.

Paper Available at: ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1997/97-05.ps.gz

DIMACS Home Page