AXIOMATISATION OF THE PROPOSITIONAL CALCULUS
IN C AND
.
1
A.N. Prior
and R.P. Kerr
By ‘the propositionl clculus in C n
’ is ment tht form of propositionl
clculus in which the only unefine symols re the propositionl vriles ‘p’, ‘q’, ‘r’, etc.,
the universal quantifier
‘
′
n the symol of impliction ‘C’
.
This has been called
by
Russell, in (1),
1
the ‘theory of
impl
ication.
’
In
Ł
ukasiewicz
n Trski’
s (2)
2
it is stated that
any set of axioms which, with the rules of substitution and detatchment, is sufficient for that
sement of the propositionl clculus which employs no opertor ut ‘C’ (e.. the Trski

Berna
ys axioms
CCpqCCqrCpr, CCCpqpp and CpCqp) will become sufficient for the full
calculus in C and
if we the followin two rules of inference (‘x’ ein vrile of
any kind)
RT1.
From
C
,
we may infer C
x
,
provided that x does not occur freely in
.
RT2.
From C
x
, we may infer
C
.
This result is credited to Tarski, but we have been unable to find any published proof of it. In
wht follows, we shll show tht Trski’s result cn e prove if certin o
ther result can be
proved, and we shall sketch the proof of this other result.
In a number of co
mparatively recent writings of
Ł
ukasie
wi
cz
, e.g. (3),
the following
two rules for the introduction of the universal quantifier
–
{2}
–
have been
employed:
–
1.
From
C
, we may infer C
x
2.
From
C
, we may infer
C
x
,
provie tht ‘x’ oes not occur freely in
.
2
and RT1 above are identical;
1 is not identical with RT2.
But if
1, with substitution
and deta
chment, is employed in any system
containing the theses
Cpp
and CCpqCCqrCpr,
RT2 may b
e obtained as a derivative rule; for
C
will always be obtainable from
C
x
as
follows:
–
1.
C
x
2.
Cpp
3.
CCpqCCqrCpr
2
p/
X
1
= 4.
4.
C
x
3
p/
, q/
x
, r/
= C1
–
C4
–
5
5.
C
1
This text has been edited by Max
Cresswell and Adriane Rini. The original is kept in
the
Prior collection
, box 5
at
the
Bodleian Library, Oxford.
[Eitors’ note: footnotes 1 n 2,
indicated by superscripts in the text are
amalgamated at the foot of page 1. The text at the
foot of tht pe res: “1, 2. For our informtion s to the contents of these two ppers, we
re inete to rofessor A. Church.”
and conversely, if RT2, with substitution and detachment, is employed in any system
containing the same two theses,
1
may be obtained as a derivative rule,
for
C
x
will
always be obtainable from
C
as follows:
–
1.
C
2.
Cpp
3.
CCpqCCqrCpr
2
p/
x
= 4
4.
C
x
x
4 X RT2 = 5
–
{3}
–
5.
C
x
3 p/
x
,
q/
, r/
= C5
–
C1
–
6
6.
C
x
.
Hence if the rules
1
and
2
will give a sufficient basis for the calculus in C and
if
adjoined to the rules of substitution and detachment, with axioms sufficient for the calculus in
C, the same will be true of the rules RT1 and RT2. (For Cpp and CCpqCCqrCpr are valid
formulae of the calculus in C).
Rule
1
above, adjoined to the pure
ly implicational calculus will suffice to prove all
valid formulae in C and
in which
occurs only as forming the proposition
pp.
For (i) if
1
be applied to the implicational thesis Cpp, we obtain C
ppp;
(ii) if ‘0’ e use s n
revition for ‘
pp’, this lw C
ppp will become C0p; and (iii)
Wajsberg has shown in
(4) that
if we introduce into propositional calculus a constant false proposition 0, a sufficient
basis for the calculus in C and 0 may be obtained by adjoining C0p to any set of axioms
s
ufficient for the calculus in C.
There are, however, other ways in which
may occur in theses of the C
–
calculus:
e.g. the way in which it occurs in the thesis C
pCpqq.
If, however, within
the C
–
system
formed by adjoining the rules
1
and
2
to th
e calculus in C, it can be shown that all
formulae in which
occurs in any way are deductively equivalent to formulae in which it
occurs only in forming the proposition
pp,
this system can be considered complete. We do
not propose here to prove this dedu
ctive equivalence, but we shall indicate where the proof
can in effect be found.
–
{4}
–
In (5), C.A. Mereith evelops system which uses not only ‘C’, ‘
’ n
propositionl vriles, ut lso the ‘functoril’ vrile ‘
’, so use tht
may represent
any truth

function of which
is an argument.
He shows tht where ‘0’ is n revition for
‘
pp’,
‘N
’ for ‘C
0’, ‘1’ for ‘N0’ n
‘K
’
for ‘
NC
N
’,
the following theses are
prov
able by substitution and det
achment from the single axiom C
Π
pp
p:
–
8.
Cpp
9.
CCpqCCprCpKqr
10.
C
K
0
1
p.
He then (p. 44) uses these, with
1 and
2, to show that fo
r any truth

function
q,
q
q
impli
es and is implied by K
0
1. In the present paper we are
concerned not with a C


system but a C

one; ut Mereith’s proof will o for this lso, if trnspose little. Of his
premises 1

3, the first two contain no functorial variables, and so are provable in Wajsber
g
’s
C

0 clculus (with ‘N
’
efine s ‘
C
0’ n ‘
K
’ s ‘
NC
N
’, n conse
quently
in that
part of the C

calculus with may be regar
d
e s n interprettion of Wjser’s.
3,
CK
0
1
p, thouh it cnnot e trete s n ctul thesis within Wjser’s clculus, cn e
treated as a metalogical abbreviation for a whole class of C

0 theses.
Thus regarded, it asserts
tht within Wjser’s clculus we my prove ny formul which consists of ‘C’, followe
y ‘K’, followe y ny truth

function of ‘0’, followe y the sme truth

function of ‘1’,
followed by the same truth

function of ‘p’.
An in this sense it is prove in Quine’
s (6); or
more accurately, Quine there proves the {5}
metalogical counterpart of C
0C
1
p, from
which that of CK
0
1
p follows easily by importation.
Mereith’
s proof of C
q
qK
0
1
and CK
0
1
q
q
may then be subjected to a similar re

interpretation.
It remains to show that in the C
–
system, if for any
and
–
e.
g. any formulae of
the forms
q
q and K
0
1
–
we
have both C
and C
as theses, we may replace either by
the other in any formula
and obtain a formula which implies and is implied by the original
one.
In the C
—
system the only
way
s
in which a formula
may be built into a larger
formula are (i) by its being the
antecedent of an implication C
or the
consequent of an
implication C
, or (ii) by its being preceded by a universal quantifier, i.e. b
y its occurring in
a formula
x
, where ‘x’ is ny propositionl vrile; or (iii) y some succession of these
procedures.
From any set of axioms sufficient for the calculus in C we may der
ive the theses
CCpqCCqrCpr and CCqrCCpqCpr
; and by means of these, and
1 and
2, we can always
derive from the theses C
and C
the furthe
r theses CC
C
, CC
C
, CC
C
,
CC
C
, C
x
x
and C
x
x
, as follows:
–
1.
C
2.
C
3.
CCpqCCqrCpr
4.
CCqrCCpqCpr
3 p/
, q/
, r/
= C2
–
5.
5.
CC
C
3 p/
, q/
, r/
= C1
–
6.
–
{6}
–
6.
CC
C
4 p/
, q/
, r/
= C1
–
7
7.
CC
C
4
p/
, q/
, r/
= C2
–
8
8.
CC
C
1
X
1 X
2 = 9
9.
C
x
x
2 X
1 X
2 = 10
10.
C
x
x
Canterbury University College, Christchurch, New Zealand.
REFERENCES
.
(1)
RUSSELL, B.A.W.,
The Theory of Implication
, Amer. Jour. Math. Vol. 28 (1906), pp.
152

202.
(2)
Ł
UKASIEWICZ, JAN and TARSKI, ALFRED,
Untersuchungen
ü
ber
den
Aussagenkalkul
, Comptes Rendus dea S
é
ances
de la
Soci
é
t
é
des Sciences et des Lettres
de
Varsovie, class III, Vol. 23
(1930), pp. 30

50.
(3)
Ł
UKA
S
IEWICZ, JAN,
Aristotle’s Sylloistic from the Stnpoint of Moern Forml
Logic
, Oxford, London and New York 1951.
(4)
WAJSBERG, M.,
Metalogische Beitrage
, Wiadomosci Matematyczne, Vol. 43 (1937),
pp. 131

168.
(5)
MEREDITH, C.A.,
On an Extended System of Propositional Calculus
, Proceedings of
the Royal Irish Academy 54 A 3 (1951).
(6)
QUINE, W.V.,
Completeness of the Propositional Calculus
, JSL, III (1938), pp. 37

40.