Priest - Modality As Meta Concept

Download as pdf or txt
Download as pdf or txt
You are on page 1of 14

401

Notre Dame Journal of Formal Logic


Volume XVII, Number 3, July 1976
NDJFAM

MODALITY AS A META-CONCEPT

GRAHAM PRIEST

1 In this paper, we will construct and consider some basic properties of a


certain modal logic, or, more correctly, family of modal logics, generated
by a construction which is a standard linguistic tool, but has never been
applied to modal logics before. All modal logics till now (with the exception
of perhaps Lemmon's SO.5) have tried to serve two purposes at once:
i) To establish which truths are necessary, e.g., kfpv~p and hence
Hf L(pv ~p) by the rule of necessitation.
ii) To establish the relationships between such necessary truths, e.g.,
hp L ~p z> ~Lp.
In other words, the axioms of the logic have had to be sufficient to
establish modal truths such as \j L(p 3 q) . 3 . (Lp 3 Lq) and non-modal
truths, such as the theses of the propositional calculus. We will show in
this paper that these functions are better separated. Further, it is
surprising that it has never been fully realized that modality is a meta-
concept; for 'necessary' as applied to sentences/propositions is in fact a
convenient corruption of Necessarily true' (and similarly for 'contingent').
The sentence/proposition is not itself necessary: it could have been any
other. The necessity for being what it is belongs to its truth-value. Now,
we know very well that for an adequate formalization of the concept of
truth, we have need of a meta-language, we need then, a fortiori, a meta-
language for the formalization of the concept of necessary truth.
A glimpse of the danger of telescoping the object and meta-language is
the following. Consider the sentence:
(A) 'This sentence is not necessarily true'. (Or its Quinean version 'gives
a statement that is not necessarily true when appended to its own quota-
tion'.)
Suppose this is false, then it is necessarily true, and hence true.
Consequently, (A) cannot be false. Hence it must be true. Thus it is not
necessarily true and must be contingently true. It must, therefore, be
possible for it to be false, but as we have seen this is not the case.

Received January 12, 1971


402 GRAHAM PRIEST

What we will do in this paper bears a relationship to the above paradox


similar to the relationship between what Tarski did in his famous paper on
'truth' [1] and the Liar paradox. We will show how, given any object
language, we can construct a meta-language of sufficient power to talk
about its (the object language's) modalities. Rather, however, than show the
process in its full generality at first, which might be a little confusing, we
will show how it is possible with an example. The generalization on this
procedure will then become more obvious. One final point, however, before
entering the body of the work; that is, at the time of the method's concep-
tion, we wished to exclude iterated modalities, because their exact nature
was even less clear than that of other modal concepts. It became clear,
though, when the language, £1, had been constructed, that this method, in
fact, provided a sound conceptual basis for the iteration of modalities. But
of this, more anon.

2 Let us now turn to our example. For an object language, we will take
propositional calculus. This we do for two reasons: first the propositional
calculus is itself a basis for many other logical languages, and is, in some
sense, the basic logical language; secondly, the meta-language, ζι, which it
generates, is of some interest on its own account.
Object Language 0 We shall write ' \$* for 'is a thesis of the object
language, 0'. Small letters, 'p', 'q', etc. will be used as syntactic variables
for wffs of O. We chose the following axiom schemes for O (although any
equivalent set would do):
01 ^q^ipΏq)
02 fe[p(pr)]3[(i)3^(ί^)]
03 \o(~p^~q)^[(~p^q)^p\
Our rule of deduction is modus ponens; from \$p and ^p^> q infer \$q.
The logical constants O ' and <~* are taken as primitive. These are
supplemented by the usual definitions of V , '=', etc. O is the 2-valued
propositional calculus.
Meta-language Qι The question now arises as to whether the meta-
language, £χ should be translational or not, i.e., whether we should have in
it wffs having the same meaning as wffs of the object language 0, (as
in [1]) either course is, in principle, possible, but we will choose the latter.
This has the advantage of making what is going on much clearer: the dual
linguistic structure is made plain, and the exact status of the rule of
translation, T, is exhibited. We will write * ^ for 'is a thesis of QJ.
Capital letters, ' P ' , 'Q\ etc. will be used as syntactic variables for wffs
of Qlm
Primitive symbols
P, q,r, . . . wffs of 0
P, Q,R, . . .wffs of £i
~ , ι^, . . . monadic operators
3, . . . dyadic operator
(, ), . . . brackets
MODALITY AS A META-CONCEPT 403

Formation rules:
1) If p is any wff of O, then 1^ p is a wff of Qλ.
2) If P, Q are wffs of Qu so are ~ P and P^> Q.
3) Only formulas derivable from rule 1) and by successive applications of
rule 2) are wffs of £ i
We note that
(i) The symbols '~',C D', etc. are used ambiguously, as logical constants of
both O and Qγ. Strictly speaking, different symbols should have been used,
but since no confusion can arise, it was thought simpler to have only the
one set of logical constants.
(ii) The formation rules of Qγ permit as wffs those, and only those,
formulas that a r e pure, and of the first degree. That is, each O wff
subformula, must be in the scope of one and only one modal operator. E.g.,
fe P> ~ fe ~ Q a r e w f f s o f Qu b u t to ~toP9 PD Q> PD te Pa r e n o t
Definitions In Ql9 we have the usual definitions of 'v9, ζ=9, etc. plus the
modal definitions:
Dl \o P =df Lp
D2 Mp=df ~L ~p
It will be seen that the symbol L, is not strictly needed. However, it makes
things intuitively much clearer, to have both ' \Q9 and iV as symbols of Qγ.
(It might well be thought that Dl is excessively strong; but remember, we
are constructing a modal meta-language for a particular object language,
and hence, this is tolerable. Further, it is very easy to relax Dl, taking6L*
as primitive, and introducing the further axiom scheme: \ψ \$ p 3 Lp,)
Axiom schemes for Qγ Our non-modal, or proper, axiom schemes for Qλ
are:
Ml \ς P 3 (Q => P)
M2 \ζ\[P^(Q^R)]^[(P^Q)^{P^R)}
M3 \ζχ ( ~ P D ~ Q) 3 [(~PD Q) 3 P]
Hence all tautological manipulations of wffs of Qx are permissible in ζl9
Further, we have the modal axiom schemes:
M4 fc to (/> D tf) =>(&/> D
b-q)
Mδ D
fo to ^ ~to~£
It is clear that M4 and M5 are equivalent to postulating modus ponens for
0, and the consistency of 0, respectively. When translated into more
familiar language, with the help of Dl and D2, they become:
1
M4 k L(p^> q) 3 (Lp => Ltf)
M5 1 ^ L/> ^> ~ L ~poτ fa Lp z> Mp
Our rule of deduction for ζ1 is modus ponens: from ^ P and
^ P D Q, infer ^ ρ.
We now come to the very important:
404 GRAHAM PRIEST

Translation Rule This is the rule that correlates O and f lβ

T: From \^p (in 0), deduce \ςχ ^ p (in (j^, and vice versa: from \ς \$ p
(in gλ) deduce fo /> (in 0).
This says that if p is a thesis of O, then ι^£ is a thesis of Qx and vice
versa. It is equivalent to saying that if p is provable, then 'p is provable'
is provable. With the help of Dl, T reads:
1
T: From ^ p deduce ^ Lp, and from ^ L£ deduce \$p.
We will now prove a few derived rules and theses of Qu to give some idea
of the power, and the proof technique, of Qx. We will take all tautologies
for granted, writing 'Taut M9 or 'Taut O9 as they follow for Ml-3 or 0 1-3.
DR1 From t^ p deduce ^ Mp.
(i) from fe /> infer fc fo /> (T)
(ii) infer ^ LP (£i)
But
(iii) ^Lp^~L~p (M5)
i.e.,
(iv) k Lp ^ M/) (i)2)
So from (ii), (iv) by modus ponens:
(v) from \Q p infer ^ M£

L D L(
(P Ό V)Ώ (LP
M4
(i) fe l) ( )
L
(ii) fe ^ D Λ D (L^D L
^ M4
( >
but
(iii) \ζχ [(P D Q).(β D S)] ^ (P. Q) ^ (R.S)] (Taut M)
hence
(iv) k [L(/> D ^).Lte D />)] D [(L/> 3 L^). (Lq D L/>)]
(v) fe L(p ^ ^ 3 (L/> = L^) (De/ ^ 0
DR2 If \$(P = q) then ^ (L^ s L^)
(i) from ^ (p = ^) infer ^ Lip ^ q) (T1)
(ii) but %L{p^q)Ώ{Lp^q) (Gl)
Hence by (i), (ii) and modus ponens
(iii) from ^ (p s #) infer ^ L/> s L^
It is now very easy to establish by induction the rule of substitutivity of
equivalents in Qγ or more precisely:
S.E.1. // fe (/> = ?) then ^ P = Q.
MODALITY AS A META-CONCEPT 405

Where P and Q a r e wffs of Q1 and are the same, except that P h a s £ as


an 0 wff subformula in one or more places, where Q has q.
S.E.2. // fe (R ^ S) then fe (P = Q).
Where P and Q a r e wffs of Qx and a r e the same, except that P has R as
a Qι wff subformula in one or more places, where Q has S.
The above results a r e shown in the normal way, by induction on the
degree of P and Q, using DR2, and the following tautological derived rules:
If k(P = Q)then ^(~P^~Q).
If k(P^>Q)then fe (P => R) ^ (Q D R).
If fe ( P => Q) then ^ (Λ D P ) D (Λ D Q).
G^ \L(p.q) ^(Lp.Lq)
(i) y-op.q^P (Taut (7)
(ii) %L(p.q^)p) (T 1 )
(iii) ^ L(p.q) ^ L^> (by M4 and modus ponens)
similarly
(iv) ^ LCM) =) L^
(v) ^ [(P 3 Q).(P ^ Λ)] => [(P => (Q.Λ))] (Taut M)
(vi) ^ L(/>.^) => Lp.Lq. (by (iii), (iv) and (v))
(vii) *dP^ (q^ (p.q)) (Ίaut 0)
(viii) ^ L/> D L(<7 =) (£.#)) (by T 1 , M4 and modus ponens)
(ix) ^ L/> D (L^ z) L(p.q)) (by M4 and modus ponens)
(x) ^ [ P 3 ( Q D Λ ) ] => [(P.Q) D Λ] (Taut M)
(xi) k L^.L^ =) L(A^) (by (ix) and (x))
Thus
(xii) ij L(p.q) = (Lp.Lq) (for (vi), (xi) and the def. of «s>)
The above proofs should be sufficient to demonstrate the proof techniques
at hand in £ 1 # Since this is only a short paper, and the details of proof a r e
somewhat tedious anyway, we will just list a selection of the most important
theses of Qx. In most cases, the actual proof is quite straightforward.
GJ.a): ^ L ~p = ~Mp
Gι3.b): \gχ~Lp = M~p
GX3: ijx Lp = ~M - ^
d4: ^M(pvq) = (~Mp.~Mq)
Gβ: \gχ M(p vq) = (Mp vMq)
Gφ: k L(p D ^) 3 (Mp ^ Mir)
Gi7: ^(LpvLq) ^ L(pvq)
Gβ: ^ M(p.^) 3 (Mp.Mq)
G,9: frL^pΏp) ^Lp
GxlO: k [Lto ^ />). L ( ~ ^ ^ />)] s L/>
dJi: \Lp^> L(q^p)
0,12: \ζlL~pΏ Up 3 q)
406 GRAHAM PRIEST

Gλ13: \ξχLp^[Mq^M(p.q)}
GJ4: k L(pvq) θ(LpvMq)
9
It is possible to define 'p strictly implies q (p -s q), in the usual way, as
L(p ^ q). This will do as an exposition of £Ί and its object properties.
3 We note that formulas such as p D Mp, Lp ^ p, and other such formulas
that straddle O and Qx are not expressible in either O or Qx. This is a
direct result of our electing to construct a non-transitional meta-language.
Clearly, had we chosen the other course we would have wished such things
to be provable in the system, and it is quite straightforward to see how this
could be done. What, in fact, do we lose by not having such straddled
formulas as theses? The answer is 'surprisingly little' and the reason is
this:
Whenever a truth of the philosophy of logical necessity is expressed by
a straddled thesis of T or S5, etc., then that truth is expressed by the
corresponding derived rule of inference in O/Qi.
We will not stop to prove this, but it is intuitively clear. E.g.,
(i) Lp => p; if \ζγhp then fe p is T\
(ii) p => Mp; if ^ p then ^M is DR1.
(iii) ~p 3 ~Lp; if *&~p then j x ~Lp is a derived rule:
Proof: to ~P (Hyp.)
so fcL ~/> (T1)
so ^"Lp. (M5)
(iv) [L(p 3 q). p] => Mq; if ^L(p => q) and ^p then \ζχMq is a derived
rule:
Proof: ϊςL(p^q) (Hyp.)
»D iP => Φ (T 1 )
but fyp (Hyp.)
so 1^ q {modus ponens)
so ^Mq, (DR1)
etc.
Further, it might be thought that we could not prove some wffs that were
pure and of the first degree that ought to be theses, due to the non-
appearance of straddled wffs. But this is not the case (see section 5 for the
completeness of Qx—in effect M5 takes over this function of straddled wffs).
Hence, we lose virtually nothing. Also, an interesting extension of Qx
might be obtained by adding a new predicate 'T9 to Qx and axiomatizing it,
such that \Tp has the force of 'p is true'. Then the equivalent of any
straddled wff could be proved in this system, e.g., for p ^> Mp, we have
Tp 3 Mp, etc. (Assuming that one wished to assume that p is true if fp.)
We will not pursue this line of thought further in the present paper,
however.
MODALITY AS A MET A-CONCEPT 407

4 A pertinent question now would be this. We know that it is possible to


prove something of the form ^ ί by a proof that is partly in Ql9 i.e., the
rule T is invoked to infer a wff of 0 from the statement of its necessity in
Qx. Is it possible to prove anything like this, that is not provable simply in
01 An affirmative answer to this question would be somewhat disastrous,
but fortunately would be false. We will postpone a proof of this result,
however, until we have considered modal predicate logics, so that the proof
may have a more general nature.
5 We now diverge slightly from the general train of the paper to consider
some individual properties of the system Qx,
Consistency That Qλ is consistent, is easily provable, by the standard
method of modal logic. That is, by mapping Qx onto the 2-valued proposi-
tional calculus by deletion of modalities. The proof is quite straight-
forward, and we refer readers to, for example, [2], pp. 41-42.
Semantics for Qγ A model for Qγ is readily found with the help of the usual
Kripke semantics for modal logics. In fact, it is quite easy to show that
any S5 model is a model for <JΊ. Since this is very similar to the standard
cases we will not go into it in great detail, but we define a model as an
ordered pair (U, V) where U is a set of worlds w{ and V is an evaluation of
wffs of O and Qu satisfying the normal S5 conditions. (See for example [2],
pp. 71-75.) A wff of Qγ is then true in the model iff it has the value 1 for
all Wi under the evaluation V. It is now readily seen that the axiom
schemes M1-M5 are true in every model (they are all theses of S5) and that
modus ponens preserves truth. The translational rule, T, cannot be said to
preserve truth, as such, in a Qx model, since the wffs of 0 are not in Qu
and hence, cannot be true in Q\. What we can do, however, is to consider
the S5 model as a dual model for both 0 and Q1 taken together, i.e., as
model for the language whose theses are the theses of 0 and the theses of
Qι. We then can say that the rule of translation preserves truth. Hence all
the theses of Qx are true in any Qγ model. Since also, in effect, a Q1 model
is a restriction of an S5 model to the wffs of S5 that are well-formed by the
formation rules of ζl9 we have shown:
If P is a wff of S5, that is well-formed according to the formation rules
°f Qu then P is true in an S5 model iff P is true in the corresponding Qγ
model.
Completeness To prove the completeness of Qu what we will do is this, we
will prove that
(A) If P is a wff of S5, well-formed with respect to the formation rules of
ςu then %5Piff ^ P .
This shows that the theses of Qλ are precisely the theses of S5, that
are well-formed with respect to the formation rules of Q±. We then invoke
the completeness theorem for S5 ([2], p. 116), to show that Qγ is complete
with respect to its model, i.e., the S5 model restricted to Qλ well-formed
formulas. We prove (A) by furnishing a decision procedure for Q\.
408 GRAHAM PRIEST

Decision Procedure We define Modal Conjunctive Normal Form (M.C.N.F.)


as follows: P (a wff of £x) is in M.C.N.F. if P is a conjunction, possibly
degenerate, of disjunctions, possibly degenerate, such that each component
of the disjunction is a wff of 0 in the direct scope of one modal operator.
E.g.:
(MpvLp). L(p ^> q)
(i) Every wff P of Qx can be reduced to M.C.N.F. P 1 such that ^ P = P 1 .
This is done by replacing all occurrences of <~Ly and '~M9 by ζM~y and
*L~y respectively, (G^.a and b). We then treat all wffs of the form Lp and
Mp, as atomic and proceed by propositional calculus methods. We know
that all propositional calculus wffs can be reduced to conjunctive normal
form.
(ii) Order each conjunct: Lpxv Lp2v. . . v Lpnv Mqxv . . ,vMqm which is
provably equivalent to
Lpx v . . . v Lpnv Mq, w h e r e q = qxv q2 . . . v qm. (GX5)

(iii) A particular conjunct is valid iff some p{ v q is propositional calculus


valid.
(iv) P 1 is valid if each conjunct is valid.
(v) P is valid if P 1 is valid.
(iv) and (v) are obvious. We will prove (iii).
Proof of (iii): a) Let p{vq be PC (propositional calculus) valid, i.e.,
fo- Pi vq. Hence ^LiPi vq) by T 1 . Hence ^(Lp vMq) by Gλ14 and Modus
ponens. If q is null, then the last step is redundant. If p{ is null, then we
have \Mq by DR1. Finally, ^Lp^Lp2 . . .vLpnvMq (^PD(PvQ)),
i.e., ^ P 1 .
b) Let none of />,- v q be PC valid. We then construct a Qγ model in which P 1
(= Lpiv . . . v Lpnv Mq) is invalid and hence, unprovable. In our model
(U, V), let U = {wλ . . . wn). Since all p{ v q (and hence all p{ and q) are PC
invalid, we^can find an evaluation V, such that
V{wiq) = 0 for all i. Viw pi) = 0 for all i.
So we have that pi is invalid in wi9 and hence Lpi is invalid in (ί/V>.
Further Mq is invalid in (C/V), since q is false in all Wi. Hence P 1 is
invalid. Thus we see that either a wff in M.C.N.F. is invalid and hence, not
provable, or it is valid and the above proof furnishes an effective proof in
gΊ starting from the PC valid p4 v q.
We note, further, that this decision procedure works for all Qι—well-
formed (by the formation rules of ζι) formulas of T, S4 and S5. We simply
replace the appeal to T 1 by an appeal to the rule of necessitation. Further,
the model in part b) of the proof is also a valid T, S4, or S5 model. We
have hence shown:
If P is Q!-well-formed, then ^ P iff ^ P iff ^P iff %5P.
MODALITY AS A META-CONCEPT 409

The completeness of Q1 to its model follows trivially from the


completeness of S5.
6 We now return to the main theme of the paper, which is the general
method of constructing Q-meta-languages. The method appears to be this:
Take an object language. Furnish a set of proper (non-modal) axioms
for Q. Add the two modal axioms M4 and M59 and the translational rule T.
This generates a Q -meta-language.
It will be noticed that the proper axioms of Q are left open to choice.
Often, they will be the axioms of 0, as in our example, but not necessarily
so. For example, suppose we wish to construct a Q-meta-language for the
intuitionist propositional calculus, or for a particular many-valued cal-
culus. Then for the proper axioms of Q we might wish to take the axioms
of the object language or we might wish to take, say, the axioms of the
ordinary two-valued, propositional calculus. Either choice would produce a
Q-meta-language, and which one one chose would depend purely on
philosophical considerations.
Another interesting way in which our original Qx system could be
extended, is to a modal predicate logic. Here, different systems arise,
again, depending on what sets of axioms we choose for 0 and Q. If the
object language is the predicate calculus, and the proper axioms of Q are
those of the propositional calculus, then we see that only modalities
de dicto can arise. If, however, we do it the other way round, only de re
modalities arise.
Probably, the most interesting system is generated by taking the
axioms of the predicate calculus (without identity) for both O, and the
proper axioms of Q. This way we get both sorts of modalities. Without
making this paper too lengthy it is impossible to go much further into any
of these systems, but we will give one proof, in the last cited system, just
to show what sort of structures are available to us. We add the following
axioms to 01-03:

04 ^ (x)a 3 a' where a* is a with all occurrences of x replaced by some


individual constant or variable, (possibly x itself).
05 ^ (a 3 β) 3> (a D (x)β) provided x is not free in a.
This makes O, the predicate calculus. We add two similar axioms M6
andM7to Ml -3.
G21: %L(x)a^> (x)La
Proof:
(i) \d(x)aoa (04)
1
(ii) ijL(MαDα) (T )
(iii) 15 L(x)a ^ La (M4)
(iv) ίξ L(x)a 3 (x)La (M7 and modus ponens)
410 GRAHAM PRIEST

It is interesting to note, however, that even in this system, the Bar can
formula (x)La 3 L(x)a is not provable, but may be taken as an extra axiom.
A little thought will show that this is equivalent to postulating the ω -com-
pleteness of 0. The rule of inference corresponding to the Barcan formula,
however, is provable. We prove:

If \ξ (x)La, then ^ L(x)a


(i) ^ (x)La (Hyp.)
(ii) %{x)La^>La (M6)
(iii) £ La (by modus ponens)
(iv) *a (T1)
(v) ft (x)a (by universal generalization)
(vi) %L(x)a (byT 1 )

A similar result is provable in the usual predicate extensions of T and S4.


Another interesting extension is gained by introducing identity into the
object language. In normal modal predicate logics,this leads to paradoxical
results, such as
a = b => L(a = b)

i.e., all identities are necessary! This is a direct result of the fact that in
the usual axiom scheme for identity, i.e., a = b ^ (A = B) where A and B
are the same, except that A has a in some or all the places where B has b,
Ά' and 'B* are allowed to range over all wffs of the language, which, of
course, include modal wffs. In our two-tier system, however, this does not
occur, since A and B range over wffs of 0 , only. In normal, so-called
'contingent identity systems' this restriction appears totally ad hoc, but in
our two-tier system, it is a natural consequence of the linguistic structure.
We see clearly now how the £-construction throws light on several
awkward problems of modal predicate logic, such as the nature of de re and
de dicto modalities, and the 'paradoxes' of identity.

Leaving aside extensions of our original system now, we will finally


consider an extension of the technique itself, to generate iterated mod-
alities. Suppose we construct a meta-meta-language QQ, axiomize it with
the same axioms as Q9 and add a rule of translation between Q and QQ, of
the form:

Ti tςPiff ^q if P.
Then, writing Lx for \^ just as we wrote L for \$ , we have wffs in QQ
such as
LxLp => LλMp.
In this manner, we can construct an infinite hierarchy of meta-
languages such that every pure wff (i.e., wff in which every 0 sub-wff is in
the scope of the same number of modal operators) is a wff of some member
MODALITY AS A META-CONCEPT 411

of the hierarchy. The subscripts of the 'V symbols then become optional
and can be dropped, giving the ζL* typical ambiguity. This technique has
one very interesting consequence, which is as follows: The construction of
modalities in our Q systems is compatible with a conventionalist view of
logical necessity. That is, that a necessary truth is necessary because of
the way we use words, i.e., it is true either by convention or definition
(i.e., the axioms of 0) or by logical consequence of conventions (logical
consequence being truth-preserving by definition).
However, returning to Ti, we see that we have:
\gPiff \ggLP.
Now 'Lp is a wff of Qx and so substituting for *Py in the above, we have:
}

fc Lpiff ϊξgLLp.
This is the equivalent, in our infinite hierarchy of languages, of the S4
principle, which is usually reckoned to be inconsistent with a conven-
tionalist point of view. We see, however, that this is not so.
7 We now return to the question posed in section four: can we prove any
wff of O that was not already provable, when we build a £-meta-language
onto OΊ The answer to this question for the system Qx is clearly 'no',
since we know that 0 (the 2-valued PC) is maximally consistent. Suppose,
however, we chose for O a weaker system, say an rc-valued logic, but retain
a 2-valued logic for the proper axioms of QΊ The answer is no longer
obvious. We will prove the following:
Theorem 1 Let 0 be any consistent system governed by modus ponens, and
let the proper axioms of Q be any subsystem (possibly not proper) of the
2-valued predicate calculus. Then if there is a proof of any wff p of 0,
there is a proof of p wholly in 0.
We note first that we cannot let the proper axioms of Q be an arbitrary
consistent system, since this would let in such things as the consistent
system whose only axiom is h(p ^> p) 3 ~q. (There is no wff p, such that
both v-p and v-~p in this system.) Hence we restrict our attention to
subsystems of the 2-valued predicate calculus. This is no drastic loss of
freedom, however, since all the systems we are normally interested in
e.g., the intuitionist or many-valued propositional and predicate logics, are
subsystems of the 2-valued predicate logic. Further, it would be very
difficult to take seriously any system that had theses that were not theses
of the 2-valued predicate logic, as an adequate formalization of the terms
'not', 'if... then', 'for all', etc. Also, it is fairly clear that the proof could
be extended to any consistent first-order logic. Secondly, we note that to
prove Theorem 1, it suffices to prove the result when Q is the full 2-valued
predicate logic. Theorem 1 then follows trivially, since if v^p were
available in some subsystem, it would certainly be available in the full
system. We prove then, the result, when the proper axioms of Q are those
of the full 2-valued predicate calculus. The first step in the proof is to
412 GRAHAM PRIEST

observe that what we are in fact trying to show is that 'Lp' can never be
proved in Q when ζp9 is not provable in O alone. Now, it is clear that no wff
of the form ζLp' is provable in Q without the rule T appearing somewhere
in the proof. If this were not so, we could merely put '~p9 for 'p*
everywhere in the proof and obtain a proof of (L ~ p' and hence, by M5, and
modus ponens, we have a proof of '~Lp', making Q inconsistent.
This suggests treating the axioms of Q as transformation rules on a
certain input. Namely, those wffs of the form Lp which are obtained
directly from O, by one application of the rule T. This in turn suggests a
Gentzen-type system. What we do then is to construct a system of natural
deduction at least as strong as the Q meta-logic whose proper axioms are
those of the 2-valued predicate logic.
Let γ be any set of rules adequate for a system of natural deduction
equivalent to the 2-valued predicate calculus containing at least the cut
rule,
AsrB ~BvC
AvC
the exchange rule,
AvBvC vD
AvCvBvD'
and the dilution rule,
A
AvD
(see, e.g., [3], pp. 81-103, where a different, though essential equivalent
formalization is used). We consider the system Γ of natural deduction,
whose rules are those of y, and the initial wffs (axioms) of whose proof
trees are (i) wffs of the form Lp where \gpf or (ii) wffs of the form ~Lp
where not \$p and no others.
To facilitate the proof, we prove two lemmas:
Lemma 1 If \^ p then \ψ P, and hence, if not \ψp, then not ij P.
Proof: If P is a thesis of Q, obtained by a direct application of the rule T,
from 0, then P is an axiom (i.e., possible initial formula) of Γ.
The axiom schemes Ml-3, 6, 7, of Q, are theses of Γ by hypothesis
on γ.
The schemes M4 and M5 are theses of Γ.
The proof is as follows: Either Lp or ~Lp is an axiom. If ~Lp is, then
Γ ~Lpv ~L ~ p by dilution. If Lp is, then ^p, and since O is consistent,
~p is not provable, and hence ~L ~ p is an axiom. Thus again we have
ψ~Lpv~L~p by dilution and exchange. Hence, in either case ~Lpv
~L ~p is provable, and this is clearly the equivalent in Γ of M5 (in
MODALITY AS A MET A-CONCEPT 413

disjunctive form) in Q. Similarly either L(p D q) or ~L(p ^> q) is an axiom


of Γ. If ~ L{p => q) is, then ^ - L(p => q) v - Lpv Lq by dilution. If L(p => #)
is, then either Lp or ~ Lp is an axiom. Suppose ~ Lp is, then [p~L(£ ^ q) v
~LpvLq by dilution and exchange. Otherwise L£ is an axiom. Hence by
construction, we have that \Q p ^> q and i# £, and thus, by modus ponens,
fo <?. Therefore, L# is an axiom of Γ, and ^ ~ L(p ^> q) v ~ Lpv Lq, by
dilution and exchange. Hence, whatever the case, ~ L(p ^> q) v~LpvLq is
provable, and this is the equivalent in Γ of M4 (in disjunctive form) in Q.
Finally, an application of modus ponens in Q is truth-preserving
between the equivalent formulas in Γ because of the cut rule. Hence we
have established that: ^ P ==> ψ P.
We now prove:
Lemma 2 If ^ Lp then Lp is an axiom, i.e., \^p.
Proof: We know that we can choose y, such that all its rules have conclu-
sions of degree higher than (i.e., more connectives and quantifiers than)
their premises, except for the cut, dilution, and exchange rules. Hence, if
Lp is a thesis of Γ, it is either an axiom, or it is the conclusion of a cut.
We know,however,that if there is a proof of P in Γ, then there is a cut free
proof. (This is Gentzen's Haupstatz.) It follows that if lp Lp then Lp is an
axiom, i.e., ^ p.
Theorem 1 is a trivial consequence of Lemma 1 and Lemma 2.
A Note on Constructivity The above proof is, of course, not constructive,
but a constructive proof is available. We construct the system of natural
deduction Γ° whose rules a r e those of y, plus:

M4o AvL(p^q) LpvB


AwLqvB
and

Av~Lp
We allow as axioms of Γ°
(i) any wff of the form A v ~A,
(ii) any wϊi Lp where \$p,
and no others.
It is quite straightforward to prove that:
a) ^PΦ^P.
b) If b,0 Lp then Lp is an axiom.
The proof of (b), however, requires that the cut theorem for Γ° be
established. This, though not a complicated matter, is relatively lengthy,
and hence we chose to give the nonconstructive proof.
414 GRAHAM PRIEST

8 With this result, which is a guarantee that we have not been doing
anything illegitimate syntactically in the previous six sections, we conclude
this paper. I am indebted to Sue Haack for a number of helpful comments
on earlier draughts of this paper.

REFERENCES

[1] Tarski, A., "The concept of truth in formalized languages," in Logic, Semantics,
Metamathematics, The Clarendon Press, Oxford (1956), pp. 152-278.
[2] Hughes, G. E., and M. J. Cresswell, An Introduction to Modal Logic, Methuen
and Co., London (1968).
[3] Gentzen, G., The Collected Papers of Gerhard Gentzen, ed. by M. E. Szabo,
North-Holland, Amsterdam-London (1969).

Bedford College
London, England

You might also like