Here denotes universal-existential sentences, with quantifier-free matrix and possibly empty blocks. Add constants for and considerWe show that is consistent. Suppose a finite subset is inconsistent. Combine its diagram facts as and its finitely many negative existential facts as . Replacing the new constants by a variable tuple gives the consequenceThis is equivalent to a universal-existential sentence: move all the existential blocks to the front of the disjunction, using the usual nonempty-domain convention. If there are no negative existential facts, the consequence is simply . By hypothesis satisfies the displayed consequence. Its named tuple satisfies but none of the existential alternatives, a contradiction.
Articles by others on the same topic
There are currently no matching articles.