= Complement of a total Sigma-1 function graph
{title2=$f(\vec x)\ne y\iff\exists z\,(f(\vec x)=z\wedge z\ne y)$}
If a total single-valued numerical <function> has a Sigma-1 graph, the complement of that graph is also Sigma-1. An input-output pair is outside the graph exactly when some different output is in the graph. Totality and uniqueness are essential to that equivalence. Stage-comparison separation of enumerations of the graph and its complement then gives <weak definability of a numerical function> in a bounded-complete <arithmetic> <first-order theory>.
Back to article page