logical truth, tautology
A property of formulas in the language of predicate calculus, meaning that the formulas are true in all interpretations and for all admissible values of their free variables. For example, for a formula containing only one $ 2 $- place predicate symbol $ \rho $ and variables of one sort (that is, variables which are interpreted in the same domain of variation), any pair $ ( M , R ) $, where $ M $ is an arbitrary non-empty set and $ R \subseteq M \times M $ is an arbitrary binary relation on $ M $, is an interpretation. Arbitrary elements of $ M $ are admissible values for the free variables. Truth of a formula $ \phi ( x _ {1} \dots x _ {n} ) $ at values $ a _ {1} \dots a _ {n} $( $ n \geq 0 $) of the variables $ x _ {1} \dots x _ {n} $, respectively, is defined by induction on the structure of the formula, as follows. (Here the free variables run through the set $ M $ and the predicate symbol $ \rho $ denotes the relation $ R $.)
Suppose that a formula $ \phi $ is given, as well as a finite sequence $ \overline{x}\; = ( x _ {1} \dots x _ {n} ) $ of variables containing all the free variables of $ \phi $; let $ | \phi ; \overline{x}\; | $ denote the set of all finite sequences $ ( a _ {1} \dots a _ {n} ) $ of elements of $ M $ at which $ \phi $ is true in $ ( M , R ) $. A set of the form $ | \phi ; \overline{x}\; | $ can be constructed inductively as follows (here it is assumed that the logical symbols in $ \phi $ are $ \wedge $, $ \neg $, $ \exists $):
$$ | \phi ; \overline{x}\; | = \ \{ {( a _ {1} \dots a _ {n} ) } : { ( a _ {i} , a _ {j} ) \in R } \} $$
if $ \phi $ has the form $ \rho ( x _ {i} , x _ {j} ) $;
$$ | \phi _ {1} \wedge \phi _ {2} ; \overline{x}\; | = \ | \phi _ {1} ; \overline{x}\; | \cap \ | \phi _ {2} ; \overline{x}\; | ; $$
$$ | \neg \phi ; \overline{x}\; | = M ^ {n} \setminus | \phi ; \overline{x}\; | ; $$
$$ | \exists y \phi ; \overline{x}\; | = \mathop{\rm pr} _ {n+} 1 | \phi ; \overline{x}\; y | , $$
where $ \cap $, $ \setminus $, $ \mathop{\rm pr} _ {n+} 1 $ denote, respectively, intersection, difference and projection along the $ ( n+ 1 ) $- st coordinate (that is, the image with respect to the mapping $ ( a _ {1} \dots a _ {n} , a _ {n+} 1 ) \mapsto ( a _ {1} \dots a _ {n} ) $) of sets.
Identical truth for a formula $ \phi $ with free variables $ x _ {1} \dots x _ {n} $ then means that for any interpretation $ ( M , R ) $, every sequence $ ( a _ {1} \dots a _ {n} ) $ of elements of $ M $ belongs to the set $ | \phi ; x _ {1} \dots x _ {n} | $. For $ n = 0 $ the set $ | \phi ; \overline{x}\; | $ is either empty or a singleton. For example, the formula
$$ \exists y \forall x \rho ( x , y ) \supset \ \forall x \exists y \rho ( x , y ) $$
is an identical truth. The converse implication is not an identically-true formula.
In the case where an interpretation is fixed, a formula is sometimes called identically true if it is true in the given interpretation for any values of its free variables.
[1] | S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951) |
[2] | J.R. Shoenfield, "Mathematical logic" , Addison-Wesley (1967) |