New Paper: Is Frege's Definition of the Ancestral Correct?

I've posted a new paper to my website, titled "Is Frege's Definition of the Ancestral Correct?" (PDF here) The paper is scheduled to appear in a special issue of Philosophia Mathematica edited by Roy Cook and Erick Rech.
Abstract:

Why should one think that Frege's definition of the ancestral is correct? It can be proven to be extensionally correct, but the argument uses arithmetical induction, and that fact might seem to undermine Frege's claim to have justified induction in purely logical terms—a worry that goes back to Bruno Kerry and Henri Poincaré. In this paper, I discuss such circularity objections and then offer a new definition of the ancestral, one that is intended to be intensionally correct; its extensional correctness then follows without proof. It can then be proven to be equivalent to Frege's definition, without any use of arithmetical induction. This constitutes a proof that Frege's definition is extensionally correct that does not make any use of arithmetical induction, thus answering the circularity objections.

In the general case, the new definition is fairly complicated. But in the special case of the concept of natural number, it reduces to:

n is a natural number iff there exists a Dedekind finite concept (or set) F such that F0, Fn, and ∀x∀y[Fx & Pxy & x≠n → Fy]

The last condition says that F is closed under successors, except that it need not be true of the successor of n. The point, which has also been noted (independently) by Aldo Antonelli and Albert Visser, is that Dedekind finitude can be used here, so the definition is non-circular. The intuitive idea is just that, if n is not finite, then the other three conditions force every natural number to be F, in which case of course F is Dedekind infinite. If n is finite, by contrast, then F is just [x: 0 ≤ x ≤ n].
One can then go onto prove induction from this definition, using many of the results Frege proves for his own definition of the ancestral.