# Standard word for a formula that is always true

If it is known from context that variables $x$ and $y$ represent integers, an open Boolean formula such as $x \ge y \Rightarrow x+1 > y$ evaluates to true regardless of the value assigned to variables $x$ and $y$, at least in the standard interpretation of arithmetic. What should (or could or would) one call such a formula?

I've been using the term "valid", but am not very happy with this. Logicians (e.g. Boolos and Jeffery") use "valid" for closed formulas that are true regardless of the interpretation. I could just call it "true", but this seems to fail to acknowledge that there are free variables. It might be called a "theorem", but I'd rather stay away from issues of provability.

Just for context: This is not a course in logic, but a course that uses logic as a tool for proving things about software. So I'd like to be consistent with standard logical terminology without getting into the possibility of multiple interpretations.

• It seems to me that you're looking for the word tautology – Jim Belk Mar 30 '14 at 15:31
• No, tautology doesn't take into account interpretation. In the question $+, \ge$ and $>$ are all being interpreted. – Git Gud Mar 30 '14 at 15:33
• It seems to me that what makes this tricky to describe is the absence of universal quantifiers. If the formula were $\forall x \forall y : x \geq y \Rightarrow x + 1 > y$ there would be no free variables and you would just say that it is "true". I note that your statement of the question does include quantifiers, but they are in the surrounding text ("regardless of the values...") rather than in the formula itself. – mweiss Mar 30 '14 at 16:33
• @GitGud This depends on which symbols you think are open to interpretation. Even a statement like $A \lor (\lnot A)$ is only a tautology if you use the standard interpretation of the symbols $\lor$ and $\lnot$. Of course, if we are discussing formal logical systems, then it is usual to think of the interpretations of logical symbols as fixed, while other symbols are open to interpretation. However, I think in the more general context of mathematics, it's perfectly reasonable to refer to a statement like $x \geq y \Rightarrow x+1 > y$ as a tautology. – Jim Belk Mar 30 '14 at 16:42
• Writing formulas with free variables where the universal quantifiers are implicit is common enough that it might be worthwhile to be explicit about this convention with your students. The formula you mention in your question is a great example with which to introduce this standard ellipsis. (Note that existential quantifiers are never left implicit in this way.) Once you read the formula with implicit universal quantifiers, the word you're looking for becomes merely "true". – Adam Bjorndahl Mar 30 '14 at 20:34

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 states in which the 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 is a "Boolean structure" which represents a set of states, while $$[x\ge y\Rightarrow x.