= Weak definability of a numerical function
{title2=$f(\vec n)=m\Longrightarrow S\vdash D(\bar{\vec n},\bar m),\quad S\vdash\neg D(\bar{\vec n},\bar r)\ (r\ne m)$}
A <logical formula> weakly defines a total numerical <function> in a <first-order theory> when, at every standard input <tuple>, it proves the graph instance with the correct standard output and refutes graph instances with every incorrect standard output. This is numeralwise representation of the graph; it does not yet assert uniqueness against nonstandard outputs inside a <first-order model>.
Back to article page
