nLab
tautology

Idea

In boolean propositional logic, a tautology is any proposition whose validity is unconditional — independent of the validity of its propositional variables. Several generalizations are possible. On the one hand, the family of boolean tautolgies is also the family of boolean theorems: a proposition is a boolean tautology iff it has a boolean proof. On the other hand, construing a boolean proposition as a universalized equation in the language of boolean algebras, the boolean propositions are also the (universal, first-order) propositions of the form $P(x_1,...,x_n)=\top$ that are valid in every boolean algebra.

Of course, tautologies exist in other logics besides boolean logic, although boolean logic is perhaps the simplest nontrivial case.

Definition

Given a logic, a context $\Gamma$ within that logic, and a class of models of $\Gamma$, a tautology is a proposition $\varphi$ in $\Gamma$ that is true in all models; that is,

$$ℳ\models \varphi$$\mathcal{M} \vDash \phi

for every model $ℳ$.

Discussion

Compare the notion of theorem, sometimes called a syntactic tautology, which asks that $\varphi$ be provable in $\Gamma$:

$$\Gamma ⊢\varphi .$$\Gamma \vdash \phi .

In the best behaved cases, each context has a free model? such that the theorems are precisely the tautologies for the free model. (For example, in the case of boolean propositional logic, the free model for the context with $n$ variables is the free boolean algebra on $n$ generators.) Even without this, there may be a class of models that can be proved to be sound? (every theorem is a tautology) and complete? (every tautology is a theorem).