Jeffery Ketland proved in his Yablo's paradox and $\omega$-inconsistency that the set of Yablo sentences, which leads to Yablo's paradox, is $\omega$-inconsistant, but I do not understand his proof. Could anyone help please?
I understand how $\forall y>n \lnot F(y)$ and $\forall y>n+1 \lnot F(y)$ are derived, but how did we get both $F(n+1)$ and $\lnot F(n+1)$? For $F(n+1)$, is it because we assumed our theory now includes $\{F(n)\}$ for any $n\in \omega$, so we can instantiate $F(n+1)$? For $\lnot F(n+1)$, is it because $\forall y>n \lnot F(y)$? (i.e. $\forall y>n$ includes $n+1$)
I see how the contradiction shows $PA_F\vdash \lnot F(n)$, for all $n\in \omega$. But how does this lead to $PA_F\vdash \exists y> n F(y)$, for all $n\in \omega$?
Re 1): Yes, from the "axiom-set" $\mathsf {PA}_F \cup \{ F(\underline n) \}$ we get $F(\underline {n+1})$ and from $∀y> \underline n ¬F(y)$ we get $¬F(\underline {n+1})$ by instantiation.
Re 2): because $\mathsf {PA}_F$ is defined as $\mathsf {PA} \cup \{ \forall x [Fx \leftrightarrow \forall y > x \lnot Fy] \}$.
But the formula is equivalent to:$\lnot F \underline n \leftrightarrow \lnot \forall y > \underline n \lnot Fy$ which is simply: $\lnot F \underline n \leftrightarrow \exists y > \underline n Fy$.
Thus, the conclusion follows by MP.