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, i think this page uses "defines" in the expresses sense (? actually i'm not sure; this sense of "defines" seems different)	this page uses "represents", but I don't think there's a standalone article for the concept