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


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.

2.1 CCpqCpp D(Cl)(C2)
2.2 Cpp D(2.1)(C2)


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 j1, . . ., jn (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 y1, . . ., ym such that y = ym and each of the yi is either

  1. One of the set j1, . . ., jn, or
  2. Α variant of an axiom of the system in question, or
  3. Inferred from two previous members of the sequence y1, . . ., ym 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 j1, . . ., jn.

The set of formulas j1, . . ., jn will be called the 'hypotheses', and the sequence y1, . . ., ym 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

j1, . . ., jn y

to mean that y is deducible from the hypotheses j1, . . ., jn. 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 jn, the formula Cjny is Cjnjn; 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,  Cjny is of form Cjnji, 1 i n; axiom C2 shows that the formula CjiCjnji is deducible from any set of hypotheses. Since ji is one of the j1, . . ., j(n-1), by detachment we have Cjnji, which is Cjny, deducible from this set of n-1 hypotheses. Α similar argument applies in case y is a variant of an axiom; here both CyCjny and y itself are deducible from any set of hypotheses; clearly, then, so too will be Cjny.

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

j1, . . ., j(n-1) CjnCcy


j1, . . ., j(n-1) Cjnc

hold. But then with an appropriate variant of Cl, proper substitutions, and two detachments, we have Cjny 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 Cjnc deducible from the n-1 hypotheses by the induction hypothesis; the same substitution which changed χ into y will change Cjnc into Cjny -- provided, of course, the variable substituted for does not occur in jn. 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


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.

2.5 CsCCpCqrCCpqCpr D(C2)(Cl)
2.6 CCsCpCqrCsCCpqCpr D(C1)(2.5)
2.7 CCqrCpCqr C2, p / Cqr, q / p
2.8 (weak syl) CCqrCCpqCpr D(2.6)(2.7)
2.9 C CCqrCpqCCqrCpr D(C1)(2.8)
2.10 CCpqCCqrCpq C2. p / Cpq, q / Cqr
2.11 (syl) CCpqCCqrCpr D(D(2.8)(2.9))(2.10)
2.12 (syl-simp) CCCpqrCqr D(2.11)(C2)
2.13 CCCCqrCprsCCpqs D(2.11)(2.11)
2.14 (syn) CCpCqrCCsqCpCsr D(2.13)(2.13)
2.15 (comm) CCpCqrCqCpr D(D(2.14)(C1))(C2)
2.16 (modus ponens) CpCCpqq D(2.15)(2.2)
2.17 CCpqCCpCqrCpr D(2.15)(C1)
2.18 (Hilbert) CCpCpqCpq D(2.17)(2.2)

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

1. Every wff j of ICI is in C-pos in itself.

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

2. j is in A-pos in Cjy.
3. y is in C-pos in Cjy.

The definition is now extended recursively to cover all ICI wffs

4. If j is in C-pos in y, and y is in C-pos in c, then j is in C-pos in c.
5. If j is in Α-ροs in y, and y is in C-pos in c, then j is in A-pos in c.
6. If j is in C-ροs in y, and y is in A-pos in c, then j is in A-pos in c.
7. If j is in Α-ροs in y, and y is in A-pos in c, then j is in C-pos in c.

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)


Let the wff y be like j except for having an occurrence of the wf subformula b where j has a. Then

if a is in C-pos in j, CCabCjy;

if a is in A-pos in j, CCabCyj.

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


Let Cab; then

if a is in C-pos in j Cjy

if a is in A-pos in j, Cyj.

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.

2.19 CCCpqqCCqpCCpqp ICI (syl)
2.20 CCqpCCCqppp 2.16, p / Cqp, q / p

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 

2.21 CCqpCCCqpCCpqpp 2.20, C3, SSI (*2.4)

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

2.22 CCCqpCCpqpCCqpp D(2.15)(2.21)
2.23 CCCpqqCCqpp 2.22, 2.19, ICI (by syl)
2.24 CCqpCCCpqqp D(2.15)(2.23)

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


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.

2.25 CKqpCKqpKpq Κ3, Κ2, Κ1, ICI
2.26 CKqpKpq D(2.18)(2.25

Formula 2.26 asserts the commutativity of Κ.

2.27 CpKpp D(2.18)(Κ1)
2.28 CCpgCpCrKqr D(2.8)(Κ1)
2.29 CCpqCKprCKprKqr 2.28, Κ2, Κ3, ICI
2.30 CCpqCKprKqr D(D(2.11)(2.29))(2.18)
2.31 CCpqCKrpKrq 2.30, 2.26, ICI

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

8. j is in C-pos in Kjy.
9. y is in C-pos in Kjy.

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

*2.8 The principles of semisubstitutivity of implication and substitutivity of the biconditional as stated in *2.2-*2.7 hold in the systems ICK and PCK.

We continue with the proof of conjunction theses.

2.32 CCqrCKqqKqr 2.31, p / q, q / r, r / q
2.32a CCqrCqKqr p / q, SSI (*2.4)
2.33 CCqpCCpqCCCqrCqKqrCCprCpKqr SBC (*2.5)

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.

2.34 CCCqrCqKqrCCqpCCpqCCprCpKqr 2.33, ICI (comm)
2.35 CCqpCCpqCCprCpKqr D(2.34)(2.32a)
2.36 CpCCpgCCprCpKqr D(2.12)(2.35)
2.37 CCpqCCprCpKqr 2.36, ICI (comm, Hilbert)

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.

2.38 CCpCqrCpCqr ICI
2.39 CCpCqrCKpqCKpqr 2.38, Κ2, Κ3, SSI
2.40 (importation) CCpCqrCKpqr 2.39, ICI (comm, Hilbert)
2.41 CCrsCCpCqrCpCqs SSI (*2.2)
2.42 CCpCqrCCrsCpCqs ICI (comm), 2.41
2.43 CKpqCCKpqrr  2.16, p / Kpq, q / r
2.44 CpCqCCKpqrr D(D(2.42)(Κ1))(2.43)
2.45 CCKpqrCpCqr 2.44, ICI (comm)

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

2.46 ECpCqrCKpqr 2.40, 2.45, Κ1, Df. Ε

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

2.47 CKpKqrp Κ2, q / Kqr
2.48 CKpKqrKqr Κ3, q / Kqr
2.49 CKpKqrq D(D(2.11)(2.48))(Κ2)
2.50 CKpKqrr D(D(2.11)(2.48))(Κ3)
2.51 CKpKqrKpq D(D(2.37)(2.47))(2.49)
2.52 (associativity) CKpKqrKKpqr D(D(2.37)(2.51))(2.50)

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

2.53 (associativity) CKKpqrKpKqr

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

2.54 (associativity) CKpKqrKKpqr 2.52, 2.53, Κ1, Df. Ε 
2.55 (commutativity) EKpgKqp 2.26, Κ1, Df. Ε
2.56 ΕpΚpp 2.27, Κ2, Κ1, Df. Ε 

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.

2.57 CAppp D(D(Α3)(2.2))(2.2)
2.58 (commutativity) CApqAqp D(D(Α3)(Α2))(Α1)
2.59 CApqAApqr  Α1, p / Αpq, q / r
2.60 CpAApqr D(D(2.11)(Α1))(2.59)
2.61 CqAApqr D(D(2.11)(Α2))(2.59)
2.62 CAqrAApqr D(D(Α3)(2.61))(Α2)
2.63 (associativity) CApAqrAApqr D(D(Α3)(2.60))(2.62)

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.

2.64 (associativity) CAApqrApAqr
2.65 CCsqCsAqr D(2.8)(Α1)
2.66 CpCCpqAqr D(D(2.11)(2.16))(2.65)
2.67 CrCsAqr D(2.15)(D(C2)(Α2))
2.68 CAprCCpqAqr D(D(Α3)(2.66))(2.67)
2.69 CCpqCAprAqr D(2.15)(2.68)
2.70 CCpqCArpArq 2.69, 2.58, ICI

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:

10. j is in C-pos in Ajy.
11. y is in C-pos in Ajy.

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

*2.9 The principles of SSI and SBC as stated in *2.2-*2.7 apply in the systems ICA and PCA.

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

2.71 CApqCCpqq D(2.15)(D(Α3)(2.2)), 2.58, SSI

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

2.72 ΕΑppp 2.57, Α1, ICK
2.73 (commutativity) EApqAqp 2.58, ICK
2.74 (associativity) EApAqrAApqr 2.63, 2.64, ICK

Certain other theses of interest are also provable in ICA 

2.75 CKqrApq D(D(2.11)(Κ2))(Α2)
2.76 CApKqrApq D(D(Α3)(Α1))(2.75)
2.77 CKqrApr D(D(2.11)(Κ3))(Α2)
2.78 CApKqrApr D(D(Α3)(Α1))(2.77)
2.79 CApKqrKApqApr D(D(2.37)(2.76))(2.78

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

2.80 CrCArqArKpq A1, ICI
2.81 CpCgArKpq Κ1, Α2, SSI
2.82 CpCrArKpq Α1, C2
2.83 CpCArqArKpq 2.81, 2.82, Α3, ICI
2.84 CArpCArqArKpq D(D(Α3)(2.80))(2.83)
2.85 CKApqAprApKqr 2.84 p / q, q / r, r / p, 2.46, SBC

Thus do we have in positive logic

2.86 EApKqrKApqApr  2.79, 2.85, ICK

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

2.87 EKpAqrAKpqKpr

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 


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

2.88 CCprCCCCrqrrCCCpqrr

is then an ICI theorem by SSI (*2.2)

2.89 CCprCCCpqrr D(D(2.15)(2.88))(C3)
2.90 ApCpq D(D(2.89)(Α1))(Α2)
2.91 CCCpqqApq D(D(2.15)(2.70))(2.90

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 

2.92 EApqCCpqq 2.71, 2.91, ICK

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 


is in Α-ροs; then

2.93 CCprCCCqrCCCrqqrCCqrCCCpqqr

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

2.94 CCprCCqrCCCpqqr D(D(2.15)(2.93))(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

2.95 CCpqCCqNpCpNp 2.11, r / Νp
2.96 CCpqCNqCpNp 2.95, Ν2, p / q, q / Νp, SSI 
2.97 (transposition)  CCpqCNqNp 2.96, Ν1, SSI (note: context here is C-pure)

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

12. j is in A-pos in Nj.

we shall then state

*2.10 The principles of SSI and SBC as expressed in *2.2-*2.7 hold in the full systems IC and PC.

Details left to reader.

2.98 CCpqCCpCqNpCpNp 2.17, r / Νp

We treat this last formula just as we did 2.95:

2.99 CCpqCCpNqNp 2.98, Ν1, Ν2, SSI

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. Cp.

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

2.100 CqCCpNqNp D(2.12)(2.99)
2.101 CCpNqCqNp D(2.15)(2.100)
2.102(weak double negation) CpNN D(2.101) (2.2)
2.103 CNNNpNp D(2.97)(2.102)
2.104 ΕΝρΝΝΝρ 2.102, 2.103

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.

2.105 CNpCNNpq D(2.15)(Ν2); p / Νp
2.106 CANpqCNNpq D(D(Α3)(2.105))(C2)
2.107 CCNNpqCpq D(2.11)(2.102)
2.108 CpCNqNCpq D(D(2.11)(2.16))(2.97)
2.109 CKpNqNCpq 2.108, ICK
2.110 CCpqNKpNq D(2.101)(2.109)
2.111 CNNCpqNKpNq D(2.97)(2.109)
2.112 CpCNqKpNq Κ1, q / Nq
2.113 CpCNKpNqNNq D(D(2.11)(2.112)) (2.97)
2.114 CNKpqCpNNq D(2.15)(2.113)
2.115 CCpCqrCqCNNpNNr 2.15, 2.97, ICI
2.116 CCpCqrCNNpCNNqNNNNr 2.115, 2.97, ICI
2.117 CCpCqrCNNpCNNqNNr 2.116, 2.103, SSI
2.118 CNNCpqCNNpNNq D(2.117)(2.2)
2.119 CCNNpNNqCpNNq 2.107, q / NNq
2.120 CCpCqrCCpCrsCpCq ICI
2.121 CCpCqrCCpNrCpNq 2.120, Ν1, Ν2, SSI
2.122 CNCpqNNp D(2.97)(Ν2)
2.123 CCpNqCCNqNpCpNp 2.11, q / Nq, r / Νp
2.124 CCpNqCCNqNpNp 2.123, Ν1, SSI
2.125 CNCpqNq D(2.97)(C2)
2.126 CNCpqCCNqNpNp D(D(2.11)(2.125)(D(2.12)(2.124))
2.127 CNCpqNCNqNp D(D(2.120)(2.126))(2.122)
2.128 CCpNNqNNCpq 2.127, 2.101, ICI

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.

2.129 CKpqKNNpq 2.2. p / Kpq, 2.102, SSI
2.130 CCNNpNqNKNNpNNq 2.110, p / ΝΝp, q / Nq
2.131 CCpNqNKNNpq 2.130, 2.102, SSI
2.132 CKNNpqNCpNq D(2.101)(2.131)
2.133 CANpNqCpNq D(D(2.11)(2.106))(2.107) q / Nq
2.134 CNCpNqNANpNq D(2.97)(2.133)
2.135 CCNpNNpNNp Ν1, p / Np
2.136 CCNppNNp 2.135, 2.102, SSI
2.137 CCpqCCANpqrCpr 2.11, Α2, SSI
2.138 CCpqCNANpqNp 2.137, r / Np, Ν1, Ν2, SSI
2.139 CCpqCNANpqANpq 2.138, Α1, SSI
2.140 CCpqNNANpq D(D(2.11)(2.139))(2.136)
2.141 CNANpNqNCpNq D(2.101)(2.140), q / Nq
2.142 CpCNKpqNq D(D(2.11)(Κ1))(2.97)
2.143 CNKpqCpNq D(2.15)(2.142)
2.144 CNANpNqNNKpq 2.141, 2.143, SSI
2.145 CNNKpqNNp D(2.97)(D(2.97) (Κ2))
2.146 CNNKpqNNq D(2.97)(D(2.97)(Κ3))
2.147 CNNKpqKNNpNNq D(D(2.37)(2.145))(2.146)
2.148 CCpNqCNNpNq D(D(2.11)(2.101))(2.97)
2.149 CNNpCCpNqNq D(2.15)(2.148)
2.150 CNNpCNNqNCpNq D(D(2.11)(2.149))(2.97)
2.151 CKNNpNNqNCpNq D(2.40)(2.150)

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:

2.152 ENNEpgKNNCpqNNCqp

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

2.153 CCpNqNKpq
2.154 CANpNqNKpq D(D(2.11)(2.133))(2.153)

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.

2.155 CNApqNp D(2.97)(Α1)
2.156 CNApqNq D(2.97)(Α2)
2.157 CNApqKNpNq D(D(2.11)(Ν2))(D(2.15)(2.71))
2.158 CNpCApqq D(D(2.11)(2.158))(2.97)
2.159 CNpCNqNApq D(D(2.11)(2.158))(2.97)
2.160 CKNpNqNApq D(2.40)(2.159)
2.161 ENApqKNpNq 2.160, 2.157, ICK

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

2.162 CApqCCpqq (this is 2.71)
2.163 CCCpqqCCpqq ICI
2.164 CCCpqqCNpq 2.163, Ν2, SSI
2.165 CCNpqNKNpNq 2.110, p / Νp

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 Cp. Certain C-Ν formulas are very characteristic classical theses

2.166 (Clavius) CCNppp C3, Ν2, SSI
2.167 (strong double negation) CNNpp D(D(2.11)(Ν2))(2.166)
2.168 ΕpΝΝp 2.167, 2.102, ICK
2.169 CCNpNqCNNqNNp 2.97, p / Νρ, q / Nq
2.170 (strong trans) CCNpNqCqp 2.169, 2.168, SBC
2.171 CCNpNNqCNqp 2.170, q / Nq 
2.172 CCNpqCNqp 2.171, 2.102, SSI 

Another typical classical thesis is

2.173 ΑpΝp 2.90, Ν2, SSI

the law of 'excluded middle'.

We now quickly examine the relationships between the connectives in PC

2.174 CCpqANpq  D(D(2.11)(2.140))(2.167
2.175 CNNCpqANpq D(D(2.11)(2.167))(2.174

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.

2.176 CNNKpqKpq 2.167, p / Kpq

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

2.177 CNKNpNqApq D(2.172)(2.157

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

2.178 EANpNqNKpq 

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, Cp; α 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.