User:IssaRice/Computability and logic/Expresses versus captures: Difference between revisions
No edit summary |
|||
Line 5: | Line 5: | ||
==Capturing functions== | ==Capturing functions== | ||
For functions, it seems like there are at least four different strengths. | |||
# <math>f</math> is captured by <math>\phi(x,y)</math> iff for all <math>m,n</math> (i) if <math>f(m) = n</math> then <math>T \vdash \phi(\overline{m}, \overline{n})</math> and (ii) <math>T \vdash \exists y (\phi(\overline{m}, y) \wedge \forall v(\phi(\overline{m}, v) \to v=y))</math>.<ref name="smith">Peter Smith. Godel book, p. 119, 120, 122.</ref> | |||
# <math>f</math> is captured by <math>\phi(x,y)</math> iff for all <math>m,n</math> (i) if <math>f(m)=n</math> then <math>T \vdash \phi(\overline m, \overline n)</math>, and (ii) if <math>f(m)\ne n</math> then <math>T \vdash \neg \phi(\overline m, \overline n)</math>.<ref name="smith"/> | |||
# <math>f</math> is captured by <math>\phi(x,y)</math> iff (i) for all <math>m,n</math>, if <math>f(m) = n</math> then <math>T \vdash \phi(\overline m, \overline n)</math>, and (ii) we have <math>T \vdash \forall x \exists y (\phi(x,y) \wedge \forall v (\phi(x,v) \to v=y))</math>.<ref name="smith"/> | |||
==Comparison of usage patterns== | ==Comparison of usage patterns== |
Revision as of 06:17, 7 February 2019
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.
- is captured by iff for all (i) if then and (ii) .[1]
- is captured by iff for all (i) if then , and (ii) if then .[1]
- is captured by iff (i) for all , if then , and (ii) we have .[1]
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")[2] | |
Boolos, Burgess, Jeffrey | arithmetically defines[3] | defines (for sets), represents (for functions)[3] |
Wikipedia | arithmetically defines | this page uses "represents", but I don't think there's a standalone article for the concept |