I use ZFC with the axiom of Regularity.
- At page 62 of my notes I prove that "There is no infinite descending membership chains" (because of well-ordering of $\mathbb{N}_0$),
- The Lemma "No infinite descending membership chains" is connected with the Axiom of Regulatity (see for example here)
- In my notes I used the axiom of Regulatity only to prove that $x\notin x$ (special case of "No infinite descending membership chains").
My question is: If I had a pretty standard derivation of the natural numbers (with Peano axioms) at which point I could have applied (I mean: is applied in the standard derivation) the axiom of Regularity? I must have done some derivation using it but unknowingly.
EDIT Other formulation of my question.
I prove that "There is no infinite descending membership chains" (because of well-ordering of $\mathbb{N}_0$), without using directly the axiom of Regularity. But, since the "no infinite descending membership chains" is connected to the Axiom of Regularity, I must have applied it somewhere on the way, unknowingly. Q: At which point is applied the Axiom of Regularity in a standard derivation (using Peano) of the claim "There is no infinite descending membership chains"?
EDIT Draw of the derivation
The construction of $\mathbb{N}_0$ is perhaps after all not that standard: see ch. 3.
- Ch. 1: Axioms of ZFC as in Wikipedia or Ciesielski1997 (there are some minor differences), nothing exotic. Consequences of the axioms (e.g $x\notin x$, aso). Set operations with their properties.
- Ch. 2: Relations and Functions
- Ch. 3: 3.1) Natural Numbers: Set-theoretic definition: A natural number is a set that belongs to every inductive set ($\varnothing \in x$ and $y\in x\to S(y)\in x$, where $S(x)=x\cup \{x\}$). 3.2) Peano System defined as $(X,i,f)$ (properties $f$ injective, $i\notin\textrm{ran}(f)$, $(X,i,f)$ has no proper subsystem). Properties of a Peano system. Proof that $\mathbb{N}_0$ (as defined in 3.1) is a Peano system. 3.3 recursion and isomorphism 3.4 operations on $\mathbb{N}_0$.
- Ch. 4: 4.1 Well-ordering 4.2 Ordering on $\mathbb{N}_0$
Note: I use $f$ for generic Peano system and $S$ for $\mathbb{N}_0$.
At this point I have the following Lemmas:
Lemma $(\mathbb{N}_0,\le)$ is a well-ordering.
Proof Suppose that $X\subseteq\mathbb{N}_0$ and that $X$ does not have a minimum. Define $Y:=\{y\in\mathbb{N}_0:\neg \exists x(x\in X\land x<y)\}$, that is "there is no member of $X$ smaller than $y$". We show that $Y$ is inductive. (1) $0\in Y$, since no natural number is smaller than $0$. (2) Suppose $y\in Y$, then $\neg \exists x(x\in X\land x<y)$ ans thus, since $y<S(y)$, $\neg \exists x(x\in X\land x<S(y))$ or $S(y)\in Y$. Thus $Y$ is inductive and $Y=\mathbb{N}_0$, therefore $X=\varnothing$, the only subset of $\mathbb{N}_0$ without a minimum.
(Actually not really relevant for this Question) Lemma, Infinite Descent Given a statement $P(x)$ with $x\in\mathbb{N}_0$, then $P(x)\to \exists y(y<x\land P(y))$ implies $\forall x\neg P(x)$, or $X=\{x\in\mathbb{N}_0:P(x)\}=\varnothing$.
Proof The consequence of the hypothesis is that $X$ has no minimum, and being $\mathbb{N}_0$ well-ordered it follows that $X=\varnothing$.
Lemma There are no infinite descending membership chains. Or: There is no infinite $\in$-decreasing sequence in $\mathbb{N}_0$, that is, there is no sequence $\{x_n:n\in\mathbb{N}_0\}$ such that $x_{n+1}\in x_n$ for all $n\in\mathbb{N}_0$.
Proof Otherwise the set $\{x_n:n\in\mathbb{N}_0\}$ would have no $\in$-minimal element (which is not the case since $\mathbb{N}_0$ is well-ordered).
You need to distinguish carefully between what you're saying and proving. As stated, you're not quite precise about what you mean by either "there are no" and "infinite descending membership chain".
In regular ZF(C), what you can prove using the Axiom of Regularity is
On the other hand, what you can prove without regularity is
Of these, (2) is a weaker claim because the class of possible things it says cannot exist is smaller. Therefore it should be unsurprising that it is easier to prove and doesn't need the specific axiom that tells you (1).
(It's like the difference between claiming "unicorns don't exist" and "there are no unicorns in my living room").
Independently of this, be aware that if you have a model of ZFC, it may well be that you, looking at the model from the outside, can find a sequence of elements such that each has the next as an element -- even though both of claims (1) and (2) above are true inside the model.
That will be because the sequence you can see from the outside is not represented as a function $f:\mathbb N\to V$ that is itself an element of the model. So formulas in the first-order language of set theory cannot even speak about whether or not it exists.
(And there must exist such models if ZFC is consistent at all, as a standard compactness argument shows. In fact, every model has an elementary extension that has a descending chain of naturals).