This question is related to Mikhail Katz's recent mathoverflow question, "Has Dedekind's proof of the existence of existence of infinite sets been analyzed by historians?". Dedekind's 'proof' seems (at least to me) to boil down to (the realm of his thoughts notwithstanding) the following question:
Can $\omega$ be proven to be Dedekind-infinite (i.e., that there is a proper subset of $\omega$ that can be put in 1-1 correspondence with $\omega$), and that no finite set of $\omega$ can be put in 1-1 correspondence with any of its proper subsets?
Positive set theory is a consistent fragment of Naive Set Theory consisting of:
Extensionality: $x$=$y$ $\leftrightarrow$($\forall$$a$)($a$$\in$$x$$\leftrightarrow$$a$$\in$$y$)
Comprehension for positive formulas: ($\forall$$w_1$,...,$w_n$)($\exists$$S$)($\forall$$x$)($x$$\in$$S$$\leftrightarrow$$\varphi$($x$,$w_1$,...,$w_n$), where $\varphi$ is contained in the smallest class of formulas closed under $\land$, $\lor$, $\exists$, $\forall$, =, $\in$.
My questions are these:
(i). Can the notion of finite set be adequately defined in positive set theory?
(ii). Can it be proven in positive set theory that no finite set can be put in 1-1 correspondence with any of its proper subsets?
Since it is reasonable to assume that $\omega$ can be defined in positive set theory and that 1-1 correspondences of $\omega$ to proper subsets of $\omega$ can also be defined in positive set theory, this would seem to show forth the basic validity of Dedekind's proof of the existence of infinite sets (the realm of his thoughts notwithstanding).