Priest - Modality As Meta Concept
Priest - Modality As Meta Concept
Priest - Modality As Meta Concept
MODALITY AS A META-CONCEPT
GRAHAM PRIEST
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
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
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
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:
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.
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
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