We show that the expressive power of order-invariant first-order logic collapses to first-order logic over hollow trees. A hollow tree is an unranked ordered tree where every non leaf node has at most four adjacent nodes: two siblings (left and right) and its first and last children. In particular there is no predicate for the linear order among siblings nor for the descendant relation. Moreover only the first and last nodes of a siblinghood are linked to their parent node, and the parent-child relation cannot be completely reconstructed in first-order.
@InProceedings{grange_et_al:LIPIcs.CSL.2020.23, author = {Grange, Julien and Segoufin, Luc}, title = {{Order-Invariant First-Order Logic over Hollow Trees}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.23}, URN = {urn:nbn:de:0030-drops-116661}, doi = {10.4230/LIPIcs.CSL.2020.23}, annote = {Keywords: order-invariance, first-order logic} }
Feedback for Dagstuhl Publishing