Add a predicate symbol for each -formula , of arity equal to its displayed free-variable tuple. Let consist of together with all defining axiomsEvery first-order model of has a unique such expansion, interpreting the new predicate symbols by their defining sets. Conversely the reduct of every first-order model of satisfies .
Given an arbitrary -formula , replace each new atomic predicate symbol by its original -definition, renaming bound variables to avoid capture. This produces an -formula withThe defining axiom for that particular logical formula now gives an atomic replacement:Thus the expanded first-order theory eliminates quantifiers. For a first-order sentence, the same translation is an -sentence, decided by completeness of ; hence every expanded first-order sentence is decided and is complete. Empty free-variable tuples can be handled by zero-ary predicate symbols, or by the usual logical truth and falsity constants. This definitional expansion is called Morleyization.
Articles by others on the same topic
There are currently no matching articles.