The Nachlass of A.N. Prior
a joint project between
Department of Information Studies - University of Copenhagen
and
Department of Communication and Psychology - Aalborg University

Prior & Kerr: Axiomatisation of the Propositional Calculus in C and p

By Arthur N. & R.P. - Prior & Kerr on NA/NA/1951

Download the PDF of this item
Please note that this text is extracted from the PDF, and is as such most likely not styled properly.
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.


  www.priorstudies.org •  University of Copenhagen •  Aalborg University •