22 November 2007, Logic Tea, Luc Segoufin

In this talk I will consider <-inv-FO, order-invariant first-order, over finite structures. <-inv-FO is the class of first-order formulas that use an extra predicate interpreted as a linear order, but such that the truthness of the formula does not depend on the choice of the linear order. Over arbitrary structures, it is a simple consequence of Craig Interpolation Theorem to show that <-inv-FO and FO have the same expressive power. Over finite structures it is possible to show that <-inv-FO express strictly more than FO. I will then show that over simple strucutres, such as words or trees, <-inv-FO=FO. To achieve this I will introduce and use an algebraic characterization of FO over trees.

The Logic Tea homepage can be found at http://www.illc.uva.nl/logic_tea/. For more information, please contact Joel Uckelmann (juckelma at science.uva.nl) or Edgar Andrade (E.J.AndradeLotero at uva.nl).