The rules that have just been stated would enable the first De Morgan law listed inClick Here to see full-size tableTable 3 to transform any wff containing any number of occurrences of · into an equivalent wff in which · does not appear at all, but in place of it certain complexes of ∼ and ∨ are used. Similarly, since ∼p ∨q has the sametruth table asp ⊃q, (p ⊃q) ≡ (∼p ∨q) is valid, and any wff containing ⊃ can therefore be transformed into an equivalent wff containing ∼ and ∨ but not ⊃. And, since (p ≡q) ≡ [(p ⊃q) · (q ⊃p)] is valid, any wff containing ≡ can be transformed into an equivalent containing ⊃ and · but not ≡, and thus in turn by the previous steps it can be further transformed into one containing ∼ and ∨ but neither ≡ nor ⊃ nor · . Thus, for every wff of PC there is an equivalent wff, expressing precisely the sametruth function, in which the only operators are ∼ and ∨, though the meaning of this wff will usually be much less clear than that of the original.

Analternative way of presenting PC, therefore, is to begin with the operators ∼ and ∨ only and to define the others in terms of these. The operators ∼ and ∨ are then said to beprimitive. If “=_Df” is used to mean “is defined as,” then the relevant definitions can be set down as follows:(α · β) =_Df ∼(∼α ∨ ∼β)
(α ⊃ β) =_Df (∼α ∨ β)
(α ≡ β) =_Df [(α ⊃ β) · (β ⊃ α)] in which α and β are any wffs of PC. These definitions are not themselves wffs of PC, nor is =_Df a symbol of PC; they are metalogical statements about PC, used to introduce the new symbols ·, ⊃, and ≡ into the system. If PC is regarded as a purely uninterpreted system, the expression on the left in a definition is simply a convenient abbreviation of the expression on the right. If, however, PC is thought of as having its standard interpretation, the meanings of ∼ and ∨ will first of all have beenstipulated by truth tables, and then the definitions will lay it down that the expression on the left is to be understood as having the same meaning (i.e., the same truth table) as the expression on the right. It is easy to check that the truth tables obtained in this way for ·, ⊃, and ≡ are precisely the ones that were originally stipulated for them.

An alternative to taking ∼ and ∨ as primitive is to take ∼ and · as primitive and to define (α ∨ β) as ∼(∼α · ∼β), to define (α ⊃ β) as ∼(α · ∼β), and to define (α ≡ β) as before.Yet another possibility is to take ∼ and ⊃ as primitive and to define (α ∨ β) as (∼α ⊃ β), (α · β) as ∼(α ⊃ ∼β), and (α ≡ β) as before. In each case, precisely the same wffs that were valid in the original presentation of the system are still valid.

Axiomatization of PC

The basic idea of constructing anaxiomatic system is that of choosing certain wffs (known asaxioms) as starting points and giving rules for deriving further wffs (known astheorems) from them. Such rules are calledtransformation rules. Sometimes the word “theorem” is used to cover axioms as well as theorems; the word “thesis” is also used for this purpose.

Anaxiomatic basis consists of

• 1.A list ofprimitive symbols, together with any definitions that may be thought convenient,
• 2.A set of formation rules, specifying which sequences of symbols are to count as wffs,
• 3.A list of wffs selected as axioms, and
• 4.A set of (one or more) transformation rules, which enable new wffs (theorems) to be obtained by performing certain specified operations on axioms or previously obtained theorems.

Definitions, where they occur, can function as additional transformation rules, to the effect that, if in anytheorem any expression of the form occurring on one side of a definition is replaced by the corresponding expression of the form occurring on the other side, the result is also to count as a theorem. Aproof or derivation of a wff α in anaxiomatic systemS is a sequence of wffs of which the last is α itself and each wff in the sequence is either an axiom ofS or is derived from some axiom(s) or some already-derived theorem(s) or both by one of the transformation rules ofS. A wff is a theorem ofS if and only if there is a proof of it inS.

Care is usually taken, in setting out an axiomatic basis, to avoid all reference tointerpretation. It must be possible to tell purely from the construction of a wff whether it is anaxiom or not. Moreover, the transformation rules must be so formulated that there is an effective way of telling whether any purported application of them is a correct application or not, and hence whether a purported proof of a theorem really is a proof or not. An axiomatic system will then be a purely formal structure, on which any one of a number of interpretations, or none at all, may be imposed without affecting the question of which wffs are theorems. Normally, however, an axiomatic system is constructed with a certain interpretation in mind; the transformation rules are so formulated that under that interpretation they are validity preserving (i.e., the results of applying them to valid wffs are always themselves valid wffs); and the chosen axioms either are valid wffs or are expressions of principles of which it is desired to explore the consequences.

Probably the best-known axiomatic system for PC is the following one, which, since it is derived fromPrincipia Mathematica (1910–13) byAlfred North Whitehead andBertrand Russell, is often calledPM:

• Primitive symbols: ∼, ∨, (,), and aninfinite set of variables,p,q,r, … (with or without numerical subscripts).
• Definitions of ·, ⊃, ≡ (see aboveInterdefinability of operators).
• Formation rules (see aboveFormation rules for PC), except that formation rule 3 can be abbreviated to “If α and β are wffs, (α ∨ β) is a wff,” since ·, ⊃, and ≡ are not primitive.
• Axioms:
• 1. (p ∨p) ⊃p
  2. q ⊃ (p ∨q)
  3. (p ∨q) ⊃ (q ∨p)
  4. (q ⊃r) ⊃ [(p ∨q) ⊃ (p ∨r)]

     Axiom 4 can be read, “Ifq impliesr, then, if eitherp orq, eitherp orr.”

• Transformation rules:

  1. The result of uniformly replacing any variable in a theorem by any wff is a theorem (rule of substitution).
  2. If α and (α ⊃ β) are theorems, then β is a theorem (rule of detachment, ormodus ponens).

Relative to a givencriterion of validity, an axiomatic system is sound if every theorem is valid, and it iscomplete (or, more specifically,weakly complete) if every valid wff is a theorem. The axiomatic system PM can be shown to be both sound and complete relative to the criterion of validity already given (see aboveValidity in PC).

An axiomatic system isconsistent if, whenever a wff α is a theorem, ∼α is not a theorem. (In terms of the standard interpretation, this means that no pair of theorems can ever bederived one of which is the negation of the other.) It isstrongly complete if the addition to it (as an extra axiom) of any wff whatever that is not already a theorem would make the system inconsistent. Finally, an axiom or transformation rule isindependent (in a given axiomatic system) if it cannot be derived from the remainder of the axiomatic basis (or—which comes to the same thing—if its omission from the basis would make the derivation of certain theorems impossible). It can, moreover, be shown that PM is consistent and strongly complete and that each of its axioms and transformation rules is independent.

A considerable number of otheraxiomatic bases for PC, each having all the above properties, are known. The task of proving that they have these properties belongs tometalogic.

In some standard expositions of formal logic, the place of axioms is taken byaxiom schemata, which, instead of presenting some particular wff as an axiom, lay it down that any wff of a certain form is an axiom. For example, in place of axiom 1 in PM, one might have the axiom schema “Every wff of the form (α ∨ α) ⊃ α is an axiom”;analogous schemata can besubstituted for the other axioms. The number of axioms would then become infinite, but, on the other hand, therule of substitution would no longer be needed, and modus ponens could be the only transformation rule. This method makes no difference to the theorems that can be derived, but, in some branches oflogic (though not in PC), it is simpler to work with axiom schemata rather than with particular axioms and substitution rules. Having aninfinite number of axioms causes no trouble provided that there is an effective way of telling whether a wff is an axiom or not.

Partial systems of PC

Various propositional calculi have been devised to express a narrower range of truth functions than those of PC as expounded above. Of these, the one that has been most fully studied is thepure implicational calculus (PIC), in which the only operator is ⊃, and the wffs are precisely those wffs of PC that can be built up from variables, ⊃, and brackets alone. Formation rules 2 and 3 (see aboveFormation rules for PC) are therefore replaced by the rule that if α and β are wffs, (α ⊃ β) is a wff. As in ordinary PC,p ⊃q is interpreted as “p materially impliesq”—i.e., as true except whenp is true butq false. The truth-table test of validity can then be straightforwardly applied to wffs of PIC.

The task ofaxiomatizing PIC is that of finding a set of valid wffs, preferably few in number and relatively simple in structure, from which all other valid wffs of the system can be derived by straightforward transformation rules. The best-known basis, which was formulated in 1930, has the transformation rules of substitution and modus ponens (as in PM) and the following axioms:

1. p ⊃ (q ⊃p)
2. [(p ⊃q) ⊃p] ⊃p
3. (p ⊃q) ⊃ [(q ⊃r) ⊃ (p ⊃r)]

Axioms 1 and 3 are closely related to axioms 2 and 4 of PM respectively (see aboveAxiomatization of PC). It can be shown that the basis is complete and that each axiom is independent.

Under the standard interpretation, the aboveaxioms can be thought of as expressing the following principles: (1) “If a propositionp is true, then if some arbitrary propositionq is true,p is (still) true.” (2) “If the fact that a certain propositionp implies some arbitrary propositionq implies thatp itself is true, thenp is (indeed) true.” (3) “If one proposition (p) implies a second (q), then if that second proposition implies a third (r), the first implies the third.” Thecompleteness of the basis is, however, a formal matter, not dependent on these or any other readings of the formulas.

An even more economical complete basis for PIC contains the sametransformation rules but the sole axiom[(p ⊃q) ⊃r] ⊃ [(r ⊃p) ⊃ (s ⊃p)]. It has been proved that this is the shortest possible single axiom that will give a complete basis for PIC with these transformation rules.

Since PIC contains no negation sign, the previous account of consistency is not significantly applicable to it. Alternative accounts of consistency have, however, been proposed, according to which a system is consistent (1) if no wff consisting of a single variable is a theorem or (2) if not every wff is a theorem. The bases stated are consistent in these senses.