AXIOMATISATION OF THE PROPOSITIONAL CALCULUS
IN C AND
ï
.
1
A.N. Prior
and R.P. Kerr
By âthe propositionï¡l cï¡lculus in C ï¡nï¤
ï
â is meï¡nt thï¡t form of propositionï¡l
cï¡lculus in which the only unï¤efineï¤ symï¢ols ï¡re the propositionï¡l vï¡riï¡ï¢les âpâ, âqâ, ârâ, etc.,
the universal quantifier
â
ï
â²
ï¡nï¤ the symï¢ol of implicï¡tion âCâ
.
This has been called
by
Russell, in (1),
1
the âtheory of
impl
ication.
â
In
Å
ukasiewicz
ï¡nï¤ Tï¡rskiâ
s (2)
2
it is stated that
any set of axioms which, with the rules of substitution and detatchment, is sufficient for that
seï§ment of the propositionï¡l cï¡lculus which employs no operï¡tor ï¢ut âCâ (e.ï§. the Tï¡rski

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ï§ ï¡ vï¡riï¡ï¢le 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
whï¡t follows, we shï¡ll show thï¡t Tï¡rskiâs result cï¡n ï¢e proveï¤ if ï¡ certï¡in 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
ï¢
,
proviï¤eï¤ thï¡t â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.
[Eï¤itorsâ 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 thï¡t pï¡ï§e reï¡ï¤s: â1, 2. For our informï¡tion ï¡s to the contents of these two pï¡pers, we
ï¡re inï¤eï¢teï¤ 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
ï¡ï¢ï¢reviï¡tion for â
ï
ppâ, this lï¡w 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. Mereï¤ith ï¤evelops ï¡ system which uses not only âCâ, â
ï
â ï¡nï¤
propositionï¡l vï¡riï¡ï¢les, ï¢ut ï¡lso the âfunctoriï¡lâ vï¡riï¡ï¢le â
ï¤
â, so useï¤ thï¡t
ï¤
ï¡
may represent
any truth

function of which
ï¡
is an argument.
He shows thï¡t where â0â is ï¡n ï¡ï¢ï¢reviï¡tion 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 Mereï¤ithâs proof will ï¤o for this ï¡lso, if trï¡nsposeï¤ ï¡ little. Of his
premises 1

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

0 cï¡lculus (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 interpretï¡tion of Wï¡jsï¢erï§âs.
3,
CK
ï¤
0
ï¤
1
ï¤
p, thouï§h it cï¡nnot ï¢e treï¡teï¤ ï¡s ï¡n ï¡ctuï¡l thesis within Wï¡jsï¢erï§âs cï¡lculus, cï¡n ï¢e
treated as a metalogical abbreviation for a whole class of C

0 theses.
Thus regarded, it asserts
thï¡t within Wï¡jsï¢erï§âs cï¡lculus we mï¡y prove ï¡ny formulï¡ which consists of ï¡ âCâ, followeï¤
ï¢y ï¡ âKâ, followeï¤ ï¢y ï¡ny truth

function of â0â, followeï¤ ï¢y the sï¡me 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.
Mereï¤ithâ
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 propositionï¡l vï¡riï¡ï¢le; 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 Sylloï§istic from the Stï¡nï¤point of Moï¤ern Formï¡l
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.