Logic, formal
Logic, formal
Investigates the structure of propositions and of deductive reasoning by a method which abstracts from the content of propositions which come under consideration and deals only with their logical form. The distinction between form and content can be made definite with the aid of a particular language or symbolism in which propositions are expressed, and the formal method can then be characterized by the fact that it deals with the objective form of sentences which express propositions and provides in these concrete terms criteria of meaningfulness and validity of inference. This formulation of the matter presupposes the selection of a particular language which is to be regarded as logically exact and free from the ambiguities and irregularities of structure which appear in English (or other languages of everyday use) — i.e., it makes the distinction between form and content relative to the choice of a language. Many logicians prefer to postulate an abstract form for propositions themselves, and to characterize the logical exactness of a language by the uniformity with which the concrete form of its sentences reproduces or parallels the form of the propositions which they express. At all events it is practically necessary to introduce a special logical language, or symbolic notation, more exact than ordinary English usage, if topics beyond the most elementary are to be dealt with (see logistic system, and semiotic).
Concerning the distinction between form and content see further the articles formal, and syntax, logical.
1. THE PROPOSITIONAL CALCULUS formalizes the use of the sentential connectives and, or, not, if . . . then. Various systems of notation are current, of which we here adopt a particular one for purposes of exposition. We use juxtaposition to denote conjunction (“pq” to mean “p and q”), the sign ? to denote inclusive disjunction (“p ? q” to mean (“p or q or both”), the sign + to denote exclusive disiunction (“p + q” to mean “p or q but not both”), the sign ~ to denote negation (“~p” to mean “not p”), the sign ? to denote the conditional (“p ? q” to mean “if p then q,” or “not both p and not-q”), the sign = to denote the biconditional (“p = q” to mean “p if and only if q,” or “either p and q or not-p and not-q”), and the sign | to denote alternative denial (“p | q” to mean “not both p and q”). — The word or is ambiguous in ordinary English usage between inclusive disjunction and exclusive disjunction, and distinct notations are accordingly provided for the two meanings of the word, The notations “p ? q” and “p = q” are sometimes read as “p implies q” and “p is equivalent to q” respectively. These readings must, however, be used with caution, since the terms implication and equivalence are often used in a sense which involves some relationship between the logical forms of the propositions (or the sentences) which they connect, whereas the validity of p ? q and of p = q requires no such relationship. The connective ? is also said to stand for “material implication,” distinguished from formal implication ( 3 below) and strict implication (q. v.). Similarly the connective = is said to stand for “material equivalence.”
It is possible in various ways to define some of the sentential connectives named above in terms of others. In particular, if the sign of alternative denial is taken as primitive, all the other connectives can be defined in terms of this one. Also, if the signs of negation and inclusive disjunction are taken as primitive, all the others can be defined in terms of these; likewise if the signs of negation and conjunction are taken as primitive. Here, however, for reasons of naturalness and symmetry, we prefer to take as primitive the three connectives, denoting negation, conjunction, and inclusive disjunction. The remaining ones are then defined as follows
A | B ? ~A ? ~B.
A ? B ? ~A ? B.
A = B ? [B ? A][A ? B].
A + B ? [~B]A ? [~A]B.
The capital roman letters here denote arbitrary formulas of the propositional calculus (in the technical sense defined below) and the arrow is to be read “stands for” or “is an abbreviation for.” Suppose that we have given some specific list of propositional symbols, which may be infinite in number, and to which we shall refer as the fundamental propositional symbols. These are not necessarily single letters or characters, but may be expressions taken from any language or system of notation; they may denote particular propositions, or they may contain variables and denote ambiguously any proposition of a certain form or class. Certain restrictions are also necessary upon the way in which the fundamental propositional symbols can contain square brackets [ ]; for the present purpose it will suffice to suppose that they do not contain square brackets at all, although they may contain parentheses or other kinds of brackets. We call formulas of the propositional calculus (relative to the given list of fundamental propositional symbols) all the expressions determined by the four following rules
all the fundamental propositional symbols are formulas
if A is a formula, ~[A] is a formula;
if A and B are formulas [A][B] is a formula;
if A and B are formulas [A] ? [B] is a formula.
The formulas of the propositional calculus as thus defined will in general contain more brackets than are necessary for clarity or freedom from ambiguity; in practice we omit superfluous brackets and regard the shortened expressions as abbreviations for the full formulas. It will be noted also that, if A and B are formulas, we regard [A] | [B], [A] ? [B], [A] = [B], and [A] + [B], not as formulas, but as abbreviations for certain formulas in accordance with the above given definitions.
In order to complete the setting up of the propositional calculus as a logistic system (q. v.) it is necessary to state primitive formulas and primitive rules of inference. Of the many possible ways of doing this we select the following.
If A, B, C are any formulas, each of the seven following formulas is a primitive formula
[A ? A] ? A.
A ? [B ? AB].
A ? [A ? B].
AB ? A.
[A ? B] ? [B ? A].
AB ? B.
[A ? B] ? [[C ? A] ? [C ? B]].
(The complete list of primitive formulas is thus infinite, but there are just seven possible forms of primitive formulas as above.) There is one primitive rule of inference, as followsGiven A and A ? B to infer B. This is the inference known as modus ponens (see below, 2).
The theorems of the propositional calculus are the formulas which can be derived from the primitive formulas by a succession of applications of the primitive rule of inference. In other words,
the primitive formulas are theorems, and
if A and A ? B are theorems then B is a theorem.
An inference from premisses A1, A2, . . . , An to a conclusion B is a valid inference of the propositional calculus if B becomes a theorem upon adding A1, A2, . . . , An to the list of primitive formulas. In other words,
the inference from A1, A2, . . . , An to B is a valid inference if B is either a primitive formula or one of the formulas A1, A2, . . . , An, and
if the inference from A1, A2, . . . , An to C and the inference from A1, A2, . . . , An to C ? B are both valid inferences then the inference from A1, A2, . . . , An to B is a valid inference.
It can be proved that the inference from A1, A2, . . . , An to B is a valid inference of the propositional calculus if (obviously), and only if (the deduction theorem), [A1 ? [A2 ? . . . [An ? B] . . . ]] is a theorem of the propositional calculus.
The reader should distinguish between theorems about the propositional calculus — the deduction theorem, the principles of duality (below), etc. — and theorems of the propositional calculus in the sense just defined. It is convenient to use such words as theorem, premiss, conclusion both for propositions (in whatever language expressed) and for formulas representing propositions in some fixed system or calculus.
In the foregoing the list of fundamental propositional symbols has been left unspecified. A case of special importance is the case that the fundamental propositional symbols are an infinite list of variables, p, q, r, . . ., which may be taken as representing ambiguously any proposition whatever — or any proposition of a certain class fixed in advance (the class should be closed under the operations of negation, conjunction, and inclusive disjunction). In this case we speak of the pure propositional calculus, and refer to the other cases as applied propositional calculus (although the application may be to something as abstract in character as the pure propositional calculus itself, as, e.g., in the case of the pure functional calculus of first order (3), which contains an applied propositional calculus).
In formulating the pure propositional calculus the primitive formulas may (if desired) be reduced to a finite number, e.g., to the seven listed above with A, B, C taken to be the particular variables p, q, r. A second primitive rule of inference, the rule of substitution is then required, allowing the inference from a formula A to the formula obtained from A by substituting a formula B for a particular variable in A (the same formula B must be substituted for all occurrences of that variable in A). The definition of a theorem is then given in the same way as before, allowing for the additional primitive rule, the definition of a valid inference must, however, be modified.
In what follows (to the end of 1) we shall, for convenience of statement, confine attention to the case of the pure propositional calculus. Similar statements hold, with minor modifications, for the general case.
The formulation which we have given provides a means of proving theorems of the propositional calculus, the proof consisting of an explicit finite sequence of formulas, the last of which is the theorem proved, and each of which is either a primitive formula or inferable from preceding formulas by a single application of the rule of inference (or one of the rules of inference, if the alternative formulation of the pure propositional calculus employing the rule of substitution is adopted). The test whether a given finite sequence of formulas is a proof of the last formula of the sequence is effective — we have the means of always determining of a given formula whether it is a primitive formula, and the means of always determining of a given formula whether it is inferable from a given finite list of formulas by a single application of modus ponens (or substitution). Indeed our formulation would not be satisfactory otherwise. For in the contrary case a proof would not necessarily carry conviction, the proposer of a proof could fairly be asked to give a proof that it was a proof — in short the formal analysis of what constitutes a proof (in the sense of a cogent demonstration) would be incomplete.
However, the test whether a given formula is a theorem, by the criterion that it is a theorem if a proof of it exists, is not effective — since failure to find a proof upon search might mean lack of ingenuity rather than non-existence of a proof. The problem to give an effective test by means of which it can always be determined whether a given formula is a theorem is the decision problem, of the propositional calculus. This problem can be solved either by the process of reduction of a formula to disjunctive normal form, or by the truth-table decision procedure. We state the latter in detail.
The three primitive connectives (and consequently all connectives definable from them) denote truth-functions — i.e., the truth-value (truth or falsehood) of each of the propositions &min;p, pq, and p ? q is uniquely determined by the truth-values of p and q. In fact,
&min;p is true if p is false and false if p is true;
pq is true if p and q are both true, false otherwise;
p ? q is false if p and q are both false, true otherwise.
Thus, given a formula of the (pure) propositional calculus and an assignment of a truth-value to each of the variables appearing, we can reckon out by a mechanical process the truth-value to be assigned to the entire formula. If, for all possible assignments of truth-values to the variables appearing, the calculated truth-value corresponding to the entire formula is truth, the formula is said to be a tautology.The test whether a formula is a tautology is effective, since in any particular case the total number of different assignments of truth-values to the variables is finite, and the calculation of the truth-value corresponding to the entire formula can be carried out separately for each possible assignment of truth-values to the variables.
Now it is readily verified that all the primitive formulas are tautologies, and that for the rule of modus ponens (and the rule of substitution) the property holds that if the premisses of the inference are tautologies the conclusion must be a tautology. It follows that every theorem of the propositional calculus is a tautology. By a more difficult argument it can be shown also that every tautology is a theorem. Hence the test whether a formula is a tautology provides a solution of the decision problem of the propositional calculus.
As corollaries of this we have proofs of the consistency of the propositional calculus (if A is any formula, A and ~A cannot both be tautologies and hence cannot both be theorems) and of the completeness of the propositional calculus (it can be shown that if any formula not already a theorem, and hence not a tautology, is added to the list of primitive formulas, the calculus becomes inconsistent on the basis of the two rules, substitution and modus ponens).
As another corollary of this, or otherwise, we obtain also the following theorem about the propositional calculus
If A = B is a theorem, and D is the result of replacing a particular occurrence of A by B in the formula C, then the inference from C to D is a valid inference.
The dual of a formula C of the propositional calculus is obtained by interchanging conjunction and disjunction throughout the formula, i.e., by replacing AB everywhere by A ? B, and A ? B by AB. Thus, e.g., the dual of the formula ~[pq ? ~r] is the formula ~[[p ? q] ~r]. In forming the dual of a formula which is expressed with the aid of the defined connectives, |, ?, =, +, it is convenient to remember that the effect of interchanging conjunction and (inclusive) disjunction is to replace A|B by ~A~B, to replace A ? B by ~A B; and to interchange = and +.
It can be shown that the following principles of duality hold in the propositional calculus (where A* and B* denote the duals of the formulas A and B respectively)
if A is a theorem, then ~A* is a theorem;
if A ? B is a theorem, then B* ? A* is a theorem;
if A = B is a theorem, then A* = B* is a theorem.
Special names have been given to certain particular theorems and forms of valid inference of the propositional calculus. Besides 2 following, see
absorption;
affirmation of the consequent;
assertion;
associative law;
commutative law;
composition;
contradiction, law of;
De Morgan’s laws;
denial of the antecedent;
distributive law;
double negation, law of;
excluded middle, law of;
exportation;
Hauber’s law;
identity, law of;
importation;
Peirce’s law;
proof by cases;
reductio ad absurdum;
reflexivity;
tautology;
transitivity;
transposition.
Names given to particular theorems of the propositional calculus are usually thought of as applying to laws embodied in the theorems rather than to the theorems as formulas; hence, in particular, the same name is applied to theorems differing only by alphabetical changes of the variables appearing; and frequently the name used for a theorem is used also for one or more forms of valid inference associated with the theorem. Similar remarks apply to names given to particular theorems of the functional calculus of first order, etc.
Whitehead and Russell,
Princibia Mathematica. 2nd edn., vol. 1. Cambridge. England, 1925.
E. L. Post,
Introduction to a general theory of elementary propositions, American Journal of Mathematics, vol. 43 (1921), pp. 163-181.
W. V. Quine,
Elementary Logic, Boston and New York. 1941.
I. Herbrand,
Recherches sur la Theorie de la Demonstration, Warsaw, 1930.
Hilbert and Ackermann,
Grundzuge der theoretischen Logik, 2nd edn., Berlin, 1938.
Hilbert and Bernays,
Grundlagen der Mathematik, vol. 1, Berlin, 1934; also Supplement III to vol. 2. Berlin. 1939.