User:IssaRice/Computability and logic/Expresses versus captures: Difference between revisions
| Line 9: | Line 9: | ||
# <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) <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>, if <math>f(m) = n</math>, then <math>T \vdash \forall y (\phi(\overline m,y) \leftrightarrow y = \overline n)</math><ref name="smith"/> | |||
# <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 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"/> | # <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"/> | ||
Revision as of 19:30, 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 , if , then [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]
- is captured by iff for all (i) if then , and (ii) if then .[2]
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")[3] | |
| Boolos, Burgess, Jeffrey | arithmetically defines[4] | defines (for sets), represents (for functions)[4] |
| Wikipedia | arithmetically defines | this page uses "represents", but I don't think there's a standalone article for the concept |
References
- ↑ 1.0 1.1 1.2 1.3 Peter Smith. Godel book, p. 119, 120, 122.
- ↑ Leary and Kristiansen. A Friendly Introduction to Mathematical Logic (2nd ed). p. 121
- ↑ Goldrei. Propositional and Predicate Calculus. p. 137.
- ↑ 4.0 4.1 George S. Boolos; John P. Burgess; Richard C. Jeffrey. Computability and Logic (5th ed). p. 199 for "arithmetically defines". p. 207 for "defines".