User:IssaRice/Computability and logic/Expresses versus captures

The expresses versus captures distinction is an important one in mathematical logic, but unfortunately the terminology differs wildly between different texts. The following table gives a comparison.

• Expressing is done by a language. There is only one form of expressing; I think this follows from the wikipedia:Law of excluded middle.
• Capturing is done by a theory or by axioms. There are two forms of capturing: strong capture (corresponding to deciding), and weak capture (corresponding to recognizing, or semi-deciding).

Capturing functions

For functions, it seems like there are at least four different strengths.

1. $f$ is captured by $\varphi (x,y)$ iff for all $m,n$ (i) if $f(m)=n$ then $T⊢\varphi (\overline{m},\overline{n})$ and (ii) $T⊢\mathrm{\exists }y(\varphi (\overline{m},y)\wedge \mathrm{\forall }v(\varphi (\overline{m},v)\to v=y))$.
2. $f$ is captured by $\varphi (x,y)$ iff for all $m,n$, if $f(m)=n$, then $T⊢\mathrm{\forall }y(\varphi (\overline{m},y)\leftrightarrow y=\overline{n})$.
3. $f$ is captured by $\varphi (x,y)$ iff for all $m,n$ (i) if $f(m)=n$ then $T⊢\varphi (\overline{m},\overline{n})$, and (ii) if $f(m)\ne n$ then $T⊢\mathrm{\neg }\varphi (\overline{m},\overline{n})$.
4. $f$ is captured by $\varphi (x,y)$ iff (i) for all $m,n$, if $f(m)=n$ then $T⊢\varphi (\overline{m},\overline{n})$, and (ii) we have $T⊢\mathrm{\forall }x\mathrm{\exists }y(\varphi (x,y)\wedge \mathrm{\forall }v(\varphi (x,v)\to v=y))$.
5. $f$ is captured by $\varphi (x,y)$ iff for all $m,n$ (i) if $f(m)=n$ then $T⊢\varphi (\overline{m},\overline{n})$, and (ii) if $f(m)\ne n$ then $T⊬\varphi (\overline{m},\overline{n})$.

Comparison of usage patterns

Text	"Expresses"	"Captures"
Peter Smith. Godel book (see especially footnote 9 on p. 45)	expresses	captures
Leary & Kristiansen	defines	represents
Goldrei	defines (but the book also uses "represents")
Boolos, Burgess, Jeffrey (5th ed)	arithmetically defines	defines (for sets), represents (for functions)
Wikipedia	arithmetically defines	this page uses "represents", but I don't think there's a standalone article for the concept