I'm struggling to understand this reasoning. I've simplified it, but you can find it in full in the text Computability and Unsolvability (1985) by Martin Davis, chapter 3, page 48.
Let $P(z)$ be a predicate on natural numbers:
Suppose that for all $z∈ℕ$ between $z=0$ and $z=y-1$, $P(z)$ holds. That is equivalent to say that y is the least $z∈ℕ$ for which $P(z)$ may not hold. That is to say that y is the least $z∈ℕ$ such that $¬P(z)$ or, if $P(z)$, than $z=y$.
More formally: $∀z∈ℕ(0≤z≤y-1 ⟹ P(z))$ iff $y=min\{z∈ℕ|¬P(z)∨z=y\}$
Now, it's not at all clear to me the last passage, especially with regard to the addition of $z=y$. Can adding $z=y$ at the end really safeguard the idea that $P(y)$ may hold? Can someone explain to me why the two propositions are equivalent? Thanks.
Try thinking about the elements of the set $S_y := \{z \in \mathbb{N} : \lnot P(z) \lor z = y\}$. It contains every $z$ for which $P(z)$ does not hold, and it also contains $y$ regardless of whether $P(y)$ holds or not. In fact, we can write $S_y = P^c \cup \{y\}$, where $P^c = \{z \in \mathbb{N} : \lnot P(z)\}$.
Does $S_y$ have a minimum element? Yes, because $y \in S_y$ it's a non-empty subset of the natural numbers, and hence it has a least element. And what does $\min(S_y) = y$ imply? Since $P^c \subseteq S_y$, $\min(P^c) \geq S_y = y$, meaning that the least element of $P^c$ is greater than or equal to $y$. But that means that $\lnot P(z)$ cannot be true for any value of $z$ less than $y$.