Why is the set of all tautologies in propositional logic recursively enumerable?

Question

I've just started reading an english edition of Gems of Theoretical Computer Science. On page 5 (or page 12 of the overall pdf), the author brings up the set of all tautologies in propositional logic as an example of a set that is recursively/computably enumerable.

Could anyone explain why this is the case? If anything, it seems to me that complement of this set should be recursively enumerable, since you only need one counter-example to show that a formula isn't a tautology.

Answer 1

The syntactic notion of "tautology" is precisely the propositions for which there exists a formal proof without any hypotheses. So enumerating them is a simple application of a basic pattern in the relation between computability and logic:

• For every string of symbols $S$
  • If the contents of $S$ have the format of a formal proof
    • If the proof has no hypotheses, output the conclusion of the proof

The semantic notion of "tautology" is precisely the propositions for which plugging in truth values always produces a true result. So there is another straightforward algorithm for enumerating these:

• For every string of symbols $S$
  • If the contents of $S$ have the format of a proposition
    • Loop over every way to assign a truth value to the variables of $S$
      • Compute the value of $S$ obtained by plugging in these truth values
    • If every value of $S$ was true
      • Output $S$

Incidentally, there is a theorem of logic that syntactic tautologies are the same thing as semantic tautologies, so both of these algorithms enumerate the same propositions. (albeit in different order and with different multiplicity)

Answer 2

You're right that the complement of the set is also recursively enumerable.

This means that the set itself ought to be decidable. And indeed you can decide if a propositional formula is a tautology simply by filling out a full truth table and checking whether the results in all lines is "true". Since there can only be finitely many lines in the truth table, this algorithm always terminates.

(It is a rather slow algorithm, but that doesn't matter. In fact recognizing non-tautologies is NP-complete, and recognizing tautologies is expected to be even worse).