Hyperintensionality
Justification logic offers a formal framework for Byperintensionality. The hy- perintensionalparadox was formulated in Cresswell (1975).
It is well known that it seems possible to have a situation in which there are two propositions p and q which are logically equivalent and yet are such that a person may believe the one but not the other.
If we regard a proposition as a set of possible worlds then two logically equivalent propositions will be identical, and so if “x believes that” is a genuine sentential functor, the situation described in the opening sentence could not arise. I call this the paradox of hyperintensional contexts. Hyper- intensional contexts are simply contexts which do not respect logical equivalence.Starting with Cresswell himself, several ways of dealing with this have been proposed. Generally, these involve adding more layers to familiar possible world approaches so that some way of distinguishing between logically equivalent sentences is available. Cresswell suggested that the syntactic form of sentences be taken into account. Justification logic, in effect, does this through its mechanism for handling justifications for sentences. Thus justification logic addresses some of the central issues of hyperintensionality but, as a bonus, we automatically have an appropriate proof theory, model theory, complexity estimates, and a broad variety of applications.
A good example of a hyperintensional context is the informal language used by mathematicians conversing with each other. Typically when a mathematician says he or she knows something, the understanding is that a proof is at hand, but this kind of knowledge is essentially hyperintensional. For instance Fermat's Last Theorem, FLT, is logically equivalent to 0 = 0 because both are provable and hence denote the same proposition, as this is understood in modal logic.
However, the context of proofs distinguishes them immediately because a proof of 0 = 0 is not necessarily a proof of FLT, and vice versa. To formalize mathematical speech, the justification logic LP is a natural choice because t:X was designed to have characteristics of “t is a proof of X.”
Going further LP, and justification logic in general, is not only sufficiently refined to distinguish justification assertions for logically equivalent sentences, but it also provides flexible machinery to connect justifications of equivalent sentences and hence to maintain constructive closure properties desirable for 
that V is a proof of X, and so v.X. It has already been mentioned that this does not mean v is a proof of Y—this is a hyperintensional context. However within the framework of justification logic, building on the proofs of X and of 
we can construct a proof term f(u, v), which represents the proof of Y and so f (u, v):Y is provable. In this respect, justification logic goes beyond Cresswell's expectations: Logically equivalent sentences display different but constructively controlled epistemic behavior.
1.4