Adequacy here means functional completeness: every Boolean truth function of finitely many positive-arity propositional inputs can be expressed by a formula using the available connectives. It is an expressive-power claim, distinct from the completeness theorem relating derivability and semantic entailment.
Negation and implication define conjunction and disjunction byGiven any truth table, for each input row where its output is true form the minterm containing each input positively or negatively according to that row. The disjunction of these minterms is true on exactly the required rows: a disjunctive normal form. Replacing its conjunctions and disjunctions by the displayed definitions gives a formula using only .
The constantly true and constantly false functions are represented by and , using a dummy input if needed. Thus the empty or full truth table also causes no difficulty. If one insists on genuinely nullary formulas with no variables at all, a separate truth constant is needed; ordinary propositional adequacy allows the constant truth functions to be expressed with irrelevant input variables.
There are sixteen binary Boolean functions, one for each four-bit truth table. Exactly eight give an adequate basis together with negation.
The eight affine functions are . Each is affine over the field with two elements, and composition with other affine functions or negation remains affine. Since conjunction is not affine, none of these eight bases is adequate.
Each remaining truth table has either one true row or three true rows. In the latter case negate its output to obtain a function with one true row. Negate selected inputs to move that row to : the resulting function is conjunction. Conjunction together with negation expresses every disjunctive normal form, proving adequacy of all remaining eight. They are AND, NAND, OR, NOR, the two directed implications, and the two asymmetric conjunctions , . The count treats the binary connective by its truth function rather than by arbitrary choices of its printed symbol.
A graph must assign exactly one output to every input, while the distinguished unary predicate must select exactly one element. Suitable sentences areThe existential clauses provide totality and nonemptiness of the selected output, respectively; the universal clauses provide uniqueness. Thus a structure satisfying uniquely determines a total unary function and a constant on its unchanged domain. Conversely any interpretations of determine such relations by and .
For each term define an -formula expressing its value. Use fresh bound variables at every step:Freshness includes avoiding all relevant free variables of the formula being translated. Define the atomic translation byand extend through the logical operations: , , and . Fresh witnesses prevent variable capture and ensure the translation preserves the original free-variable set.
For an -structure , let have the graph relation of and singleton relation . Induction on terms proves that holds precisely when is the value of . Induction on formulas then provesConversely every -structure satisfying is uniquely the relational version of an -structure on that same domain. Hence, for arbitrary possibly infinite , semantic entailment on the left is equivalent to semantic entailment from on the right, with assignments retained in the free-formula case. Applying soundness theorem for first-order logic and Gödel's completeness theorem givesThe prohibition on completeness in the preceding direct equality question is local to that proof; here it supplies the clean semantic-to-syntactic transfer after the actual translation and model correspondence have been established.
Replace each -ary function symbol by an -ary graph predicate, with axioms asserting exactly one output for each input tuple. Replace each constant by a unary predicate asserted to hold of exactly one element. Recursively introduce witnesses for term values, then translate formulas through their logical connectives and quantifiers as above.
Every original structure has a unique corresponding relational structure satisfying these axioms, on exactly the same carrier, and every such relational structure reconstructs the original functions and constants. Truth under assignments and logical consequences are preserved in both directions. In this precise relative sense, purely relational languages are adequate to represent first-order languages with functions and constants: expressive power is retained after adjoining the graph and uniqueness axioms. Arbitrary relational interpretations that fail those axioms are not claimed to represent functions.
Neither constants alone nor functions alone gives the same uniform adequacy on all nonempty carriers. A one-element set has exactly one interpretation of each function symbol of any finite arity and of every constant symbol. In contrast it has two interpretations of a unary predicate: empty or full. Thus a fixed purely functional or constant-only language has only one structure on that singleton, and cannot encode both truth values of by a same-carrier truth-preserving translation with reconstruction. This is the singleton truth-preservation obstruction to expressive completeness, even when logical equality is available.
Constants alone also cannot represent general variable-dependent relations on larger infinite carriers: a fixed formula mentions only finitely many named elements, and its remaining equality tests do not encode an arbitrary binary relation. Functions offer more flexibility. On carriers with at least two elements, predicates can be encoded by characteristic functions taking two distinguished values, and constants can be represented by constant-valued unary functions if explicit constant symbols are forbidden. Such a construction can work after adding axioms for distinct truth markers, but those axioms exclude the singleton case. Enlarging the carrier or adding a Boolean sort is another possible encoding; it changes the same-carrier sense established in the preceding part and must not be silently identified with it.
Articles by others on the same topic
There are currently no matching articles.