Graph projections

The loop-free directed complement is a quantifier-free projection: equality of the endpoints selects false on the diagonal; otherwise the output is the negation of one input edge. The numeric interpretation is the identity, so this construction preserves any chosen relational numeric structure. It works for every universe, including the empty one, and needs neither order nor BIT. For simple graphs this is the usual graph complement. Both properties are proved by the automation of Complexity.Tactic.FirstOrder: fo_qf for quantifier-freeness and fo_simp for the edge predicate.

Main definitions

• Cslib.Logic.FO.Projection.offDiagonalComplement: complement off the diagonal, with identity numeric data.

Main results

• Cslib.Logic.FO.Projection.realize_offDiagonalComplement: the output edge predicate is inequality and nonadjacency.
• Cslib.Logic.FO.Projection.isQF_offDiagonalComplement: all numeric tests and definitions are quantifier-free.

References

• N. Immerman, Descriptive Complexity

def Cslib.Logic.FO.Projection.offDiagonalComplement (N : FirstOrder.Language) : Projection N N FirstOrder.Language.graph FirstOrder.Language.graph Unit

Complement a binary edge relation off the diagonal. Equality is a numeric test and the negative edge literal supplies the only input bit inspected by each output bit.

theorem Cslib.Logic.FO.Projection.isQF_offDiagonalComplement (N : FirstOrder.Language) : (offDiagonalComplement N).IsQF

The loop-free directed complement is quantifier-free.

theorem Cslib.Logic.FO.Projection.realize_offDiagonalComplement (N : FirstOrder.Language) {M : Type u_1} [N.Structure M] [FirstOrder.Language.graph.Structure M] (x : Fin 2 × Unit → M) : ((offDiagonalComplement N).rel FirstOrder.Language.graphRel.adj).toFormula.Realize x ↔ x (0, ()) ≠ x (1, ()) ∧ ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj fun (i : Fin 2) => x (i, ())

The output contains precisely the unequal, nonadjacent pairs. No symmetry or irreflexivity assumption is imposed on the input relation.