User:IssaRice/Computability and logic/Expresses versus captures - Revision history

IssaRice: /* Capturing functions */

2023-04-23T07:52:02Z

Capturing functions

← Older revision		Revision as of 07:52, 23 April 2023
Line 23:		Line 23:

	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 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==		==Comparison of usage patterns==

IssaRice: /* Capturing functions */

2023-04-23T07:36:38Z

Capturing functions

← Older revision		Revision as of 07:36, 23 April 2023
Line 22:		Line 22:
	# <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>		# <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.		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.

	==Comparison of usage patterns==		==Comparison of usage patterns==

IssaRice: /* Capturing functions */

2023-04-23T07:32:46Z

Capturing functions

← Older revision		Revision as of 07:32, 23 April 2023
Line 22:		Line 22:
	# <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>		# <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 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.		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.

	==Comparison of usage patterns==		==Comparison of usage patterns==

IssaRice: /* Capturing functions */

2023-04-23T07:31:48Z

Capturing functions

← Older revision		Revision as of 07:31, 23 April 2023
Line 22:		Line 22:
	# <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>		# <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 explanation in ~~GWT2~~ 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.		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.

	==Comparison of usage patterns==		==Comparison of usage patterns==

IssaRice: /* Capturing functions */

2023-04-23T07:31:22Z

Capturing functions

← Older revision		Revision as of 07:31, 23 April 2023
Line 22:		Line 22:
	# <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>		# <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 explanation in GWT2 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.		I tried reading Peter Smith's explanation in GWT2 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.

	==Comparison of usage patterns==		==Comparison of usage patterns==

IssaRice: /* Capturing functions */

2023-04-23T07:25:21Z

Capturing functions

← Older revision		Revision as of 07:25, 23 April 2023
Line 21:		Line 21:
	# <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"/>
	# <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>		# <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 explanation in GWT2 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.

	==Comparison of usage patterns==		==Comparison of usage patterns==

IssaRice: /* Comparing strengths */

2019-04-07T18:42:28Z

Comparing strengths

← Older revision		Revision as of 18:42, 7 April 2019
Line 10:		Line 10:
	It turns out that given a sound theory, "captures" implies "expresses".		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.		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==		==Capturing functions==

IssaRice at 18:41, 7 April 2019

2019-04-07T18:41:38Z

← Older revision		Revision as of 18:41, 7 April 2019
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]].		* 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 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.

	==Capturing functions==		==Capturing functions==

IssaRice: /* Comparison of usage patterns */

2019-02-11T05:47:12Z

Comparison of usage patterns

← Older revision		Revision as of 05:47, 11 February 2019
Line 28:		Line 28:
	\| 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"/>		\| 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: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 \|\| [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		\| 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
	\|}		\|}

IssaRice at 05:38, 11 February 2019

2019-02-11T05:38:36Z

← Older revision		Revision as of 05:38, 11 February 2019
Line 28:		Line 28:
	\| 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"/>		\| 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:Arithmetical set\|arithmetically defines]] \|\| [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		\| 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 \|\| [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
	\|}		\|}