Question on deriving $\alpha \rightarrow \Box \alpha$ in modal logic KTU

Let K and T be the usual modal logical principles $\Box (\alpha \rightarrow \beta) \rightarrow (\Box \alpha \rightarrow \Box \beta)$ and $\Box \alpha \rightarrow \alpha$. Let U be the modal logical principle $\Box \Diamond \alpha \rightarrow \Box \alpha$. Let propositional modal logic KTU be the extension of classical propositional logic with the modal logical principles K,T and U. Also, KTU is supposed to be normal so that it has the necessitation rule.

T imposes reflexivity upon situations, and U corresponds with the first order condition that a situation $u$ sees a situation $v$ just if $u$ sees a situation $w$ suchthat $w$ only sees $v$. By an elementaryargument, KTU is characterized by frames which are autistic, i.e where any situation sees itself and only sees itself.

$\alpha \rightarrow \Box \alpha$ is valid in autistic frames. Question: How do we derive $\alpha \rightarrow \Box \alpha$ in KTU? Alternatively, is KTU incomplete?

• The logic should be complete, as both $\Box p\to p$ and $\Diamond p\to\Diamond\Box p$ are Sahlqvist formulas. – Emil Jeřábek May 5 '14 at 15:05
• Off-topic comment: like the word "schizophrenic" in categorical studies of Stone duality, this word "autistic" is a pretty unfortunate term, although it seems to be standard. – Todd Trimble May 5 '14 at 15:32

$\let\B\Box\let\D\Diamond\let\A\alpha$T gives $\B\D\neg\A\to\D\neg\A$, i.e., $\D\B\A\lor\D\neg\A$. This implies $\D(\A\to\B\A)$ in K, and then we derive $\B\D(\A\to\B\A)$ by necessitation, $\B(\A\to\B\A)$ by U, and $\A\to\B\A$ by T.