Standard word for a formula that is always true

Question

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.

Answer 1

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 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+1 > y$, where $x$ and $y$ are integer variables, is a "Boolean structure" which represents a set of states, while $[x\ge y\Rightarrow x+1 > y] = \mathit{true}$.

Answer 2

Expanding my comment into an answer:

So you want the umbrella term for a predicate (propositional function), like the triangle or Cauchy–Schwarz inequality, that's always true, but not necessarily so regardless of interpretation. So, ‘validity’ and ‘tautology’ are ruled out.

If the object is an equality instead of inequality, I'd have suggested ‘identity’ (a universally-quantified equation)...

@RyanG Yes, that's what I want. Although, as mentioned in a recent comment, I'm skittish around the word "predicate". I like 'identity' because it's a word that students already know, e.g. from trig. The question is whether it's too much of a reach to extend the word to boolean expressions that aren't equalities.

...For inequalities, we might similarly distinguish between “identity inequalities” and non-identity inequalities? This is clearly not standard terminology either, but a google search did return this definition as the first result:

“An identity inequality is an inequality that is true no matter what values we plug in for the variable.”

P.S. I agree that "predicate" is a bad choice for the purpose: not only is it distractingly formal-logical, it even has two (related but) distinct definitions within the field of logic.

P.P.S. Possibly related.

Answer 3

Your self-answer is wrong, because a tautology must be true under every interpretation, but your example is certainly not so. There is no single word for what you want, but the standard terminology is that your formula is true under standard/intended interpretation. And you can note that it is conventional to say just "true" to mean that when dealing with arithmetical formulae. The failure to understand this conventional meaning of "true arithmetical sentence" underlies a large fraction of misunderstandings of Godel's incompleteness theorems due to the phrase "true but unprovable statements".

Nor is "universally true" correct for the same reason.