2.

GROUNDWORK - THE PROPOSITIONAL CALCULUS

Building blocks

OUR first task will be to set down a propositional calculus -- or, more accurately, to set down some propositional calculi. Many systems discussed later will be presented as extensions of the propositional calculus, and in almost all we do we may expect to be referring quite often to the systems discussed in this chapter. As remarked earlier, our notation is that of Łukasiewicz with primitive binary operators

forming well-formed formulas in the pattern Cjy

where j and y are themselves wf. As is usual, we read the above operators respectively as the signs of implication, conjunction, and alternation. We shall also employ the primitive unary operator

Ν

-- the sign of negation -- forming well-formed formulas in the pattern Nj

where j is wf. These are all the primitive connectives introduced in this chapter; later on, however, we shall employ others. We now define another commonly used propositional connective by noting that we shall use

Ejy

as an abbreviation for ΚCjyCyj.

Ε is, of course, the sign of equivalence.

Our basic or 'atomic' wffs will be the propositional variables

p, q, r, . . .

of which we assume there are always as many as we need.

Implicational systems - positive implication

Basis. In all of what follows, we take as postulated the rule of substitution for variables and the rule of detachment, which permits us to infer y from j and Cjy. The first system we examine consists of these rules of inference plus the axioms

Cl. CCpCqrCCpqCpr

C2. CpCqp.

These are, of course, formulas 1 and 2 of chapter 1. This system may be called the 'positive implicational calculus'; we shall commonly refer to it as 'ICI'. As a first proof in ICI, we reproduce some of the work of chapter 1; the leftmost column in the proof assigns a number to the formula listed in the centre column, and the right column justifies the proof line.

Deduction

In what follows, a variant of a formula j is any formula derivable from j by substituting variables only for the variables of j. Thus CrCsr is a variant of C2. Given a set of wffs j₁, . . ., j_n (of ICI or of one of its extensions which we shall discuss later) we say that the wff y is deducible from this set provided there is a sequence of wffs y₁, . . ., y_m such that y = y_m and each of the y_i is either

1. One of the set j₁, . . ., j_n, or
2. Α variant of an axiom of the system in question, or
3. Inferred from two previous members of the sequence y₁, . . ., y_m by the rule of detachment, or
4. Inferred from a previous member of that sequence by the rule of substitution, provided the variable substituted for occurs in none of the j₁, . . ., j_n.

The set of formulas j₁, . . ., j_n will be called the 'hypotheses', and the sequence y₁, . . ., y_m will be called a 'deduction of y' from these hypotheses. Α deduction in which the set of hypotheses is null may be called simply a 'proof'. We will use

j₁, . . ., j_n y

to mean that y is deducible from the hypotheses j₁, . . ., j_n. We now state and prove a key metatheorem of ICI and its extensions: the deduction theorem.

*2.1	If j1, . . ., jn y, then j1, . . ., j(n-1) Cjny.

The proof is by induction on the length of the deduction of y (that is, on the number m in y); if this deduction is just one step long, y can only be either one of the hypotheses or a variant of an axiom. If it is the hypothesis j_n, the formula Cj_ny is Cj_nj_n; by 2.2 we see that there is a proof in ICI for this formula; it is thus deducible from any set of hypotheses. If y is one of the other hypotheses,  Cj_ny is of form Cj_nj_i, 1 £ i £ n; axiom C2 shows that the formula Cj_iCj_nj_i is deducible from any set of hypotheses. Since j_i is one of the j₁, . . ., j_(n-1), by detachment we have Cj_nj_i, which is Cj_ny, deducible from this set of n-1 hypotheses. Α similar argument applies in case y is a variant of an axiom; here both CyCj_ny and y itself are deducible from any set of hypotheses; clearly, then, so too will be Cj_ny.

We now assume that the deduction theorem holds whenever the deduction of y from the η hypotheses is of length k or shorter. If a deduction is of length k + 1, y, which is the (k + 1)th step, might be one of the hypotheses or a variant of an axiom, in which case the arguments of the preceding paragraph apply. It might also be the result of a detachment, by clause 3 of the definition of deduction; in this case, there are two formulas, c and Ccy, preceding y in the deduction and so by the induction hypothesis both

j₁, . . ., j_(n-1) Cj_nCcy

and

j₁, . . ., j_(n-1) Cj_nc

hold. But then with an appropriate variant of Cl, proper substitutions, and two detachments, we have Cj_ny deducible from the n - 1 hypotheses. If y -- the (k+1)th formula in the deduction results from a substitution in a previous formula χ of the deduction, then again we have Cj_nc deducible from the n-1 hypotheses by the induction hypothesis; the same substitution which changed χ into y will change Cj_nc into Cj_ny -- provided, of course, the variable substituted for does not occur in j_n. By the proviso on clause 4 of the definition of deduction, this last condition holds. We have thus proved the deduction theorem.

It should be immediately obvious that so far as ICI itself is concerned, clause 2 in the definition of deduction is redundant. For deductions corresponding to

2.3

CpCqr, Cpq, p r

and

2.4

p, q  p

may easily be constructed with the use only of clauses 1 and 3 of that definition. With applications of the deduction theorem, 2.3 eventually yields Cl and 2.4 gives C2; any substitution instance of either of these axioms may be similarly proved. Thus the deduction theorem plus the rule of detachment is equivalent to the system ICI, making clause 2, and indeed clause 4 of the definition of deduction redundant, so far as the system ICI is concerned. But we retain these clauses in this definition, for they become necessary for the use of the deduction theorem in the extensions of ICI formed by adding new axioms to this system of positive implication.

Some ICI theses

We use the terms 'thesis' and 'theorem' interchangeably here; either refers to a formula deducible from the null set of hypotheses, that is, to a formula provable within the system in question. Many important 'pure implicational' theses (those whose only connective is C) are provable in ICI; in the manner of Whitehead and Russell 1910 we attach names to the more important of these. With our notion of 'application' of one assertion to another, we note that each thesis may be thought of as being implicitly an operation upon other theses of the system; by its application to another thesis, the operation is made explicit. The implicit operation is sometimes suggested by the name attached to a formula: the formula called 'comm' below, for example, permits the commutation of certain subformulas of a given thesis. Axioms C1 and C2 may be referred to as 'Frege' (C1 was used as an axiom in Frege 1879) and 'simp' (for simplification) respectively.

The semisubstitutivity of implication

Another important metatheorem of ICI is one which may be considered a generalization of the property of implication implicit in syl and weak syl above. This metatheorem will, by the way, be expanded to cover the various extensions of ICI that we shall encounter. Before we state this metatheorem, however, we must discuss the terminology we shall use in expressing it. In the formula Cjy, j is referred to as the antecedent, and y as the consequent of the formula. We now extend the notions of antecedent and consequent to cover all the wf subformula occurrences of a pure implicational formula. Some of the wf subformula occurrences of an ICI wff will be said to be in 'antecedental position' - 'A-pos' for short - while the remainder of such formulas will be in 'consequential position', abbreviated 'C-pos'. Α-pos and C-pos are defined relative to the whole formula of which the subformula occurrences are a part. The first clause of our definition considers the whole formula as a subformula of itself

We now cover the cases in which the subformula occurrence in question is actually the antecedent or the consequent of the whole formula

The definition is now extended recursively to cover all ICI wffs

Although we used seven clauses to define A-pos and C-pos for ICI, in practice one learns to identify subformulas as being in one or the other of these positions almost at a glance. Any wf subformula of an ICI wff may now be classified as being in A-pos or in C-pos in the formula of which it is a part. We may now state the basic principle of semisubstitutivity of implication (SSI)

a is a subformula of j; as such it will stand in the scope of α certain number of the C's belonging to j; b, of course, will stand in the scope of precisely the same C's in y. Let n be the number of such C's. Suppose first of all that n = 0; in this case, a = j and b = y, and so by clause 1 of the definition of Α- and C-pos, a is in C-pos in j. But then CCabCjy (the correct form for C-pos) is really CCabCab, an ICI thesis by 2.2.

We now assume that whenever n = k, the principle of SSI holds. Let n = k + 1; j will then be of form Cgd, and we must consider the four following cases of the possible location of a in j:

(a) a in C-pos in g

(b) a in A-pos in g 

(c) a in C-pos in d

(d) a in A-pos in d. 

Let g' and d' be, respectively, the formulas just like g and δ except for having an occurrence of b where the latter formulas have a. We consider case (a) above; by the induction hypothesis, CCabCgg' (since α is in the scope of precisely k of the C's of g). By syl (2.11) we have CCgg'CCg'dCgd; but then we may move immediately to CCabCyj (the above substitution instance of syl is, of course, CCgg'Cyj). By clauses 2 and 6 of the definition of position a is in A-pos in j, and so SSI holds for case (a).

In case (b) by the induction hypothesis CCabCg'g. By syl we have CCg'gCCgdCg'd as α thesis; again by the transitivity of C implicit in syl, we go directly to CCabCjy. This is the proper form for this case, since by clauses 2 and 7 a is in C-pos in j.

In case (c) the induction hypothesis gives CCabCdd'. By weak syl (2.8) we have as α thesis CCdd'CCgdCgd', and so we get CCabCjy, which is the proper form for case (c) since by clauses 3 and 4 a is in C-pos in j.

Finally, in case (d) we have CCabCd'd by the induction hypothesis. Weak syl again gives us CCd'dCCgd'Cgd; thus do we have CCabCyj, the proper form for this case, since by clauses 3 and 5 a is in Α-pos in j.

Weaker versions of SSI follow as immediate corollaries; with a, b, j, and y as in *2.2, we have

Equivalently, we have

*2.4	Let a be in C-pos in j; if both Cab and j, then y; let a be in A-pos in j; if both Cab and y, then j, then j.

This last version of SSI gives us permission to replace α subformula in A-pos by any formula implying it and a subformula in C-pos by any formula it implies, salva veritate.

Also following SSI as immediate corollaries are the various versions of substitutivity of the biconditional (as stated here for pure implicational systems); with the Greek letters again as in *2.2, we have

*2.5	CCabCbaCjy
*2.6	If both Cab and Cba, then Cjy
*2.7	If Cab, Cba, and j, then y.

Classical implication

ICI is the pure implicational fragment of the intuitionist propositional calculus (IC); it contains all and only the IC theses whose only connective is C (this might be easily established using the systems and methods of chapter 3). If the intuitionist calculus IC is extended to the full classical (two-valued) propositional calculus PC, pure implicational theses become provable which are not IC theorems; typical of  these is 'Peirce's law' or, for short, just 'Peirce' (used in the propositional calculus of Peirce 1885)

C3. CCCpqpp.

If Peirce is added to ICI, the result is the system of full classical implication. We call this system PCI; all and only the pure implicational theses of the classical PC are provable in PCI (Wajsberg 1936).

In this and the following chapters, when we are dealing with a system which is an extension of an already discussed system, we shall often simply refer to that subsystem in justifying proof lines; thus, if a formula is clearly a thesis of ICI, we shall simply write ICI as justification; similarly for an inference clearly permissible in ICI.

Note that the second p from the right in 2.20 is in an Α-pos; since PCI contains ICI, it also contains the principle of SSI, and so 

The above-mentioned occurrence of p has been replaced by CCpqp, which implies p in PCI by C3.

Note that formula 2.23 asserts α certain kind of commutativity of the formula CCpqq (this is only in PCI, of course).

Conjunction

The implicational systems discussed in the last section will serve as bases for most of the systems we shall discuss. We are now ready for our first extensions of ICI and PCI; these extensions will be systems admitting Κ, the sign of conjunction, as well as C as an operator. Three new axioms will be involved:

Κ1. CpCgKpq 

Κ2. CKpqp 

Κ3. CKpqq. 

The addition of Κ1-K3 to ICI yields α system which we may call 'the C-Κ fragment of positive logic', and which we will designate 'ICK'. These axioms may also be added to the classical system PCI; in this case they yield the C-Κ fragment of classical logic, or ΡCΚ. Among the theorems provable in ICK (and so in PCK) are the following.

Formula 2.26 asserts the commutativity of Κ.

Formulas 2.30 and 2.31 are the basis for the extension of the principle of SSI to ICK and PCK. To do this we must first add clauses to the definition of position to cover cases in which the relevant subformula is in the scope of conjunction signs; we continue the numbering started in the section on implication

It should be clear that with formulas 2.30 and 2.31 the induction step in the proof of *2.2 may be extended to cover the cases in which the (k+1)th connective is a Κ; details are left to the reader. This permits us to state that

We continue with the proof of conjunction theses.

Note that there is actually a double application of *2.5 here, with some implicit ICI steps; the formula corresponding to y in *2.5 has had two occurrences of q replaced by p.

ICI, especially the formula comm, is used on 2.36 to bring the two underlined p's together at the start of the formula, where one of them is 'removed' by an application of Hilbert (2.18). The remaining p is then shuffled back to the position where it stands underlined in 2.37. 2.37 is α formula which can serve as an alternative axiom to Κ1 for the systems ICK and PCK.

The combined theses of importation and exportation exhibit an important relationship between implication and conjunction. Since we have α definition of Ε, the sign of equivalence (biconditional) stated in chapter 1, we may combine 2.40 and 2.45 thus

We may also restate the metatheorems on SBC (*2.5-*2.7) if we wish, replacing the pairs of implicational hypotheses Cab and Cba in *2.6 and *2.7 by the simple Eab and using importation to move from the CCabCCbaCjy of *2.5 to CEabCjy and CEabCyj and thus, through 2.37, to CEabEjy. The conclusion of *2.6, Cjy, may similarly be altered to Ejy

The converse of 2.51 also holds in ICK; its proof involves a 'decomposition-recomposition' procedure similar to that of 2.47-2.52, We leave the details to the reader and state that formula

The last two formulas enable us to state another equivalence; we also state two others derivable from previously proved formulas 

The full positive logic

We now add to the systems ICK and PCK our final primitive binary connective and the set of axioms governing it. The connective is Α, the 'sign of alternation,' and the axioms added are the following 

Α1. CpApq

Α2. CqApq

Α3. CCprCCqrCApqr.

We shall call the system formed by adding these axioms to ICK the 'full positive logic', or ICA, and that formed by adding them to PCK the 'C-Κ-A fragment of classical logic', or PCA.

We now work with the C-Α fragment of ICA, that is, with axiom,. Cl, C2, and Al-A3.

The procedure for proving 2.63 is a 'decomposition-recomposition' method analogous to that for proving the associativity of Κ; prod of the converse of 2.63 is similar. We shall state that converse leaving details to the reader.

As might be expected, the last two formulas are used in the proof of SSI for our thus-far extended systems. We extend the definition of Α- and C-pos to the present systems, retaining the original clause numbering:

Again, the induction step in the proof of SSI may be extended to cover contexts involving Α by the use of 2.69 and 2.70; details left to reader. We state

We now state another thesis to which we shall be referring:

Given the full system ICA, a number of the implications we have proved may be stated as equivalences

Certain other theses of interest are also provable in ICA 

Formula 2.79 is 'one direction' of the distributive law of alternation into conjunction. Going the other way

Thus do we have in positive logic

which shows alternation to 'distribute into' conjunction. Proof of the distributive law of conjunction into alternation 

is similar to that of 2.86, and will be left as an exercise for the reader.

Classical C-Κ-A; the redundancy of Α

If we add the axioms Al-A3 to the classical system PCK, we obtain the C-Κ-A fragment of classical logic, PCA. It is here that the classical logic begins very noticeably to differ from the intuitionist. In the intuitionist logic, none of the connectives C, Κ, Α, N is definable in terms of any combination of the others (McKinsey 1939). In the classical system, this is not the case. We see this first in the relationship of Α and C in the system PCA. (Recall that PCA differs from ICA in containing the additional axiom C3, CCCpqpp.)

In the following formula 

CCCpqrr

the underlined p is in an Α-pos; the formula 

is then an ICI theorem by SSI (*2.2)

The theoremhood of 2.91 in the classical system is quite significant, for with it, its converse 2.71, and the principle of SSI, the formulas Αjy and CCjyy are interchangeable in all contexts; Α is then expressible in terms of C. We sum up 2.91 and its converse in 

With 2.92 holding, formula 2.16 becomes axiom Α1; axiom C2 with q / Cpq, p / q becomes axiom Α2. Now note that the p in the formula 

CCqrCCCpqqr

is in Α-ροs; then

is an ICI theorem by SSI (*2.2). Since in PCI we have 2.24, 

In the presence of 2.92, 2.94 is axiom Α3. We see then that for the classical system the postulation of the equivalence 2.92 is equivalent to the postulation of axioms Al-A3. Indeed, it is common practice to set down the classical PC using only one of C, Κ, and Α as a primitive binary operator, and introducing the other two by 'definitions'; the definition of Α in α system having C primitive might well be 'Αjy is defined as CCjyy'; this definition would be, in effect, a postulation of formula 2.92.

Negation: the full system IC

We expand the system ICA of positive logic to the full intuitionist propositional calculus (IC) by adding as α primitive sign the unary operator Ν (the sign of negation) and axioms governing Ν; Ν, of course, forms wffs in the pattern Nj where j is wf. The axioms we shall employ for Ν are

Ν1. CCpNpNp (reductio ad absurdum)

Ν2. CNpCpq (ex falso quodlibet)

The addition of Ν1 and Ν2 to the classical PCA gives the full classical PC. In IC, now, we have

This last formula is the basis for the extension of the principle of SSI to the full calculi IC and PC; we add a final clause to the definition of position for ordinary propositional calculi

we shall then state

Details left to reader.

We treat this last formula just as we did 2.95:

This formula could replace Ν1 as an axiom of IC.

Instead of taking Ν as primitive, we might have taken a constant false proposition as primitive, and then defined Ν in terms of it. Let Æ be this constant false proposition; Nj is then defined by CjÆ. In this case, the only axiom we need add to ICA to get IC is

Æ1. CÆp.

We continue deductions in IC with Ν1 and Ν2 as axioms.

By 2.104 we see that any odd-numbered string of negation signs will be equivalent to one and any even-numbered string to two negation signs in IC.

Relationships between IC connectives

In the proofs to follow, we shall place the theses proved into two colors; formulas in black will be those we are primarily concerned with, while those in grey are intermediate steps. Many of the implications below are equivalences in the classical system; the first group of theses below will involve the relationship between implication and the other connectives. Each of the formulas involved, such as ANpq, CNNpq, or NKpNq, is classically equivalent to the implication Cpq; in IC, however, these equivalences do not hold, in spite of the fact that the formulas in question resemble implication in many ways. Because of this resemblance, we may refer to such formulas as 'quasi-implications'; the following are some theorems relating implication and some quasi-implications.

Note that the sequences of formulas 2.111, 2.114, 2.128, 2.111 and 2.118, 2.119, 2.128, 2.118 are self-returning chains of implications; each of these formulas may then be written as an equivalence rather than as an implication, and so NKpNq, NNCpq, CNNpNNq, and CpNNq are thus equivalent quasi-implications of q by p, even in IC. We turn now to the relationship between Κ and some quasi-conjunctions.

An examination of formulas 2.134, 2.141, 2.144, 2.147, and 2.151 shows again the self-returning chain of implications; thus the initial C in each of these formulas may be replaced by an Ε, and NCpNq, NANpNq, NNKpq, and KNNpNNq are equivalent quasi-conjunctions. Based on the definition of Ε, we may then state the following:

Let us do D(2.101)(D(D(2.11)(2.129))(2.132)); this yields

This last thesis is 'one direction' of one of 'De Morgan's laws'; the converse of 2.154 is α classical thesis, but-does not hold in IC.

This last formula is the other one of De Morgan's laws; here 'both directions' hold in IC.

We now work with alternation and some of the quasi-alternations of IC

Thus Apq implies CCpqq, which implies CNpq, which implies NKNpNq.

Classical negation: the full system PC

The full system PC is formed by adding Ν as α primitive symbol and the axioms Ν1 and Ν2 to the C-Κ-A system PCA. Alternatively, it may be formulated by adding the constant false proposition Æ as primitive rather than Ν, defining Ν as indicated previously, and adding the single axiom CÆp. Certain C-Ν formulas are very characteristic classical theses

Another typical classical thesis is

the law of 'excluded middle'.

We now quickly examine the relationships between the connectives in PC

The last formula completes the returning chain of quasi-implications from the weakest to the strongest, ANpq. This means that ANpq, CNNpq, Cpq, NKpNq, NNCpq, CNNpNNq, and CpNNq are all classically equivalent.

Formula 2.176 closes the chain of implications for quasi-conjunctions, making Kpq, KNNpq, NCpNq, NANpNq, NNKpq, and KNNpNNq all classically equivalent.

And 2.177 closes the implication chain for quasi-alternations, making Apq, CCpqq, CNpq, and NKNpNq all classically equivalent. It should now be simple for the reader to supply a proof for the converse of 2.154, resulting in the theoremhood classically of the first mentioned of De Morgan's laws

Alternative bases for PC

As the previous section indicated, if we have Ν plus one of the connectives C, Κ, Α, the other two of the binary connectives become redundant in PC in the sense that Α is redundant in the C-Κ-A fragment of PC. This means that PC may be formulated with Ν and one of C, Κ, Α as its only primitive operators, all other operators being defined in terms of the pair of primitives (there are, of course, other 'functionally complete' sets of primitive operators for PC than those discussed here; it is not, however, our purpose to go into α detailed examination of them). Also, as has been indicated, if C is taken as primitive we may make use of a primitive constant false proposition rather than Ν and then define Ν (and so all the other connectives) in terms of it and C. For reference in the chapters that follow, we shall be interested in C-N, C-Æ, and Κ-Ν formulations of PC. Definitions will be as follows (Ε is defined as before in all systems)

In C-Ν primitive systems,

Κjy is defined as NCjNy

Ajy is defined as CCjyy (alternatively as CNjy). In C-Æ primitive systems,

Nj is defined as CjÆ

all other definitions as in C-Ν-primitive. In Κ-Ν primitive systems, Cjy is defined as ΝΚjΝy, while  Ajy is defined as ΝΚNjΝy. Rules of inference will be substitution and detachment, and the set of axioms we shall take as standard for C-Ν primitive PC are those of Łukasiewicz,

CN1. CCpqCCqrCpr (= 2.11, syl)

CN2. CpCNpq (= D(2.15)(Ν2))

CN3. CCNppp (= 2.166, Clavius)

As α C-Æ primitive base, we might take axioms C1, C2, and C3 plus axiom Æ1, CÆp; α simpler system is available by replacing C1 by 2.11, syl Formulas. 2.11 + C2 + C3 are the Tarski-Bernays basis for pure classical implication.

The axioms for our Κ-Ν primitive system will be those of Rosser 1953:

ΚΝ1. CpΚpp (= 2.27)

ΚΝ2. CKpqp (= Κ2)

ΚΝ3. CCpqCNKqrNKrp.

Proof of the equivalence of each of these systems to PC is left as an exercise for the reader.

As is well known, PC in any of these formulations is such that a formula is a PC theorem iff it is also a tautology, is truth functionally valid. We do not here enter into a proof of this completeness result; many sources are available for the reader wishing to see such a proof. We suggest, for example, Church 1956 or Rosser 1953.