# Sometime a Paradox, Now Proof: Non-First-Order-izability of Yablo's Paradox

## TL;DR

This paper investigates Yablo's paradox within formal logic frameworks, demonstrating that its second-order formalization cannot be captured by first-order logic, highlighting limitations in formalizing certain paradoxes.

## Contribution

It proves that Yablo's paradox, formalized in second-order logic, is non-first-order-izable, revealing fundamental constraints in logical formalizations of paradoxes.

## Key findings

- Yablo's paradox formalization is second-order in nature.
- It cannot be represented within first-order logic.
- This highlights limitations in formal logical systems.

## Abstract

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).