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

Latest revision as of 07:52, 23 April 2023

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).

Comparing strengths

For the predicate version of expresses/captures, does one imply the other?

It turns out that given a sound theory, "captures" implies "expresses".

However, even for a "nice" theory, the implication in the other direction does not hold. A good example is the provability property for the theory, which takes a Goedel number of a sentence and is true iff that sentence is provable. This property turns out to be expressible but not capturable.

Capturing functions

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

$f$ is captured by $\phi (x,y)$ iff for all $m,n$ (i) if $f(m)=n$ then $T\vdash \phi ({\overline {m}},{\overline {n}})$ and (ii) $T\vdash \exists y(\phi ({\overline {m}},y)\wedge \forall v(\phi ({\overline {m}},v)\to v=y))$ .^[1]
$f$ is captured by $\phi (x,y)$ iff for all $m,n$ , if $f(m)=n$ , then $T\vdash \forall y(\phi ({\overline {m}},y)\leftrightarrow y={\overline {n}})$ .^[1]
$f$ is captured by $\phi (x,y)$ iff for all $m,n$ (i) if $f(m)=n$ then $T\vdash \phi ({\overline {m}},{\overline {n}})$ , and (ii) if $f(m)\neq n$ then $T\vdash \neg \phi ({\overline {m}},{\overline {n}})$ .^[1]
$f$ is captured by $\phi (x,y)$ iff (i) for all $m,n$ , if $f(m)=n$ then $T\vdash \phi ({\overline {m}},{\overline {n}})$ , and (ii) we have $T\vdash \forall x\exists y(\phi (x,y)\wedge \forall v(\phi (x,v)\to v=y))$ .^[1]
$f$ is captured by $\phi (x,y)$ iff for all $m,n$ (i) if $f(m)=n$ then $T\vdash \phi ({\overline {m}},{\overline {n}})$ , and (ii) if $f(m)\neq n$ then $T\nvdash \phi ({\overline {m}},{\overline {n}})$ .^[2]

I tried reading Peter Smith's explanation in IGT2 for why one version of functional capture is preferred (in particular why it's better for the theory like Q or PA to "know" that the two-place formula is functional), but I am still confused. I can't tell where, downstream in some proof that leads up to the first incompleteness theorem, this definition gets used in a way that the naive "just make sure the theory can case-by-case prove the graph relation of the function" approach doesn't work. Like he says that it basically doesn't matter which definition you pick, but then still prefers one definition that's not the naive one, without elaborating on where exactly his preferred definition is helpful compared to the naive version. Ok actually i think he does say at the beginning of that section that the crucial thing is in section 17.3, something to do with the godel beta trick.

i think i'm still confused. smith writes, "But our preferred somewhat stronger notion is the one that we will need to work with in smoothly proving the key Theorem 17.1. So that's why we concentrate on it." Theorem 17.1 is the statement that Q is p.r. adequate. But the definition of p.r. adequacy itself uses the definition of capturing functions! So maybe the trouble is that even though it doesn't matter which version of p.r. adequacy we use (possibly even what we can call "weak p.r. adequacy", the idea that the theory can weakly capture any p.r. function, is sufficient to carry on with godel's proof), what goes wrong with weak capturing is that it's very difficult to prove weak p.r. adequacy directly (i.e. without first proving regular p.r. adequacy).

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 (5th ed)	arithmetically defines^[4]	defines (for sets), represents (for functions)^[4]
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

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".

[smith-1] 1.0 ^1.1 ^1.2 ^1.3 Peter Smith. Godel book, p. 119, 120, 122.

[2] Leary and Kristiansen. A Friendly Introduction to Mathematical Logic (2nd ed). p. 121

[3] Goldrei. Propositional and Predicate Calculus. p. 137.

[boolos-4] 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".

[1]

[2]

[3]

[4]

@@ Line 3: / Line 3: @@
 * 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).
+==Comparing strengths==
+For the predicate version of expresses/captures, does one imply the other?
+It turns out that given a sound theory, "captures" implies "expresses".
+However, even for a "nice" theory, the implication in the other direction does not hold. A good example is the provability property for the theory, which takes a Goedel number of a sentence and is true iff that sentence is provable. This property turns out to be expressible but not capturable.
+==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>, 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 (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 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 \nvdash \phi(\overline m, \overline n)</math>.<ref>Leary and Kristiansen. A Friendly Introduction to Mathematical Logic (2nd ed). p. 121</ref>
+I tried reading Peter Smith's [https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf#chapter.16 explanation in IGT2] for why one version of functional capture is preferred (in particular why it's better for the theory like Q or PA to "know" that the two-place formula is functional), but I am still confused. I can't tell where, downstream in some proof that leads up to the first incompleteness theorem, this definition gets used in a way that the naive "just make sure the theory can case-by-case prove the graph relation of the function" approach ''doesn't'' work. Like he says that it basically doesn't matter which definition you pick, but then still prefers one definition that's ''not'' the naive one, without elaborating on where exactly his preferred definition is helpful compared to the naive version. Ok actually i think he does say at the beginning of that section that the crucial thing is in section 17.3, something to do with the godel beta trick.
+i think i'm still confused. smith writes, "But our preferred somewhat stronger notion is the one that we will need to work with in smoothly proving the key Theorem 17.1. So that's why we concentrate on it." Theorem 17.1 is the statement that Q is p.r. adequate. But the definition of p.r. adequacy itself uses the definition of capturing functions! So maybe the trouble is that even though it doesn't matter which version of p.r. adequacy we use (possibly even what we can call "weak p.r. adequacy", the idea that the theory can weakly capture any p.r. function, is sufficient to carry on with godel's proof), what goes wrong with weak capturing is that it's very difficult to prove weak p.r. adequacy directly (i.e. without first proving regular p.r. adequacy).
+==Comparison of usage patterns==
 {| class="sortable wikitable"
@@ Line 8: / Line 32: @@
 ! Text !! "Expresses" !! "Captures"
 |-
-| Peter Smith. Godel book || expresses || captures
+| Peter Smith. Godel book (see especially footnote 9 on p. 45) || expresses || captures
 |-
 | Leary & Kristiansen || defines || represents
 |-
-| Goldrei ||
+| Goldrei || defines (but the book also uses "represents")<ref>Goldrei. ''Propositional and Predicate Calculus''. p. 137.</ref> ||
 |-
-| Boolos, Burgess, Jeffrey || arithmetically defines<ref>George S. Boolos; John P. Burgess; Richard C. Jeffrey. ''Computability and Logic''. p. 199 for "arithmetically defines".</ref> ||
+| Boolos, Burgess, Jeffrey (5th ed) || arithmetically defines<ref name="boolos">George S. Boolos; John P. Burgess; Richard C. Jeffrey. ''Computability and Logic'' (5th ed). p. 199 for "arithmetically defines". p. 207 for "defines".</ref> || defines (for sets), represents (for functions)<ref name="boolos"/>
 |-
-| Wikipedia || ||
+| Wikipedia || [[wikipedia:Arithmetical set|arithmetically defines]], i think [https://en.wikipedia.org/wiki/Tarski's_undefinability_theorem#Statement_of_the_theorem this page] uses "defines" in the expresses sense (? actually i'm not sure; this sense of "defines" seems different) || [https://en.wikipedia.org/wiki/Diagonal_lemma#Background this page] uses "represents", but I don't think there's a standalone article for the concept
 |}
+==References==
+<references/>