5.4. Tuple Reachability🔗

Cslib.Logic.FO.TC.tc binds two k-tuples in its body and takes two endpoint tuples as arguments. Its semantics is Relation.ReflTransGen: a path of zero or more body edges. The zero-length path makes a tuple reachable from itself even when the body is false. Parameters stay fixed along the path. Width-zero closure is meaningful on an empty domain, because there is still one empty tuple.

Cslib.Logic.FO.TC.pair concatenates the endpoints; TC.left and TC.right recover them. The semantic API proves reflexivity, inclusion of body edges, and composition of paths. Cslib.Logic.FO.Ordered.TCDefinable.encodedLanguage_mem_NL gives the easy half of Immerman's capture theorem: on canonically ordered structures, every query defined by one FO(TC) sentence lies in native NL. The converse, Cslib.Logic.FO.Ordered.PosTCDefinable.of_encodedLanguage_mem_NL, defines every native NL query by one sentence with a single positive closure, so Cslib.Logic.FO.Ordered.tcDefinable_iff_encodedLanguage_mem_NL states FO(TC) = NL.

Cslib.Logic.FO.Ordered.FullTupleInterpretation.onTCSentence transports FO(TC) sentences along a full-tuple interpretation, as onLFPSentence does for FO(LFP). A closure over pairs of width-w target tuples becomes one over pairs of width-w * k source tuples. Each closure keeps its polarity, so positive sentences stay positive, and truth on Fin (n ^ k) equals truth of the pullback on Fin n. The converse uses this: a machine configuration is coded by a fixed number of elements of a polynomially larger universe, one per register, and its reachability is still expressed over the input universe.