# Verum or T in dynamic epistemic logic models

I've been reading a paper on dynamic epistemic logic where they use T in a way that I'm not really familar with. The paper is here by Wesley Holliday, page 16: https://pdfs.semanticscholar.org/dae6/739b8b05bf2845f2de41611c3cd0c9ae03d5.pdf

Anyway so he defines the notion of a descriptive update of phi, < phi >. Where < phi >psi is true if roughly speaking, we move from a model t1 to model t2 phi is true in t1 and psi is true in t2.

In particular however holliday talks about < phi >T V <¬ phi > T being valid. I'm trying to understand what the T here is meant to mean. He doesn't fully define it but he does say that the above sentence means that t2 is obtained from t1 by everyone publically learning whether or not phi held at t1.

For clarity, I've written this in latex:

http://www.texpaste.com/n/k44y21q2

More generally, I just want to know what it means for T to be true in a model. Part of the definition involves something like (M, t2) models T, what does that mean?

Sorry if this was unclear, I'm not really sure how to use Latex on this stack exchange, and I found it difficult to understand parts of the paper. I have attached it above with the relevant page number if that makes anything easier.

The verum symbol is a logical constant that denotes a proposition that is always true.

This implies that is true in every model.

the propositional constant ⊤ for truth is true (since ⊤ is a tautology).