A collection of logical connectives is functionally complete, or adequate, if every Boolean function of finitely many propositional variables is represented by a logical formula using only those logical connectives. More explicitly, for every and every there is a logical formula whose truth value under each Boolean valuation is . Constant functions with Boolean values may use an otherwise irrelevant logical variable, for example for truth and for falsity.
Translate logical formulas recursively, leaving propositional variables unchanged and translating negation by applying negation to the translation. For the other two logical connectives set
The first logical implication is false exactly when both original inputs are false; the second displayed logical formula is true exactly when both inputs are true. Hence each clause preserves truth values. Structural induction gives for every Boolean valuation and every logical formula in the larger language.
By the assumed functional completeness of negation, logical conjunction and logical disjunction, any finite Boolean function has such a logical formula . Its translation uses only negation and logical implication and represents the same function. Thus is adequate.
Under any Boolean valuation there are two possibilities. If is false, the outer logical implication is true by vacuous truth. If it is true, then is false, which forces true and false. In that case is true, so the outer logical implication is again true. These possibilities exhaust the truth values of its antecedent; therefore
There is a three-line Hilbert formal proof. Use A1 with , ; then use A3 with , :
This is a direct logical derivation in the displayed Hilbert proof system. Neither the deduction theorem for propositional logic nor a completeness theorem for propositional logic is needed: the desired logical implication is just the contrapositive, supplied by A3, of the particular A1 instance on line 1.
Yes, for soundness and completeness of theoremhood. An axiom-only complete propositional calculus is obtained as follows. Declare every propositional tautology, and only such a tautology, to be an axiom; supply no inference rules. A formal proof then consists of a single axiom. Every proved logical formula is valid, giving soundness, and every valid logical formula is already an axiom, giving completeness.
This is not merely an unspecified collection: whether a finite propositional formula is a tautology is decidable by its finite truth table, so the axiom set can be recognized effectively. It is a deliberately uninformative Hilbert proof system, since all the work has been put into axiom recognition. If one instead asked for strong completeness of derivations from arbitrary additional assumptions, a system whose only formal proof lines are axioms or assumptions would not suffice; the affirmative construction here concerns versus .

Articles by others on the same topic (0)

There are currently no matching articles.