Core Concepts
Yablo's paradox, which avoids self-reference, can be transformed into genuine mathematical theorems in Linear Temporal Logic by showing that certain operators do not have fixed-points in this logic.
Abstract
The paper presents a formal treatment of Yablo's paradox in the framework of Linear Temporal Logic (LTL). The authors show that Yablo's paradox, which was designed to avoid self-reference, can be transformed into genuine mathematical theorems in LTL.
Key highlights:
Yablo's paradox can be formalized in LTL as a fixed-point equation involving the "next" and "always" temporal operators.
The authors prove that the operator x → #2¬x (which corresponds to the original Yablo paradox) does not have any fixed-points in LTL, making this a valid theorem.
They also prove that the operators x → ¬2x and x → 2¬x do not have any fixed-points in LTL.
The authors extend this approach to other versions of Yablo's paradox, such as the "sometimes", "almost always", and "infinitely often" variants, and derive corresponding theorems in LTL.
The proofs follow the same logical structure as Yablo's original paradox, but are formalized within the LTL framework.