# A Kripke kōan

A student came to Spivey and said, "Master, is it true that enlightenment, once achieved, is everlasting [ **G** (*p* → **G** *p*) ], and that enlightenment brings contentment [ **G** (*p* → *q*) ]?"

"What you say is true."

"Then will all attain enlightenment [ **F** (**G** *p*) ]?"

"No, but all will achieve everlasting contentment [ **F** (**G** *q*) ]."

"How can this be?"

"It is the search for enlightenment that brings discontent. Those who never seek it remain content, as do the beasts of the field."

"Then will all reach a condition where their contentment is secure [ **AF** (**AG** *q*) ]?"

"No, for the possibility of seeking enlightenment endlessly burdens the unenlightened with the risk of passing discontent [ **EG** (**EF** ¬*q*) ]."

"I ask again, how can this be?"

"My child, you must study diligently the writings of the master Kripke. For these truths cannot be written in the linear way."

The student left, more puzzled than before.

## Analysis

In lecture notes, it is stated that **F** (**G** *q*) is an LTL formula without an equivalent CTL formula, and conversely that the CTL formula **AF** (**AG** *q*) has no equivalent in LTL. The question naturally arises of showing at least that these two formulas are not counterparts of each other.

To do this, consider the following Kripke structure:

Every infinite path from *s*_{0} either stays in state *s*_{0}, 'never seeking enlightenment,' and therefore keeps *q* true forever, or it eventually reaches state *s*_{2}, where *q* remains true. Thus the structure satisfies the LTL formula **F** (**G** *q*).

On the other hand, state *s*_{0} does not satisfy the CTL formula **AG** *q*, since there is a path 〈*s*_{0}, *s*_{1}, *s*_{2}, *s*_{2}, ...〉 on which *q* is momentarily false. Therefore state *s*_{0} does not satisfy **AF** (**AG** *q*), for there is a path 〈*s*_{0}, *s*_{0}, ...〉 on which **AG** *q* is never true.

[I found the counteraxample in a much-cited paper of Clarke and Draghicescu; indeed, most of the examples of mutual inexpressibility that appear online seem to be taken directly from that source.]