Theoremizing Yablo's Paradox
Ahmad Karimi, Saeed Salehi
TL;DR
The paper reframes Yablo's paradox as a mathematical theorem within Linear Temporal Logic (LTL), treating the paradox as a fixed-point problem for time-indexed propositions. It formalizes the core Yablo construction as $\mathcal{Y}_n \Longleftrightarrow \forall k>n (\mathcal{Y}_k \text{ is not true})$ and shows that the associated operator $x \mapsto \Circle\Box\neg x$ has no fixed-point in LTL, yielding the theorem $LTL \models \neg \Box (\varphi \leftrightarrow \Circle\Box\neg\varphi)$. The work extends this approach to several Yablo variants (always, sometimes, almost always, infinitely often), providing corresponding LTL theorems and corollaries (e.g., $LTL \models \neg \Box (\varphi \leftrightarrow \Circle\diamondsuit\neg\varphi)$ for the sometimes version). Overall, the authors demonstrate that paradoxical reasoning can give rise to rigorous, new theorems in temporal logic, linking classic diagonal/self-reference themes to time-sensitive semantics.
Abstract
To counter a general belief that all the paradoxes stem from a kind of circularity (or involve some self--reference, or use a diagonal argument) Stephen Yablo designed a paradox in 1993 that seemingly avoided self--reference. We turn Yablo's paradox, the most challenging paradox in the recent years, into a genuine mathematical theorem in Linear Temporal Logic (LTL). Indeed, Yablo's paradox comes in several varieties; and he showed in 2004 that there are other versions that are equally paradoxical. Formalizing these versions of Yablo's paradox, we prove some theorems in LTL. This is the first time that Yablo's paradox(es) become new(ly discovered) theorems in mathematics and logic.