Abstract
We prove that any positive elementary (least fixed point) induction expressing the negation of transitive closure on finite nondirected graphs requires at least two recursion variables.

This publication has 13 references indexed in Scilit: