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