Weak definability of a numerical function ($f(\vec{n})=m⟹S⊢D(\overline{\stackrel{⃗}{n}},\bar{m}),S⊢\neg D(\overline{\stackrel{⃗}{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.

Strong definability of a numerical function adds internal uniqueness of the output at every standard input tuple. Together with a proved correct instance, this says the first-order theory proves that the output logical formula is equivalent to logical equality with the correct numeral, for arbitrary potential outputs.