  The fundamental proposal in this article is that logical formulas of the form
(f <-> ~f) are not contradictions, and that formulas of the form (t <-> t) are
not tautologies. Such formulas, wherever they appear in mathematics, are
instead reason to conclude that f and t have a third truth value, different
from true and false. These formulas are circular definitions of f and t. We can
interpret the implication formula (f <-> ~f) as a rule, a procedure, to find
the truth value of f on the left side: we just need to find the truth value of
f on the right side. When we use the rules to ask if f and t are true or false,
we need to keep asking if they are true or false over and over, forever.
  Russell's paradox and the liar paradox have the form (f <-> ~f). The truth
value provides a straightforward means of avoiding contradictions in these
problems. One broad consequence is that the technique of proof by contradiction
involving formulas of the form (f <-> ~f) becomes invalid. One such proof by
contradiction is one form of proof that the halting problem is uncomputable.
The truth value also appears in Cantor's diagonal argument, Berry's paradox,
and the Grelling-Nelson paradox.
