In this paper we investigate the relation of temporal logics and properties of Yablo sentences. We provide an (first in the literature) analysis of Yablo sentences (as formalized in temporal logic vocabulary) in , i.e., the
Linear Temporal Logic over finite traces.
0 1 2 ⋮ ⋮ For any > 0 , is false.
For any > 1 , is false.
For any > 2 , is false.
For any > , is false.
CEUR
Specifically, the so-called Assumption Logic is a multi-modal logic designed to formalize the beliefs and assumptions of agents within a multi-agent system. Initially introduced by Bonanno for belief revision, it was later simplified by Brandenburger and Keisler to articulate their paradox in epistemic game theory. To reframe their two-player impossibility result within a modal logic framework, Brandenburger and Keisler developed an interactive version of Assumption Logic, featuring two operators. Temporal Assumption Logic extends this framework, allowing for the study of how agents’ beliefs change over time.
Ensuring the reliability of both software and hardware systems is a complex task, particularly when these systems are distributed. Over the past fity years, researchers have proposed various solutions to this challenge. One notable success is the application of formal methods techniques [4]. These methods allow for the verification of a system’s correctness by formally assessing whether a mathematical model of the system meets a formal representation of its intended behavior. Linear Time Temporal Logic (LTL) [5] is a formalism used to describe sequences of events in a linear, chronological order. It allows for the specification and verification of temporal properties in systems, such as safety and liveness conditions and it is extensively used as a specification language in formal methods. LTL over finite traces ( [6] adapts Linear Time Temporal Logic to handle finite sequences of events, making it ideal for systems ) that eventually stop. Unlike standard
, which assumes events continue indefinitely, on properties within a limited timeframe. This is especially useful for scenarios like workflows or test cases where the process has a clear endpoint. This is particularly relevant in areas such as Planning and Business Process Management. A key computational advantage of finite-trace interpretation is the ability to use standard finite-state automata for modeling and reasoning, instead of the more complex omega-automata needed for infinite traces. In this paper, we give a formalization of Yablo’s Paradox focuses within the framework of .
Yablo’s paradox is one of major phenomena in formal semantics and has been investigated from many logical, mathematical, computer-scientific and philosophical points of view. A body of works that is particuarly interesting and relevant from the point of view of this paper, concerns topics such as the metalogical properties of Yablo sequences, as formalized in arithmetic and axiomatic theories of truth, metalogical properties of Yablo sequences when interpreted over potentially infinite domains with the semantics formalizing the notion of truth in the limit, and last, but not least, properties of Yablo sentences, as formalized in the temporal logic . S. Salehi and A. Karimi in [7] have initiated , obtaining some preliminary results on the semantics of Yablo’s . The study was further extended by A. Karimi in [8], where syntactic proofs using an were given for Yablo’s paradox in its various variants. the study of Yablo’s sentences in sentences in appropriate axiomatization of
A fruitful study of Yablo’s paradox formalized over arithmetic performed e.g. in [9] and in [10] has revealed that the reasoning has the following interesting feature. If we formalize the Yablo sentences over arithmetic, then in order to derive the contradiction, one needs to use a strong assumption concerning the notion of truth: namely one has to assume “for all , if and only if ⌜ ⌝ is true.” ∀ ( ≡ (
)). If we wanted to replace this uniform disquotation with an infinity of local disquotation instances, contradiction could be obtained only if we used some infinitary inference rule (requiring an infinite number of premises) such as the -rule.
So far, the story is rather well-known. What is somewhat less known, is that there is a way of handling the paradox which relies on finitistic assumptions. After all, if the world is finite, there aren’t enough things in the world to interpret all sentences from the Yablo sequence, and the last interpreted one is vacuously true without any threat of paradox. Yablo’s paradox can be thought of as an infinitary version of the Liar paradox, so perhaps thinking it can be dealt with by tackling the notion of infinity isn’t extremely implausible.
Definition 1 (Syntax of language ℒ is given by: • the set , • logical connectives: →, and ¬, • the bracket symbols: (, and ), • logical operators: ○, and .
In this paper we fill a certain gap in the literature concerning the relation of temporal logics and properties of Yablo sentences and for the first time in the literature, we perform the analysis of Yablo sentences (as formalized in temporal logic vocabulary) in , i.e., the Linear Temporal Logic over ifnite traces.
In this section, we give a formalization of Yablo’s Paradox within the framework of LTL. Before doing so let us recall the syntax and semantics of LTL.
). Let be a set of propositional variables. The alphabet of a basic propositional We use the following recursive definition of the set of formulas of ℒ : 1. every propositional variable ∈ is a formula, 2. if is a formula, then ¬ , ○ are formulas 3. if , and are formulas, then ( → ) and are formulas, and nothing else is a formula.
Semantical interpretations in classical propositional logic are given by boolean valuations. For LTL we have to extend this concept according to our informal idea that formulas are evaluated over sequences of states (’time scales’).
Definition 2 (Semantics of ). A temporal (Kripke) structure for is an infinite sequence = ( 0, 1, 2, …) of mappings ∶ → {0, 1} called states. The mapping 0 is called initial state of . Observe that states are just valuations in the classical logic sense. For and ∈ ℕ we define , ⊧ (in another formalism denoted by () = 1 ), informally meaning the ’truth value of in the th state of ’ for every formula inductively as follows: 1. , ⊧ 2. , ⊧ ¬ 3. , ⊧ → 4. , ⊧ ○ 5. , ⊧ if ( ) = 1 for each ∈ , if , ⊧ ̸ ,
if , ⊧ ¬ or , ⊧ , if , + 1 ⊧ , if there exists ≥ s.t. , ⊧
and for each ≤ < it holds that , ⊧
The Boolean connectives ∨, ∧ and ⊤ (and their semantics) can be defined as usual. We write ♦ as a shortcut for ⊤ and □ as a shortcut for ¬♦¬ .
Definition 3 (Validities of ). A formula of ℒ is called valid in the temporal structure for (or satisfies ), denoted by ⊧ , if , ⊧ for every ∈ ℕ . A formula is called a consequence of a set Δ of formulas Δ ⊧ if ⊧ holds for every such that ⊧ for all ∈ Δ . A formula is called (universally) valid ⊧ if ∅ ⊧ . Then we also say that the formula is a law of or that entails it, denoted as ⊧ . A formula is called (locally) satisfiable if there is a temporal structure and ∈ ℕ such that , ⊧ .
It can be easily seen that the following are examples of formulas that are universally valid in : and as well:
, will be of particular importance when analyzing the main diferences between behavior of Yablo sentences in and .
It immediately follow from the equivalences below that the following equivalences hold universally
is defined as the equivalence: ○□¬ ↔ □ ○ ¬ ↔
□¬ ○ . ↔ ○ □¬.
Theorem 1 (A. Karimi, S. Salehi [7]). The following is a theorem of : The proof goes by an argument demonstrating that the formula ○□ ↔
□ ○ , ¬ ○ ↔ ○¬. ¬□ ( ↔ ○ □¬. ) □ ( ↔ ○ □¬. ) ↔ ○ ♦¬, ↔ ○ ♦□¬, ↔ ○ □♦¬. ⊧ ¬ □ , is unsatisfiable in
. We will show below that this is in contrast with what happens in
As Yablo’s paradox comes in several varieties, in the paper [7] by S. Salehi and A. Karimi it has also been demosntrated that other variants of Yablo formulas are paradoxical in the same sense as obve, . when formalized in the framework of temporal logic rather than arithmetic.
The original version of Yablo’s sequence consists of the so-called Always-Y-sentences: ↔ ∀ > is not true, which when formalized in ℒ
gives the formula mentioned above, i.e., ↔ ○ □¬ .
1. Sometimes-Y-sentences: ↔ ∃ > is not true, which has the following form when A. Karimi and S. Salehi show in [7] that all the formulas above they are paradoxical in the sense that for each equivalence of the above (Sometimes, Almost-Always, and Unboundedly-Often) the following holds: meaning that the formula □ is unsatisfiable.
Below, we demonstrate that this is in contrast with the situation in when formalized in ℒ : form when formalized in ℒ : 2. Almost-Always-Y-sentences: ↔ ∃ > ∀ > is not true, which has the following form 3. Unboundedly-Often-Y-sentences : ↔ ∀ > ∃ > is not true, which has the following 1. , ⊧ 2. , ⊧ ¬ 3. , ⊧ → 4. , ⊧ ○ 5. , ⊧ the following holds: but simultaneously validity of the logic.
if ( ) = 1 for each ∈ , if , ⊧ ̸ , if , ⊧ ¬
or , ⊧ , if < max and , + 1 ⊧ , ♦ if there exists ≤ ≤
max s.t. , ⊧ .
Thus, by the semantics above, for each formula of the language ℒ we have that for any trace which proves that the law of duality of Next of does not hold universally for , i.e., it is not a 3. -interpretations, i.e., interpretations over finite traces denoting a finite sequence of consecutive instants of time. -interpretations are represented here as finite words over the alphabet of {0, 1} , i.e., as alphabet we have all the possible propositional interpretations of the propositional symbols in .
We use the following notation. We denote the length of a trace as | | . We denote the positions, i.e., instants, on the trace as ()
with 0 ≤ ≤ max, where max = | | − 1 is the last element of the trace. We denote by [, ]
the segment (i.e., the subword) obtained from starting from position and terminating in positon , 0 ≤ ≤ ≤
max.
). A temporal ( Kripke) structure for is a finite sequence = ( 0, 1, 2, … , max) of mappings ∶ → {0, 1} called states. The mapping 0 is called initial state of . Observe that states are just valuations in the classical logic sense. For and ∈ ℕ we define , ⊧ (in another formalism denoted by () = 1 ), informally meaning the ’truth value of in the th state of ’ for every formula inductively as follows: Proof. We demonstrate a stronger result, namely that for each natural number ≥ 2 there exists an interpretation (i.e., a finite trace) of size that satisfies the Yablo formula. Recall that
Let ≥ 2 be arbitrary natural number. Consider a finite trace with | | = . Let be formula mentionted in the Yablo equivalence, i.e., defined as equivalent to ○□¬ .
For each = 0 … , − 3 (observe that if = 2 , then there are no such ’s, but it does not result in any problems for the valuation) put:
, ⊧ ¬. 4. Yablo’s sentences in
under -semantics over
-domains. temporal logic over finite traces.
Theorem 2. The formula
, and allow us to recover the counterpart of the arithmetical result on non-paradoxicality of the Yablo sequence when considered We now present a result that shall e interpreted as one stating that there is no Yablo Paradox in linear , max ⊧ ¬ ○ , , max ⊧ ̸○ ¬, □ ( ↔ ○ □¬ ) of size at least 2. . Finally, for = max = − 1 define:
For = − 2 =
max −1 put: Finally, for = max = − 1 define:
, ⊧ .
⊧ ¬̸□ ( ↔ ○ □¬ ) Proof. We demonstrate a stronger result, namely that for each natural number ≥ 2 there exists an - interpretation (i.e., a finite trace) of size that satisfies the Sometimes-Y formula. Recall that
Let ≥ 2 be arbitrary natural number. Consider a finite trace with | | = . Let be formula mentionted in the Yablo equivalence, i.e., defined as equivalent to ○□¬ .
in contrast to the status of the formula in
.
Observe the valuation above is the only consistent one that can be defined on any given finite trace We also obtain similar results concerning the avoidance of paradoxicality of other Yablo sentences in Theorem 3. The temporal Sometimes-Y-formula formula □ ( ↔ ○ ♦¬ ) , ⊧ .
, ⊧ ¬. , 0 ⊧ □ ( ↔ ○ ♦¬ ) .
⊧ ¬̸□ ( ↔ ○ ♦¬ ) □ ( ↔ ○ ♦□¬ ) in contrast to the status of the formula in
.
gives us also proofs of satisfiability of the Almost-Always-Y-formula and the Unboundedly-Often-Y-formula: Theorem 4. The temporal Almost-Always-Y-formula
□ ( ↔ ○ □♦¬ )
Theorem 6. Let be the Unboundedly-Often-Y-formula, i.e., □ ( ↔ ○ □♦¬ ). Then: ∈ (Π) , where Π is the class of all finite traces over the set of propositional variables .
In this paper we have investigated the relation of temporal logics and properties of Yablo sentences, providing the analysis of Yablo sentences (as formalized in temporal logic vocabulary) in , i.e., the
2024.
1999. F. Spegni, E. Tosello, A. Umbrico, M. Vallati (Eds.), Proceedings of the International Workshop on Artificial Intelligence for Climate Change, the Italian workshop on Planning and Scheduling, the RCRA Workshop on Experimental evaluation of algorithms for solving problems with combinatorial explosion, and the Workshop on Strategies, Prediction, Interaction, and Reasoning in Italy (AI4CC-IPS-RCRA-SPIRIT 2024), co-located with 23rd International Conference of the Italian Association for Artificial Intelligence (AIxIA 2024), CEUR Workshop Proceedings, CEUR-WS.org, 2019.020.