一句话：证明有限图上 Łoś–Tarski 式的禁用诱导子图刻画失效，且该刻画不可计算、大小无界。
论文研究被诱导子图封闭的有限与无限图类何时可由一阶逻辑（FO）定义，及其禁用诱导子图刻画的可计算性。经典 Łoś–Tarski 定理表明，此类图类可由 FO 句子 φ 定义当且仅当它有有限个禁用有限诱导子图；由完备性定理还可从 φ 计算该刻画，并用于小顶点覆盖、有界 tree-depth/shrub-depth 等图类。作者证明该机制在有限图上失效：存在 FO 可定义且对诱导子图封闭的有限图类，却无有限禁用诱导子图集；即使图类可由有限禁用诱导子图刻画，该刻画也不能从定义它的 FO 句子计算，其规模不能由任何可计算函数 f(|φ|) 界定。结果还加强了任意结构上的类似定理。
LetCbe a class of finite and infinite graphs that is closed under induced subgraphs. The well-known Łoś-Tarski Theorem from classical model theory implies thatCis definable in first-order logic (FO) by a sentence φ if and only ifChas a finite set of forbidden induced finite subgraphs. It provides a powerful tool to show nontrivial characterizations of graphs of small vertex cover, of bounded tree-depth, of bounded shrub-depth, etc. in terms of forbidden induced finite subgraphs. Furthermore, by the Completeness Theorem, we can compute from φ the corresponding forbidden induced subgraphs. Our results (a) and (b) show that this machinery fails on finite graphs. (a)There is a class of finite graphs that is definable in FO and closed under induced subgraphs but has no finite set of forbidden induced subgraphs. (b)Even if we only consider classesCof finite graphs that can be characterized by a finite set of forbidden induced subgraphs such a characterization cannot be computed from an FO-sentence φ that definesCand the size of the characterization cannot be bounded by f(|φ|) for any computable function f.Besides their importance in graph theory, our results also significantly strengthen similar known theorems for arbitrary structures.
DOI 原文 ·
@inproceedings{paperbot6175,
title = {Forbidden Induced Subgraphs and the Łoś–Tarski Theorem},
author = {Yijia Chen and Jorg Flum},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470742}
}