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

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.

## migrated from cstheory.stackexchange.comSep 6 '18 at 20:54

This question came from our site for theoretical computer scientists and researchers in related fields.

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).

• I'll add (since this came over from CS and OP may want the connection) that the problem of recognizing non-tautologies is pretty famous in the study of computational complexity: it's called SAT (or is equivalent to it, anyway). – spaceisdarkgreen Sep 7 '18 at 1:07
• I'm intrigued by your final comment: in what sense do we expect co-NP complete problems like recognising tautologies to be "worse" than NP-complete problems? – Rob Arthan Sep 7 '18 at 15:27
• @RobArthan: If NP$\neq$coNP (which is unknown but generally expected), then the complement of an NP-complete problem is not in NP at all. It may be that I'm stretching it a bit by calling that "even worse", though. – Henning Makholm Sep 7 '18 at 15:41

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)