I asked
What should (or could or would) one call such a formula?
Several good suggestions came up in the comments
- "a law"
- "a fact"
- "a tautology"
- "true"
- "universally true"
I'd like to thank everyone who commented. Given that these are all good suggestions, I'm willing to consider the question answered.
Many people up voted "tautology". In fact, it is a word I've used in the past. I'd like to warn that there is at least one competing definition for "tautology" applied to a first order formula. This is that a formula is a tautology if and only if it is an instance of a propositional tautology. For example $x=0 \vee \neg(x=0)$ is a tautology, as it is an instance of $P\vee \neg P$, but $2+2=4$ is not a tautology. As I said in the OP, I wanted to be consistent with the standard logical terminology, so that ruled out "tautology" for me.
I ended up with "universally true". For context, this is a computing course and the kinds of formulas we typically deal with describe states of the computer. E.g. $x=y$ describes all state in which a location called "x" contains the same value as the location called "y". Usually the right question to ask about such a formula is not whether it is "true" or not, but which states is it true of. This is the reason I preferred not to use simply "true". "Law" and "fact" are to me slightly more suggestive than "true", but I didn't think that they went far enough in emphasizing the universality.
Finally, I'll note that Dijkstra and Scholten in their book Predicate Calculus and Program Semantics use the square brackets as an operator which they call "everywhere". This operator is applied to what they call "Boolean structures", which are essentially the same as what most of us would call Boolean functions. For them a condition $x\ge y\Rightarrow x<y+1$ is a "Boolean structure" which represents a set of states, while $[x\ge y\Rightarrow x<y+1] = \mathit{true}$.