Editing Transitive closure (section)

== In logic and computational complexity ==
The transitive closure of a binary relation cannot, in general, be expressed in [[first-order logic]] (FO).
This means that one cannot write a formula using predicate symbols ''R'' and ''T'' that will be satisfied in
any model if and only if ''T'' is the transitive closure of ''R''.
In [[finite model theory]], first-order logic (FO) extended with a transitive closure operator is usually called '''transitive closure logic''', and abbreviated FO(TC) or just TC. TC is a sub-type of [[fixpoint logic]]s. The fact that FO(TC) is strictly more expressive than FO was discovered by [[Ronald Fagin]] in 1974; the result was then rediscovered by [[Alfred Aho]] and [[Jeffrey Ullman]] in 1979, who proposed to use fixpoint logic as a [[database query language]].<ref>(Libkin 2004:vii)</ref> With more recent concepts of finite model theory, proof that FO(TC) is strictly more expressive than FO follows immediately from the fact that FO(TC) is not [[Gaifman-local]].<ref>(Libkin 2004:49)</ref>

In [[computational complexity theory]], the [[complexity class]] [[NL (complexity)|NL]] corresponds precisely to the set of logical sentences expressible in TC. This is because the transitive closure property has a close relationship with the [[NL-complete]] problem [[STCON]] for finding [[directed path]]s in a graph. Similarly, the class [[L (complexity)|L]] is first-order logic with the commutative, transitive closure. When transitive closure is added to [[second-order logic]] instead, we obtain [[PSPACE]].