 where the positive sentences are those built without using negation \((\neg)\). Since (7) is satisfiable in a totally interpreted language, the first-order theory containing the sentences of (7) as axioms must be consistent. This should be contrasted with Tarski’s theorem stating that the unrestricted \(T\)-schema is inconsistent. If the unrestricted comprehension principle is similarly restricted to the positive formulae, we also get a consistent theory. This was originally shown by Gilmore (1974).