  Paradoxes are interesting puzzles in philosophy and mathematics, and they
could be even more fascinating, when turned into proofs and theorems. For
example, Liar's paradox can be translated into a propositional tautology, and
Barber's paradox turns into a first-order tautology. Russell's paradox, which
collapsed Frege's foundational framework, is now a classical theorem in set
theory, implying that no set of all sets can exist. Paradoxes can be used in
proofs of some other theorems; Liar's paradox has been used in the classical
proof of Tarski's theorem on the undefinability of truth in sufficiently rich
languages. This paradox (and also Richard's paradox) appears implicitly in
G\"{o}del's proof of his celebrated first incompleteness theorem. In this
paper, we study Yablo's paradox from the viewpoint of first and second order
logics. We prove that a formalization of Yablo's paradox (which is second-order
in nature) is non-first-order-izable in the sense of George Boolos (1984).
