Smullyan's Unifying Principle

Smullyan's Unifying Principle states that every (sufficiently pure) member of an abstract consistency class has a frugal model. An abstract consistency class is a class of sets of sentences satisfying certain properties. These properties vary according to the particular logical system of interest, but the idea is always to ensure that an "abstract consistent" set can be extended in reasonable ways. Obviously, Smullyan's Unifying Principle implies an abstract consistency class is a subclass of the class of all satisfiable sets of sentences.

In the context of first-order logic, an abstract consistency class Gamma is a class of sets of sentences S satisfying six conditions:

1. If A is atomic, then A is not in S or -A is not in S.

2. If --A is in S, then S union {A} is in Gamma.

3. If "A or B" is in S, then S union {A} is in Gamma or S union {B} is in Gamma.

4. If "-[A or B]" is in S, then S union {-A,-B} is in Gamma.

5. If "forall x A" is in S, then S union {A[t/x]} is in Gamma.

6. If "exists x A" is in S and c is any constant which does not occur in S, then S union {A[c/x]} is in Gamma.

Andrews uses Smullyan's Unifying Principle in the context of first-order logic to prove completeness. He also uses it to prove a sequent calculus G is equivalent to his first order system F. Other applications show that Semantic Tableaus and Resolution provide complete refutation procedures. The principle can also be used to show the Craig-Lyndon Interpolation Theorem.

Andrews also uses Smullyan's Unifying Principle in the context of Elementary Type Theory to prove a cut-free sequent formulation is equivalent to a (Hilbert-style) axiomatic formulation. He also uses it to show that if a formula is provable in elementary type theory, then its negation is refutable in a certain resolution-style system.