I’m not sure that adding the conjunction (R(x,y,z)&R(x,y,w)->z=w) would have made things clearer...I thought it was obvious the hypothetical mathematician was just explaining what kind of steps you need to “taboo addition”
Yes, the educational goal of that paragraph is to “taboo addition”. Nonetheless, the tabooing should be done correctly. If it is too difficult to do, then it is Eliezer’s problem for choosing a difficult example to illustrate a concept.
This may sound like nitpicking, but this website has a goal is to teach people rationality skills, as opposed to “guessing the teacher’s password”. The article spends five screens explaining why details are so important when defining the concept of a “number”, and the reader is supposed to understand it. So it’s unfortunate if that explanation is followed by another example, which accidentally gets the similar details wrong. My objections against the wrong formula are very similar to the in-story mathematician’s objections to the definitions of “number”; the definition is too wide.
Your suggestion: ‘∀x∀y∀z∀w: R(x, 0, x) ∧ (R(x, y, z)↔R(x, Sy, Sz)) ∧ ((R(x, y, z)∧R(x, y, w))→z=w)’
My alternative: ‘∀x∀y∀z: (R(x, 0, z)↔(x=z)) ∧ (R(x, y, z)↔R(x, Sy, Sz)) ∧ (R(x, y, z)↔R(Sx, y, Sz))’.
Both seem correct, and anyone knows a shorter (or a more legible) way to express it, please contribute.
Both seem correct, and anyone knows a shorter (or a more legible) way to express it, please contribute.
The version in the article now, ∀x∀y∀z: R(x, 0, x) ∧ (R(x, y, z)↔R(x, Sy, Sz)), is better than before, but it leaves open the possibility that R(0,0,7) as well as R(0,0,0). One more possibility is:
“Not in second-order logic, which can quantify over functions as well as properties. (...) It would look like, ‘∀ functions f: ((∀x∀y: f(x, 0) = x ∧ f(x, Sy) = Sf(x, y)) → Q)’ (...)”
(I guess I’m not entirely in favor of this version—ETA: compared to Kindly’s fix—because quantifying over relations surely seems like a smaller step from quantifying over properties than does quantifying over functions, if you’re new to this, but still thought it might be worth pointing out in a comment.)
I’m not sure that adding the conjunction (R(x,y,z)&R(x,y,w)->z=w) would have made things clearer...I thought it was obvious the hypothetical mathematician was just explaining what kind of steps you need to “taboo addition”
Yes, the educational goal of that paragraph is to “taboo addition”. Nonetheless, the tabooing should be done correctly. If it is too difficult to do, then it is Eliezer’s problem for choosing a difficult example to illustrate a concept.
This may sound like nitpicking, but this website has a goal is to teach people rationality skills, as opposed to “guessing the teacher’s password”. The article spends five screens explaining why details are so important when defining the concept of a “number”, and the reader is supposed to understand it. So it’s unfortunate if that explanation is followed by another example, which accidentally gets the similar details wrong. My objections against the wrong formula are very similar to the in-story mathematician’s objections to the definitions of “number”; the definition is too wide.
Your suggestion: ‘∀x∀y∀z∀w: R(x, 0, x) ∧ (R(x, y, z)↔R(x, Sy, Sz)) ∧ ((R(x, y, z)∧R(x, y, w))→z=w)’
My alternative: ‘∀x∀y∀z: (R(x, 0, z)↔(x=z)) ∧ (R(x, y, z)↔R(x, Sy, Sz)) ∧ (R(x, y, z)↔R(Sx, y, Sz))’.
Both seem correct, and anyone knows a shorter (or a more legible) way to express it, please contribute.
Shorter (but not necessarily more legible): ∀x∀y∀z: (R(x, 0, z)↔(x=z)) ∧ (R(x, Sy, z)↔R(Sx, y, z)).
Done!
Perfect!
The version in the article now, ∀x∀y∀z: R(x, 0, x) ∧ (R(x, y, z)↔R(x, Sy, Sz)), is better than before, but it leaves open the possibility that R(0,0,7) as well as R(0,0,0). One more possibility is:
“Not in second-order logic, which can quantify over functions as well as properties. (...) It would look like, ‘∀ functions f: ((∀x∀y: f(x, 0) = x ∧ f(x, Sy) = Sf(x, y)) → Q)’ (...)”
(I guess I’m not entirely in favor of this version—ETA: compared to Kindly’s fix—because quantifying over relations surely seems like a smaller step from quantifying over properties than does quantifying over functions, if you’re new to this, but still thought it might be worth pointing out in a comment.)