Expressibility of output equals input. Negative and positive results (Q1323378)

We examine the common and seemingly simple specification that the output stream equals the input stream. We show that this is not in full generality expressible in first-order or temporal logic by an infinite set of sentences or a recursive specification, but requires certain extra assumptions, such as the existence of a clock or discrete input values. The main negative results are stated for first-order expressibility and have direct corollaries for inexpressibility in first-order temporal logic: output equals input with arbitrary delay is not expressible by a (perhaps infinite) theory (Theorems 2 and 3), even with a timestamp (Theorem 8), and is not expressible for an \(\omega\) timeline by a sentence, even with a timestamp (Theorem 10). Output equals input with constant delay cannot be expressed for \(\omega\) timeline by a sentence with extra unary predicates over the timeline. As an example of the positive results, we show output equals input can be expressed by a sentence in the language with a (weak) clock if the base model contains either an extra function (Theorem 14), or arithmetic (Theorem 15).