Definability in the Substructure Ordering of Simple Graphs

For simple graphs, we investigate and seek to characterize the properties first-order definable by the induced subgraph relation. Let \({\mathcal{P}\mathcal{G}}\) denote the set of finite isomorphism types of simple graphs ordered by the induced subgraph relation. We prove this poset has only one non-identity automorphism co, and for each finite isomorphism type G, the set {G, G ^co } is definable. Furthermore, we show first-order definability in \({\mathcal{P}\mathcal{G}}\) captures, up to isomorphism, full second-order satisfiability among finite simple graphs. These results can be utilized to explore first-order definability in the closely associated lattice of universal classes. We show that for simple graphs, the lattice of universal classes has only one non-trivial automorphism, the set of finitely generated and finitely axiomatizable universal classes are separately definable, and each such universal subclass is definable up to the unique non-trivial automorphism.