Loop Invariants as Tautologies Would it be correct to characterize loop invariants as a type of tautology?  I ask since the invariant must basically always be true, before the loop starts, before each iteration and after the loop terminates.  I realize that there is the possibility that the invariant could become false during the body of the loop.  But since inside the loop "doesn't count" is it fair to characterize the invariant as a tautology?
A Tautology is a formula (in a certain logic) that is true under every model of that logic. That is, it is equivalent to the formula "$True$".

A loop invariant, however, is a certain claim that is usually true under some models, and false under others (a model in this case is an algorithm). Then, you prove that the invariant is true under your specific model.

If you add axioms to your logic that forces then only model to be the one of your specific program, then indeed this would be a tautology. But such a process (adding axioms and proving that something is a tautology), is what is more commonly known as "proof". (For clarification: even if you add enough axioms, you may not be able to prove your claim, even if it's a tautology, in case of incomplete systems).

For example, consider a loop that increases a variable $i$ by $1$. An invariant of the loop may be that if before the loop $i&gt;0$, then after the loop $i&gt;0$. Indeed, this loop satisfies it. But it is not a tautology, since we can come up with other loops that do not satisfy it.