User:IssaRice/Computability and logic/Expresses versus captures: Difference between revisions

From Machinelearning
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.

  1. is captured by iff for all (i) if then and (ii) .[1]
  2. is captured by iff for all (i) if then , and (ii) if then .[1]
  3. 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

References

  1. 1.0 1.1 1.2 Peter Smith. Godel book, p. 119, 120, 122.
  2. Goldrei. Propositional and Predicate Calculus. p. 137.
  3. 3.0 3.1 George S. Boolos; John P. Burgess; Richard C. Jeffrey. Computability and Logic (5th ed). p. 199 for "arithmetically defines". p. 207 for "defines".