POSSIBLE WORLDS SEMANTICS FOR PREDICATES

VOLKER HALBACH, HANNES LEITGEB, AND PHILIP WELCH

Abstract. We develop possible worlds semantics for □ as a predicate rather than as an operator of sentences. The unary predicate symbol □ is added to the language of arithmetic (or an extension thereof); this yields the language L_{□}. Every world in our possible worlds semantics is the standard model of arithmetic plus an interpretation of □. We investigate possible–worlds models where □⌜A⌝ is true at a world w if and only if A is true in all worlds seen by w. The paradoxes exclude certain frames from being frames for □ as a predicate. We provide some sufficient and also some necessary conditions on frames that are allowed to act as frames for the predicate approach. Completeness results for certain infinitary systems corresponding to well known modal operator systems are established. We draw some conclusions concerning the current state of the predicate approach to modalities.

§1. Modalities as Predicates. Modalities like necessity and possibility, may be analysed logically in essentially two ways: either as predicates, or as operators. In the first case they are applied to singular terms, whereas in the second case they are applied to formulæ, but in both cases the application gives us new formulæ. Thus the distinction between the operator and the predicate conception of necessity is made on the syntactical level at first. Both conceptions are tied to certain semantics respectively. If “necessary” and “possible” are regarded as predicates, they are interpreted as properties of objects and a decision has to be made concerning what precisely they should be predicates of: syntactical entities like sentences, or contents of syntactical entities like propositions (let us ignore further options like utterances or mental objects). In either case, necessity and possibility are properties of such entities, or, perhaps, relations between such entities and further objects. If “necessary” and “possible” are regarded as operators, they do not express properties or relations like predicate and relation expressions; necessity does not apply to anything – much like the logical connectives or the quantifiers. In this sense the operator conception of necessity is radically deflationary. Similar considerations apply not only to necessity but also to the notions of knowledge, belief, future and past truth, obligation and so on, which have been treated in analogous fashions as necessity.

Received by the editors March 1, 2002.

The closure ordinal γ for the operator Φ was suggested to Volker Halbach by Peter Aczel and independently by Philip Welch, who later agreed to be a co-author of the paper and proved Theorem \underline{g=k} 4.8. The work of Volker Halbach was partially sponsored by the research group Logic in Philosophy at the Universities of Tübingen and Konstanz.

There are various arguments in favour of, or against, each of these options of logical representation, but we shall not dwell on the pros and cons in more detail because this would require a careful analysis (see Bealer ^{\underline{Bea82}} [4] and Halbach ^{\underline{Halhabil}} [16]). Instead we are going to concentrate on a particular problem affecting modalities if regarded as unary predicates of sentences, i.e., according to the extensionalist version of the predicate view from above. This position has been held and defended most notably by Quine \underline{Qui77,Qui56b} [25, 24]. We think that there would be very good reasons for preferring this account if it was not threatened by inconsistency: Montague ^{\underline{Mon63}} [22] was the first to notice that the predicate version of the acknowledged modal system T is inconsistent if it is joined with arithmetic. This is due to the existence of self-referential expressions, which is a consequence of Gödel’s diagonalisation lemma, which is in turn derivable from even weak systems of arithmetic. From this Montague concluded:

Thus if necessity is to be treated syntactically, that is, as a predicate of sentences, as Carnap and Quine have urged, then virtually all of modal logic [ …] must be sacrificed.

Note that the intensionalist version of the predicate view on modality, i.e., where necessity is considered a predicate of intensional entities, is not necessarily affected by analogous problems. Propositions might e.g. be much more different from their syntactical counterparts than sometimes thought of, and therefore there might not be any self-referential propositions; perhaps self-referential sentences do not express propositions at all (for a recent account following that line of thought see Slater ^{\underline{Sla??}} [31]). On the other hand, if propositions have a syntactical structure similar to sentences, and if every well-formed sentence expresses a proposition, then inconsistency strikes again (as has been pointed out by Asher and Kamp

\underline{Ash89} [2]).

According to the operator account of modality, there are simply no self-referential sentences rising from the use of modal expressions, since in order to be self-referential the sentences with operators would have to contain themselves as a proper part, which they certainly do not in the standard operator languages (below we shall make a remark on operator languages with additional devices like propositional quantification). Thus self-reference is abandoned from the start by suppressing referential clauses and by that move also the inconsistencies are avoided. This is one of the reasons why the majority of philosophers and logicians have opted to reject the predicate view altogether.

For the security from inconsistency, however, one has to pay a high price: quantification is not expressible in operator languages unless one adds further devices like propositional quantifiers. For instance, there is no way of expressing “All tautologies are necessary” in a single sentence of the operator language. If auxiliary devices like propositional quantification are employed, we expect that these additional devices reintroduce the difficulties of the predicate approach (Grim ^{\underline{Gri91}} [12] argues for this view).

We doubt that the inconsistencies justify the general preference of the operator view over the predicate conception. We shall sketch some arguments for this claim but leave a thorough discussion of these matters to another paper.

First of all, by far not every system of modal logic has an inconsistent predicate counterpart. E.g. the predicate version of the minimal normal operator system K is indeed consistent. Secondly, des Rivières & Levesque ^{\underline{Riv86}} [27] and Belnap & Gupta ^{\underline{Bel93}} [5, p. 240ff] have shown that sentences of modal operator systems can be translated into sentences of corresponding and consistent predicate systems such that provability is preserved. Thus, roughly speaking, everything that can be said with operators can (consistently) be expressed with a predicate. Only if the provability of axiom schemes is to be preserved, troubles are emerging: we can have □⌜A⌝ → A for any translation of a modal operator formula into the language with □ as a predicate, but we cannot have it for all sentences of the predicate language. The translations of operator sentences are always grounded in the set of sentences which are modality-free, and therefore self-referential instantiations of the T-scheme are excluded.

Along the main stream of the operator conception of the modalities there has been some work on the predicate approach. One ‘modality’, however, has even been treated as a predicate by most authors, namely truth. The motivation for preferring the predicate approach in this case is obvious: the trivial modal system with the ‘T-sentences’ □p ↔ p as axioms for □ will hardly qualify as a satisfying analysis of truth. Again we leave a discussion of the involved relations holding between the truth predicate, modal operators, and substitutional quantification to another paper. For our present purposes, however, it is important that several logicians have provided various models for axiom systems with predicates of sentences (or their codes). Friedman and Sheard ^{\underline{Fri87}} [11], for instance, have studied a variety of systems built over an arithmetical base theory plus axioms for an additional unary (truth) predicate. Although the additional predicate is usually labelled as a truth predicate, some systems rather resemble systems for necessity or other typical modalities. We think that this applies, e.g., to one important derivative of the Friedman & Sheard systems, namely Cantini’s ^{\underline{Can90}} [7] system VF. Therefore we surmise that some work on axiomatic theories of truth is also relevant for the predicate conception of other notions.

Truth theorists have investigated a variety of axiom systems (see, e.g., Cantini ^{\underline{Can96}} [8], Halbach ^{\underline{Halred}} [15] and Sheard ^{\underline{She94}} [30] for overviews). Consistency proofs for these systems have been provided by model constructions. One aim of the present paper is a generalisation of these model constructions: we do no longer consider a single system and construct a model for this system. Rather we investigate a natural family of systems and provide a general pattern for generating models. And vice versa we aim at a generalisation of the inconsistency results. By showing that there is no model of a certain kind, we shall be able to conclude that a (semiformal – in the sense of Schütte ^{\underline{Sch77}} [29],Sect.28) system is inconsistent or that a certain formal system does not have an ω-model.

Of course, we cannot hope to capture all the sophisticated model constructions found in the literature in a single approach, simply because they are too varied. Here we take some inspiration from the operator approach. Modal logicians do not investigate arbitrary modal systems (i.e. logic plus arbitrary axioms and rules for the modal operator □) but they restrict their focus on certain well behaved theories. The most common class of such well behaved theories is known as the set of normal modal systems (see, e.g., Boolos ^{\underline{Boo93}} [6]). We follow exactly the same route for predicates. In this way we shall obtain results on the semantics of a comprehensive and important class of systems with a modality predicate.

Opting for possible world semantics in a more or less standard form implies certain restrictions. For instance, necessitation holds in all normal modal systems. Our possible world semantics for predicates will verify an analogous rule. Thus axiom systems which are not compatible with necessitation (like the Kripke-Feferman system Ref(PA) of Feferman ^{\underline{Fef91}} [10]), which is also known as KF, fall outside the scope of our present paper. By no means do we wish to claim that these systems are less interesting or natural than ‘normal’ systems, but it makes sense to restrict attention to a class of well behaved system, that is, ‘normal’ systems first. Just as in the case of modal logic one finally can go on and explore non-normal systems and their semantics in a general framework.

Our approach does not only include a restriction to normal modal systems or, more exactly, to the predicate analogues of normal modal systems (see Lemma ^{\underline{normality}} 2.3), but also a restriction to systems consistent in ω-logic. This restriction is brought about by our choice of the standard model of arithmetic as the basis for our model constructions. First of all this restriction serves the purpose of avoiding the intricacies of nonstandard models of arithmetic, but furthermore systems consistent in ω-logic are certainly quite natural. (However, there are natural and philosophically significant ω-inconsistent systems like the system FS mentioned below).

In our approach we want to stick as closely as possible to the common possible worlds semantics for operators, i.e. we use frames of worlds such that every world is a classical model. Since we shall apply the predicate □ to numerical codes of sentences, we assume that every world is actually a standard model of arithmetic which is only extended by assigning some extension to the Box – thus we restrict ourselves at first to just the arithmetical vocabulary plus a unary modal predicate. Later we are going to extend this language by non-arithmetical and non-logical vocabulary. Our treatment of necessity by means of a predicate extends to other modalities as well, but for the sake of simplicity we shall only speak of necessity and not enumerate all other modalities to which our approach may be applied.

On the semantical level, and as is common in modal logic, necessity is considered as truth in all accessible worlds, i.e., □⌜A⌝ is true in w if and only if A is true in all worlds accessible from w, where accessibility is a binary relation (defined by the frame) on the class of worlds. At this point the fundamental difference between possible worlds semantics for modal operator and modal predicate languages shows up: according to the operator conception, the satisfaction clause for □⌜A⌝ can be turned into a proper definition, but not so in the predicate case. If a frame is given and a function that assigns a model for the □-free language to any world, then truth or falsity for all sentences without □ extends to truth for all sentences with □ as an operator in the usual recursive way. Thus one can always build a model on any given frame if the operator conception is presupposed. But if □ is treated as a predicate, the recursive definition of truth at a world cannot be carried out anymore, because a sentence □⌜A⌝ is atomic, while on the operator account □A has the complexity of A plus one. There is also no way to provide a definition of the (possibly transfinite) complexity of a formula that would allow for a recursive definition of truth at a world. The satisfaction clause for modal sentences now works just as a condition on models, such that every model that meets the conditions counts as a proper instance of a possible worlds semantics for predicates. For some frames a recursive definition of truth at a world is not only impossible, but there is not even a model based on the frame at all due to self-referentiality. Montague’s ^{\underline{Mon63}} [22] Theorem, for instance, shows that one cannot build possible worlds models on reflexive frames (see Example ^{\underline{mezzo}} 3.1 below) if necessity is expressed by a predicate. This means that there is no way to assign truth and falsity to all sentences in such a way that □⌜A⌝ comes out as true if and only if A holds at any world (and if some conditions are met which will be explained below) . Another example is provided by McGee’s ^{\underline{McG85}} [21] theorem on ω-inconsistent systems. It is a direct consequence of this theorem that a frame consisting of the natural numbers ordered by the predecessor relation (so that 0R1R2R3R …) does not support a possible worlds model (see Example \underline{mcgee} 3.2 below).

Our question from above may finally be stated in the following form: which frames support a possible worlds model, if □ is a predicate, and if the object language allows for self-referentiality? We call the problem of characterising the frames which support possible worlds models for predicates the Characterisation Problem.

A satisfying answer to the characterisation problem would exhibit a graph-theoretical description of the frames supporting possible worlds models. The restrictions imposed by theorems like those due to Montague and McGee should be consequences of such a characterisation result. A system with a modal predicate might thus be checked for consistency (or rather consistency in omega logic) by investigating what its corresponding possible worlds semantics would look like and whether the latter satisfies our characterisation criteria. In this way paradoxes and inconsistency results for modalities as predicates can be modelled in a systematic and informative way.

Our development of possible worlds semantics for predicates also yields some further insights: it sheds new light on hierarchies of metalanguages; some results of provability logic and modal logic show up in a different fashion; we can state the sound and complete systems for necessity as a predicate corresponding to certain types of frames; our treatment of transitive converse wellfounded frames can be seen as a variant of the revision theory of truth.

We regard this paper as a preliminary view on the issues sketched above. We also omit the more involved proofs, which we shall give in ^{\underline{hlw}} [17], but we outline some of the essential ideas.

§2. Formal Development. In this section we develop formally the account set out in the previous section.

L_{PA} is the language of arithmetic; L_{□} is L_{PA} augmented by the oneplace predicate symbol □. We shall identify L_{PA} with the set of all arithmetical formulæ and L_{□} with set of all formulæ that may contain □. We do not distinguish between expressions (like formulæ and terms) and their arithmetical codes. We use uppercase roman letters A, B, … for sentences of L_{□}. If a formula may have a free variable we always indicate this by writing A(v) etc.

We shall assume that the language L_{PA} features certain function symbols. This will render the notation somewhat more perspicuous. Of course, these function symbols can be eliminated in the usual way and thus are not really required.

On our account all arithmetical truths come out necessary. Thus one might wish to include further vocabulary that allows for more contingent sentences, but we shall only do so later, in order to keep the exposition of the main definitions and results as simple as possible. Once they have been established they can be carried over easily to languages with additional vocabulary.

We shall consider standard models only, i.e., worlds with the set of natural numbers in the domain and the standard interpretation of the arithmetical vocabulary. Hence models for L_{□} have the form (ℕ, X) where ℕ = ⟨ℕ, +, ×, 0,′ , … ⟩ is the standard model of arithmetic and X ⊆ ω the extension for □. Since models differ only in the extension of □, we may identify such a model with an extension for □. Thus we write X ⊧ A for (ℕ, X) ⊧ A.

◇x is defined as ¬□¬.x where ¬. is a function symbol for the function sending the code of a sentence of L_{□} to the code of its negation.

The definition of frames and possible worlds models (PW-models, for short) parallels the usual definitions for the operator approach as given, e.g., in Hughes and Cresswell ^{\underline{Hug96}} [19, p. 37f.] Boolos ^{\underline{Boo93}} [6].

Definition 2.1. A frame is an ordered pair ⟨W, R⟩ where W is nonempty and R is a binary relation on W.

The elements of W are called worlds, R is the accessibility relation. w sees v if and only if and only if wRv; alternatively we say that w is below v.

defi Definition 2.2. A PW-model is a triple ⟨W, R, V ⟩ such that ⟨W, R⟩ is a frame and V assigns to every w ∈ W a subset of L_{□} such that the following condition holds:

V (w) = {A ∈ L_{□}| ∀u(wRu ⇒ V (u) ⊧ A)}

If ⟨W, R, V ⟩ is a model, we say that the frame ⟨W, R⟩ supports the PWmodel ⟨W, R, V ⟩ or that ⟨W, R, V ⟩ is based on ⟨W, R⟩. A frame ⟨W, R⟩ admits a valuation if there is a valuation V such that ⟨W, R, V ⟩ is a PWmodel.

V assigns to every world a set of sentences, the extension of □ at that world. The condition on the function V in the definition says that a sentence is in the extension of □ at a world w if and only if it is true in all worlds seen by w. Thus if ⟨W, R, V ⟩ is a PW-model, the following holds:

V (w) ⊧□⌜A⌝ iff ∀v ∈ W (wRv ⇒ V (v) ⊧ A)

If we had to include further ‘contingent’ vocabulary, the valuation V had not only to interpret □ but also this additional vocabulary. Since we are only concerned with the language L_{□}, V needs to interpret only □ at every world and therefore it needs to assigning only a set of sentences to every world, i.e., the extension of □ at the world.

As pointed out above, the definition of truth at a world cannot be carried out recursively as in the operator case. On the operator account one can build models on every frame. Thus the question whether a frame supports a model does not arise for □ as an operator. For this problem is trivial: every frame admits a model for □ as an operator. However, if □ is a predicate, there are restrictions and the following question is sensible:

Characterisation Problem. Which frames support PW-models?

An answer to this problem exhibits the restrictions imposed by the ‘paradoxes’ (like Montague’s) on possible worlds semantics for predicates. We are only able to present partial solutions to the Characterisation Problem in this paper.

We shall now show that possible worlds semantics for predicates is in many respect similar to the usual possible worlds semantics for operators.

Analogous definitions of frames and models for operators lead to the so called normal systems of modal logic with the minimal system K (see, e.g., Boolos ^{\underline{Boo93}} [6]). These systems are closed under necessitation and the necessity operator □ distributes over material implication. For the predicate account something similar can be shown.

normality Lemma 2.3 (Normality). Suppose ⟨W, R, V ⟩ is a PW-model, w ∈ W and A, B ∈ L_{□}. Then the following holds:

(i) If V (u) ⊧ A for all u ∈ W, then V (w) ⊧ □⌜A⌝. (ii) V (w) ⊧□⌜A → B⌝ → (□⌜A⌝ → □⌜B⌝)

Since we are dealing with standard models only, we do not only obtain schemata like (ii) but also their universal closure, that is

∀x∀y(Sent_{L_{□}}(x) ∧ Sent_{L_{□}}(y) → □(x\overrightarrow{.}y) → (□x → □y))

ergerg (1)

\overrightarrow{.} represents the function that yields, when applied to two codes of sentences, their material implication. Sent_{L_{□}}(x) represents the set of sentences of L_{□}. In order to avoid confusing notation, we shall state schemata like (ii) instead of the universally quantified sentences like ^{\underline{ergerg}} 1. This does not make a difference because of the use of standard models.

limit

§3. Some Limitative Results. In order to illustrate the limitations imposed by the main condition in Definition ^{\underline{defi}} 2.2, we present some examples of frames that do not support PW-models.

As has been noted in the introduction, several restrictions on the class of frames supporting a PW-model are known. These restrictions correspond to several well known inconsistency results.

mezzo Example 3.1 (Montague). If ⟨W, R⟩ admits a valuation, then ⟨W, R⟩ is not reflexive.

The trivial proof resembles Montague’s proof showing that the predicate version of the modal system T is inconsistent.

Montague’s theorem is a generalisation of Tarski’s theorem which says that the scheme □⌜A⌝ ↔ A for all sentences A ∈ L_{□} is inconsistent with a theory proving diagonalisation. The possible worlds analogue of the scheme □⌜A⌝ ↔ A is a frame with only one world that sees itself. Of course, such a frame does not admit a valuation, because the frame is reflexive, and thus Example ^{\underline{mezzo}} 3.1 implies the possible worlds analogue of Tarski’s theorem which states that a frame with one single reflexive world seeing itself does not support a PW-model.

The arguments showing that a frame does not admit a valuation proceed by diagonal arguments (in our last example by a Liar sentence).

McGee’s main theorem in ^{\underline{McG85}} [21] on the ω-inconsistency of a certain theory of truth imposes a restriction on the existence of PW-models based on a non-transitive frame. Pred is the predecessor relation: for any natural number n it holds only between n and n + 1.

⋮2[u]1[u]0[u]

mcgee Example 3.2 (McGee, Visser). ⟨ω, Pred⟩ does not support a PW-model.

In order to prove this, one can adapt McGee’s proof in ^{\underline{McG85}} [21]), which uses a certain self-referential sentence with quantification. Instead of McGee’s theorem Visser’s theorem ^{\underline{Vis89}} [33] on illfounded hierarchies of languages can be used for deriving the above result. The relations between the different ω-inconsistency results and their implications is studied by Leitgeb ^{\underline{Lei01}} [20].

Also Gödel’s Second Incompleteness Theorem can be rephrased in terms of possible worlds semantics. One may prove an analogue of Löb’s Theorem, which will be very useful in latter sections.

Transitivity yields the predicate analogue of the 4 axiom:

K4 Lemma 3.3. Let ⟨W, R, V ⟩ be PW-model based on a transitive frame.

Then

V (w) ⊧□⌜A⌝ → □⌜□⌜A⌝⌝

obtains for all w ∈ W and all sentences A ∈ L_{□}.

loeb Lemma 3.4 (Löb’s Theorem). For every world w in a PW-model based on a transitive frame and every sentence A ∈ L_{□} the following holds:

V (w) ⊧□⌜□⌜A⌝ → A⌝ → □⌜A⌝

The proof is just the usual proof of Löb’s Theorem with the provability predicate replaced by the primitive symbol □.

Löb’s Theorem is a kind of an induction principle (see Boolos ^{\underline{Boo93}} [6]). Since we cannot assign arbitrary truth values to the sentences of L_{□} in any given world, we cannot conclude that R is converse wellfounded in general.

We shall also use the following version of Löb’s Theorem: unformloeb Corollary 3.5. Assume ⟨W, R⟩ is transitive and A ∈ L_{□}. If V (w) ⊧

□⌜A⌝ → A for all w ∈ W, then also V (w) ⊧ A for all worlds w.

From (the modal version of) Löb’s Theorem ^{\underline{loeb}} 3.4 (the modal version of) Gödel’s Second Incompleteness Theorem can be derived by setting A = ⊥ for a fixed contradiction ⊥. A dead end is a world that does not see any world. V (w) ⊧ □⌜⊥⌝ holds if and only if w is a dead end. It follows:

ultimo Example 3.6 (Gödel’s Second Incompleteness Theorem). In a transitive frame admitting a valuation every world is either a dead end or it can see a dead end.

Proof. Since the frame is transitive the predicate analogue of the 4 axiom scheme holds. This suffices for a proof of the formalized incompleteness theorem and we obtain V (w) ⊧□⌜⊥⌝ ∨ ◇⌜□⌜⊥⌝⌝. ⊣

In the sequel we shall provide a theorem (Theorem ^{\underline{atleastnt}} 6.1) that implies all the above results and does away with the need for all the different diagonal sentences.

tf

§4. Inductive Definitions of Valuations. A world w is converse wellfounded in a frame ⟨W, R⟩ if and only if every subset of {v| wR^{∗}v} has an R-maximal element, where R^{∗} is the transitive closure of R. A set of worlds is converse wellfounded if and only if all its elements are converse wellfounded. A set W′ ⊆ W of worlds is converse wellfounded if and only if {u ∈ W | ∃v ∈ W′(u = v ∨ vRu} is wellfounded with respect to R^{−1}.

So far we did not show that there exist any PW-models. As Belnap and Gupta ^{\underline{Bel93}} [5, Theorem 6E.5] have shown, the extension of □ can easily be defined by recursion on R^{−1} in converse wellfounded frames. It applies also to frames that are not transitive.

v Theorem 4.1. If ⟨W, R⟩ is converse wellfounded, then ⟨W, R⟩ admits exactly one valuation V.

Proof. The extension for □ is defined by transfinite recursion on R^{−1}. Assume V (v) has been defined for all v such that wRv. Then V (w) is

defined in the obvious way:

V (w) := {A ∈ L_{□}| ∀v(wRv ⇒ V (v) ⊧ A}

Clearly there is no choice in the definition of V (w), which is thus uniquely determined. ⊣

As we shall show later, there are frames that admit more than one valuation. Of course, these frames are converse illfounded (i.e., not converse wellfounded) .

We turn to the transitive frames and investigate the following special case of Characterisation Problem: which transitive frames support PWmodels? Throughout the rest of the section we assume that ⟨W, R⟩ is transitive.

In order to fit the present definition in the general framework of inductive definitions, it is convenient to define the extension of ◇ rather than the extension of □. The choice of ◇ as the basic predicate does not make a difference, because □ and ◇ are interdefinable in the following way:

□x :⟺ ¬◇¬.x
◇x :⟺ ¬□¬.(x)

We employ the following operation ^{◇} turning an extension of □ into the corresponding extension of ◇ and vice versa:

X^{◇} = {A ∈ L_{□}| ¬A ∉ X}

We have X^{◇◇} = X for deductively closed X.

We define a satisfaction relation ⊧_{◇}:

(ℕ, X) ⊧_{◇} A :⟺ (ℕ, X^{◇}) ⊧ A

Thus (ℕ, X^{◇}) ⊧_{◇} A holds if and only if (ℕ, X) ⊧ A. Usually we shall write Y ⊧_{◇} A for (ℕ, Y) ⊧_{◇} A.

Definition 4.2. We define an operator Φ whose domain is all sets of Gödel numbers of sentences of L_{□}: X ↦ Φ(X).

Φ(X) := X ∪ {A ∈ L_{□}| (ℕ, X) ⊧_{◇} A}

The operator Φ is not monotone, that is, X ⊆ Y does not generally imply Φ(X) ⊆ Φ(Y). For instance ¬◇⌜0 = 0⌝ is an element of Φ(Ø), but it fails to be an element of Φ({0 = 0}). In the following, Φ^{α}(X) designates the α-fold application of Φ to X; at limit ordinals λ, Φ^{λ}(X) is defined as the union ⋃_{α<λ} Φ^{α}(X) of all previous stages. Clearly then: for any X α < β → Φ^{α}(X) ⊆ Φ^{β}(X); there is a least κ such that Φ^{κ}(Ø) = Φ^{α}(Ø) for all α ≥ κ.

match Lemma 4.3. Assume ⟨W, R, V ⟩ is a PW-model based on a transitive converse wellfounded frame. If w has R^{−1}-rank α, then V (w)^{◇} = Φ^{α}(Ø).

The hierarchy of sets Φ^{α}(Ø) of sentences for all ordinals α may be seen as a transitive version of revision semantics as introduced by Gupta \underline{Gup82} [13] and Herzberger ^{\underline{Her82}} [18] (see Belnap and Gupta ^{\underline{Bel93}} [5]). For finite levels we can model revision in our possible–worlds semantics in the following way. Now think of our ◇ as something like the truth predicate. In the revision semantics the revision operator yields applied to a set X the set of sentences that are true if the truth predicate is interpreted by X. Thus in our notation the revision operator Γ may be rephrased as

A ∈ Γ(X) :⟺ X ⊧_{◇} A

In contrast to the situation with Φ, X ⊆ Γ(X) does not hold. The liar sentence, for instance, will be in Γ^{n}(Ø) if n is odd and it will not be in any Γ^{2n}(Ø). Thus the sequence (Γ^{n}(Ø))_{n∈ω} of sets of sentences does not

Is this itself a converge, whilst (Φ^{n}(Ø))_{n∈ω} converges to Φ^{ω}(Ø) = ⋃_{n<ω} Φ^{n}(X). controversial statement!?(PDW)→ Maybe this and the previous para. can be omitted? I am not sure what it brings to the discussion here?

The definition of the limit stages Γ^{λ}(Ø) for the revision operator is the central controversial problem of revision semantics. If we force (Γ^{n}(Ø))_{n∈ω} to converge by taking not Γ(X) but Γ(X) ∪ X at every step we obtain our operator Φ.

A set X ⊆ L_{□} is a fixed point (of Φ) if and only if Φ(X) = X. Since Φ is not monotone, Φ^{κ}(Ø) is not necessarily the smallest fixed point.

fixref Remark 4.4. X ⊆ L_{□} is a fixed point if and only if X ⊧_{◇} □⌜A⌝ → A (or, equivalently, X ⊧_{◇} A → ◇⌜A⌝) for all A ∈ L_{□}.

The existence of fixed points implies that there are frames that are converse illfounded but which admit a valuation nevertheless, as we shall show in the following theorem.

In order to state the theorem, we need some definitions. The converse wellfounded part of a set of the form {v| wRv} is the largest R-upwards closed set X (i.e., the largest X such that ∀y ∈ X(yRx ⇒ x ∈ X)) on which R^{−1} is wellfounded. The depth of a world w is the rank of R^{−1} restricted to the converse wellfounded part of {v| wRv}. Obviously the depth is defined also for converse illfounded worlds. We shall apply these notions only to transitive frames.

hoch Theorem 4.5. Assume ⟨W, R⟩ is transitive and every converse illfounded world in ⟨W, R⟩ has depth at least κ. Then ⟨W, R⟩ admits a valuation.

Proof. The definition of V for converse wellfounded w is forced by Lemma ^{\underline{match}} 4.3. If w ∈ W has depth at least κ we put V (w) = Φ^{κ}(Ø). This holds in particular for all converse illfounded worlds.

As κ is a fixed point, the condition

V (w) = {A ∈ L_{□}| ∀u(wRu ⇒ V (u) ⊧ A)}

is satisfied by all worlds w ∈ W. ⊣ This and Löb’s Theorem imply the following corollary:

undef Corollary 4.6. If ⟨W, R, V ⟩ is a transitive converse illfounded model, then there is no formula A that holds exactly in the converse wellfounded worlds of ⟨W, R⟩.

Using an ordinal notation system for the ordinals below ω_{1}^{CK}, the first non-recursive ordinal (see Rogers ^{\underline{Rog67}} [28]), it is possible to construct for each α < ω_{1}^{CK} sentences that hold at a world w of a transitive frame if and only if the world is converse wellfounded and w has depth α. However, in general one cannot express converse wellfoundedness in L_{□} according to Corollary ^{\underline{undef}} 4.7.

In the following we determine the closure ordinal κ of Φ and thereby show that there is a gap between ω_{1}^{CK} and κ.

We abbreviate by setting X_{α} = Φ^{α}(Ø). The function δ ↦ X_{δ} can be defined by a Σ_{1}-recursion over any sufficiently closed model M containing the standard model ℕ of arithmetic. In particular this is true over any model M of Kripke-Platek (KP) set theory containing the integers as a standard set. Transitive models of KP are called admissible sets. An ordinal α is admissible if L_{α} is a model of KP. ADM is the set of all admissible ordinals greater than ω. ADM^{∗} is the class ADM together with its limit points.

The idea of the proof of the following theorem is that for infinite ordinals δ below the closure ordinal κ of this operation, the sets X_{δ+1} can be construed essentially as truth sets for the δ’th level of the L-hierarchy. The point where this identification breaks down is precisely where the L-hierarchy requires parameters in the first order definitions that are required to make up the elements of the next level.

Let γ be least so that L_{γ} has a transitive Σ_{1}-end extension (that is, there is a transitive M with L_{γ} as an element, and ⟨L_{γ}, ∈⟩ ≺_{Σ_{1}} ⟨M, ∈⟩). Then one may show the following facts: (i) that ⟨L_{γ}, ∈⟩ ≺_{Σ_{1}} ⟨L_{γ+1}, ∈⟩ and (ii) that L_{γ} is an admissible set that is the Skolem Hull of Σ_{1} parameter free terms inside itself. Thus any element x of L_{γ} is named by a parameter free Σ_{1} Skolem term, and the ∈-diagram of L_{γ} is essentially given by the Σ_{1}-truth set for L_{γ}. This fails first at L_{γ+1}. (For background on the theory KP and on admissible sets, see Barwise ^{\underline{Bar75}} [3].) These two facts are used in the proof of ^{\underline{g=k}} 4.8 below.

It is also well known that γ is least so that L_{γ} is first-order reflecting, that is, for all n, if φ is any Π_{n} formula (with parameters from L_{γ} allowed) in the language of set theory, then the following holds (see Aczel ^{\underline{Acz73}} [1]):

L_{γ} ⊧ φ ⟹ ∃α < γ L_{α} ⊧ φ

The proof theoretic strength of this ordinal lies strictly between ACA + → Bar Induction + Δ_{2}^{1}-Comprehension Scheme, and the latter strengthened with the Π_{2}^{1}-Comprehension Scheme — see Rathjen ^{\underline{Rat94}} [26].

g=k Theorem 4.7. γ = κ.

In particular, this shows that κ > ω_{1}^{CK} (ω_{1}^{CK} is Π_{2}-reflecting but not Π_{3}-reflecting).

For A an admissible set we let WFP(A) denote the wellfounded part of A, that is, the largest structure B ⊆ A such that ∈↾ |B| × |B| is wellfounded. If α is the ordinal rank of the wellfounded part WFP(A), then it is known that L_{α} ⊧ KP. If A is a model of KP, On(A) denotes the class of ordinals in the sense of A. We identify the standard part of On(A) with the standard ordinals. Hence On(WFP(A)) ⊇ ω + 1 holds if and only if the integers of A are standard. We shall only have to consider in what follows admissible sets in which the integers are standard.

We can prove the following existence theorem for valuations, which yields valuations for converse illfounded frames if it is applied to nonstandard models A of KP.

pc Theorem 4.8. If ⟨W, R⟩ is transitive, A is a model of KP, ⟨W, R⟩ ∈ A and “if w ∈ ⟨W, R⟩ is converse illfounded then its depth is greater than the closure ordinal of the operator Φ” holds in A, then ⟨W, R⟩ admits a valuation.

Note: there is no requirement that the model A be wellfounded in the above. The theorem is the non-standard counterpart to Theorem \underline{hoch} 4.6 (which it generalises). The point is simply the observation that the operation w ↣ X_{w}, for w ∈ W, is sufficiently absolute between A and the universe of all sets, that the valuation defined by a Σ_{1}-recursion inside A really does serve as a true valuation.

anc

§5. A Necessary Condition for the Existence of a Valuation. As we have explained above, a frame need not be converse wellfounded for it to admit a valuation. However, Löb’s Theorem can be employed for showing the following:

atleast Theorem 5.1. Let ⟨W, R, V ⟩ be a transitive model. Then the following must hold for the depth α of every converse illfounded world in ⟨W, R⟩: either α ∈ ADM^{∗} or α ≥ κ.

The partial characterisation of the class of transitive frames admitting valuations yielded by Lemma ^{\underline{atleast}} 5.1 and Theorem ^{\underline{hoch}} 4.6 is incomplete because it does not say whether worlds of depth α with ω_{1}^{CK} ≤ α ≤ κ have to be converse wellfounded. Proposition ^{\underline{ogeht}} 5.2 shows that for any admissible ordinal α > ω, there exists frames with converse illfounded worlds of depth α.

→ To summarise: For the following classes of transitive frames ⟨W, R⟩: (i) If every world w ∈ W has a depth α < ω_{1}^{CK} then R is converse wellfounded iff ⟨W, R⟩ admits a valuation; (ii) if every converse illfounded world has depth α ≥ κ (without any restriction being placed on the ordering R for the part containing those worlds of depth ≥ κ, i.e., arbitrary loops and infinitely descending chains are possible) then the frame admits a valuation. Thus for frames where all depths are smaller than ω_{1}^{CK} or larger than κ the Characterisation Problem for transitive frames is settled. Between these two ordinals the depth of every converse illfounded world of a transitive frame admitting a model must be admissible or a limit of admissibles according to Theorem ^{\underline{atleast}} 5.1. In the next proposition we shall see that there actually are frames admitting models with converse illfounded worlds of depth ω_{1}^{CK}. Thus converse illfounded worlds occur as low as allowed possible by Theorem ^{\underline{atleast}} 5.1.

In the following proposition WFP(R^{−1}) denotes the largest wellfounded initial segment of R^{−1}.

npu ogeht Proposition 5.2. For any α ∈ ADM there is a model ⟨W, R, V ⟩ with R^{−1} illfounded, with WFP(R^{−1}) ≅ α and V (w) is a fixed point for some w ∈ W.

This follows from Barwise’s ^{\underline{Bar75}} [3] Compactness Theorem and the fact that for any countable ordinal α ∈ ADM there is an illfounded model with a wellfounded initial part of order type α.

We conclude this section with a note on the uniqueness of valuations. Are there two distinct PW-models based on the same frame? That is,

are there frames that admit at least two distinct valuations? Converse wellfounded frames have exactly one valuation by Theorem ^{\underline{v}}4.1; thus the valuation is always unique. Therefore two valuations for the same frame can differ only on converse illfounded worlds. One can show the following by employing illfounded models of KP.

Theorem 5.3. There is a linearly ordered frame ⟨W, R⟩ which admits two different valuations V, V′.

§6. The General Characterisation Problem. So far we have focused on transitive frames. In this section we generalise some results to other frames.

Theorem ^{\underline{atleast}} 5.1 yields information also on frames that are not transitive. For the transitive closure of R can be defined within the language L_{□}.

atleastnt nt Theorem 6.1. If ⟨W, R⟩ supports a PW-model, then in the transitive closure of ⟨W, R⟩ every converse illfounded world in W has depth α with α ∈ ADM^{∗} or α ≥ κ.

Theorem ^{\underline{nt}} 6.1 can be used for demonstrating that the frame ⟨ω, Pred⟩ in Example ^{\underline{mcgee}} 3.2 does not admit a valuation. Thus Theorem ^{\underline{nt}} 6.1 implies all negative results in § ^{\underline{limit}} 3. Therefore, in a sense, Löb’s Theorem implies the possible worlds analogues of Tarski’s, Montague’s, McGee’s and Visser’s theorems. In § ^{\underline{completeness}} 7 we shall show how to get from these analogues back to ω-inconsistency results.

By Theorem ^{\underline{hoch}} 4.6 a transitive frame admits a valuation if every converse illfounded world w ∈ W has at least depth κ. One might hope to generalise Theorem ^{\underline{hoch}} 4.6 by showing that a frame admits a valuation if all converse illfounded worlds are of depth at least κ in the transitive closure of the frame. However, this generalisation fails. Thus there is no characterisation of the class of frames that admit valuations in terms of the transitive closure of the frames.

Theorem 6.2. There are frames that do not support a PW-model, although their transitive closure does.

Obviously, if ⟨W, R, V ⟩ is a PW-model and wRw, then V (w) is a fixed point of Φ. So far we have used only the fixed point Φ^{κ}(Ø). However, other fixed points of Φ are required for valuations of certain frames that are not transitive. There is a model with two reflexive worlds v and w such that V (v) ≠ V (w). Again we omit the proofs.

completeness

§7. Completeness. In modal logic completeness theorems play a central role. For instance, the sentences valid in all frames at all words under any valuation are exactly the theorems of the modal system K. Similarly, the system K4 is associated with the class of transitive frames, the Gödel system G with the class of converse wellfounded frames (see Boolos ^{\underline{Boo93}} [6]). Can we obtain analogous results in our setting?

Since we are dealing with standard models only, the set of all sentences valid in all PW-models ⟨W, R, V ⟩ contains all arithmetical truths and is closed under the ω-rule. Of course this set is not recursively enumerable.

fdsdf Definition 7.1. A set T h of sentences of L_{□} is □-closed if and only if

it satisfies the following conditions:

(i) T h contains PA and is closed under logic, necessitation and the ωrule:

\frac{A(\overline{0}), A(\overline{1}), A(\overline{2}), …}{∀xA(x)}

(ii) □⌜A → B⌝ → (□⌜A⌝ → □⌜B⌝) is in T h for all A and B in L_{□}. (iii) All instances ∀x□⌜A(ẋ)⌝ → □⌜∀xA(x)⌝ of the Barcan formula (i.e.,

the formalised ω-rule) are in T h for all formulæ A(v) of L_{□}. For a set T h of sentences of L_{□} we write (ℕ, S) ⊧ T h if for all sentences

A ∈ L_{□} (ℕ, S) ⊧ A holds.

completenesst Theorem 7.2 (Completeness). If T h is □-closed and consistent, then there is a PW-model ⟨W, R, V ⟩ such that (ℕ, V (w)) ⊧ T h holds for all w ∈ W.

Our completeness proof resembles the usual proofs for operator modal logic (see, e.g., Chagrov and Zakharyaschev ^{\underline{Cha97}} [9, chapter 5]). However, since we are dealing with standard models only, we have to employ ωlogic rather than pure first-order logic.

From the Completeness Theorem we can also derive several inconsistency results. For instances, we can prove that the truth theory FS in Halbach ^{\underline{Hal94}} [14], which is equivalent to a system introduced by Friedman and Sheard ^{\underline{Fri87}} [11], is inconsistent in ω-logic. Here we present still another example.

D is the smallest □-closed set containing all instances of □⌜A⌝ → ◇⌜A⌝ for all A ∈ L_{□}. Obviously D is the predicate analogue plus the ω-rule of the system D of deontic logic. Note that, according to the definition of D, the ω-rule and the rule of necessitation may be applied to consequences of □⌜A⌝ → ◇⌜A⌝ for all A ∈ L_{□}.

D Example 7.3. D is inconsistent.

This follows from the Completeness Theorem and the fact that every frame admitting a PW-model contains a dead end, which contradicts the axiom scheme □⌜A⌝ → ◇⌜A⌝ of D.

If the ω-rule is dropped from D the system becomes consistent (though ω-inconsistent because of McGee’s ^{\underline{McG85}} [21] result) because it is a subtheory of the consistent system FS of Halbach ^{\underline{Hal94}} [14].

We define the predicate counterparts of the operator modal systems K and K_{4}.

Definition 7.4. K is the smallest □-closed set. K_{4} is the smallest □-closed set that contains all instances of □⌜A⌝ → □⌜□⌜A⌝⌝.

By applying the theorem to T h = K and T h = K_{4} we get the following two corollaries:

K Corollary 7.5. The following are equivalent for all A ∈ L_{□}:

(i) A is valid at all worlds in all PW-models, i.e., V (w) ⊧ A for all PW-models ⟨W, R, V ⟩ and w ∈ W.

(ii) A is in K.

Proof. In order to prove that (i) implies (ii), we apply our Completeness Theorem. If A ∉ K there is a world w in the PW-model ⟨W, R, V ⟩ constructed in the proof of the completeness result such that A ∉ w, i.e., V (w) |̸= A.

The Normality Lemma 2.3 ensures that (ii) implies (i). ⊣ We obtain also an analogous result for K_{4}:

cK4 Corollary 7.6. The following are equivalent for all A ∈ L_{□}:

(i) A is valid at all worlds in all transitive PW-models, i.e., V (w) ⊨ A for all PW-models ⟨W, R, V ⟩ and w ∈ W.

(ii) A is in K_{4}.

Not all completeness theorems known from operator modal logic carry over to their predicate counterparts. For instance, the logic G obtained from K_{4} by adding the operator version □(□p → p) → □p is complete with respect to the class of all transitive converse wellfounded frames. The predicate system K_{4} has Löb’s Theorem already as a theorem. However, it does not prove all sentences valid in all transitive converse wellfounded frames, as we shall show now by recursion-theoretic considerations, more precisely by comparing the complexities of K_{4} and the fixed point Φ^{κ}(Ø).

By Corollary ^{\underline{cK4}} 7.6 K_{4} is the set of sentences valid in all transitive PWmodels; Φ^{κ}(Ø)^{◇} is the set of all sentences valid in a all transitive converse wellfounded PW-models. Therefore Φ^{κ}(Ø) is a subset of K_{4}. We shall show that the converse does not hold: there are sentences that are valid in all transitive converse wellfounded PW-models but that fail at a world of some transitive converse illfounded PW-model. In particular, Corollary \underline{cK4} 7.6 does not hold if (i) is restricted to converse wellfounded frames.

K_{4} is obviously Π_{1}^{1}. The following Theorem shows that Φ^{κ}(Ø) has a much higher complexity than K_{4}. Thus converse illfounded PW-models really do matter.

delta12 Theorem 7.7. The set Φ^{κ}(Ø) is Δ_{2}^{1} but neither Σ_{1}^{1} nor Π_{1}^{1}.

exp

§8. Extensions to Other Languages and Ground Models. In this section we generalise our approach and the methods developed so far to languages extending L_{□}.

Our results carry over to acceptable models in a straightforward way. Thus we can use other well behaved models M (with the appropriate language L_{M}) instead of the standard model of arithmetic. In this case □ has to be conceived as a relation obtaining between formulas and variable assignments. Thereby we introduce genuine de re–modality.

Definition 8.1. Let M = ⟨M, R, …⟩ be any structure. Let κ_{M} be the least ordinal so that L_{κ_{M}} (⟨M, R, …⟩) is the first level of the relativised Gödel L-hierarchy built over M, using elements of M as urelemente, which is first order reflecting.

The methods of § ^{\underline{tf}} 4 can be used to show the following. Let M be a countable acceptable structure (in the sense of ^{\underline{Mos74}} [23], that is essentially M has a definable coding scheme). Consider the class of frames where now ℕ has been replaced by M at each world of the frame. One may show:

(i) The fixed point Φ^{κ_{M}}(Ø) occurs in sufficiently long converse wellfounded frames ⟨W, R⟩ at the ordinal κ_{M}.

(ii) We may look at admissible sets A over the structure M (much as Barwise does in ^{\underline{Bar75}} [3], and take orderings R ∈ A with A ⊧ “R^{−1} is wellfounded” and construct valuations V for the worlds of W.

(iii) The Characterisation Theorem ^{\underline{atleastnt}} 6.1 of the wellfounded parts of frames admitting valuations holds with κ replaced by κ_{M} and the class ADM replaced by ADM(M) - the class of ordinals admissible with respect to the structure M.

In general the results of § ^{\underline{tf}} 4 and § ^{\underline{anc}} 5 go through mutatis mutandis. The formulæ of the language L_{M} are interpreted in every world in

the same way. In particular, in the special case L_{M} = L_{PA} we have considered in the previous sections, the arithmetical vocabulary does not allow for any variation in its evaluation, at least not on our account: it is interpreted in every world by the standard model.

Moreover, we could allow the universe to vary from world to world, as long as the codes of sentences and codes of sequences of all objects existing in the respective world are in the universe. However, we do not go that far afield from our original approach and we illustrate the effects of contingent vocabulary by considering a slight modification of our approach with L_{PA}. For our simple examples we need only an extension of L_{PA} by an additional propositional parameter.

Let L_{PA}^{p} be the language L_{PA} of arithmetic extended by an additional propositional variable p. By adding □ we obtain the language L_{□}^{p}. A PW-model is defined as in Definition ^{\underline{defi}} 2.2 except that V has also to tell whether p is true at that world. More precisely V (w) is a pair ⟨S, k⟩ where S ⊆ L_{□}^{p} is the extension of □ and k is the truth value 0 or 1 of p at w. If V (w) = ⟨S, k⟩, S has to satisfy the following condition:

S = {A ∈ L_{□}^{p}| ∀u(wRu ⇒ V (u) ⊧ A}

Of course V (u) ⊧ A for A ∈ L_{□}^{p} is defined in the obvious way.

In the following theorem we show that we are not completely free to assign truth values to p if the frame is converse illfounded.

p Proposition 8.2. Assume ⟨W, R⟩ supports a PW-model. Then the transitive closure of a frame ⟨W, R⟩ is converse wellfounded if and only if it allows for arbitrary interpretations of p.

By the latter we mean that given a frame and given a function g : W → {0, 1} we have a model ⟨W, R, V ⟩ based on that frame such that for all w ∈ W and some S ⊆ L_{□}^{p} the equation V (w) = ⟨S, g(w)⟩ holds.

Proof. Assume that the frame is transitive.

Löbs Theorem ^{\underline{loeb}} 3.4 applies also to p, that is, the following holds for any valuation V and world w:

V (w) ⊧□⌜□⌜p⌝ → p⌝ → □⌜p⌝

By stipulating V (w) ⊧p for converse wellfounded w and V (w) ⊧¬p for converse illfounded w, one can exclude converse illfounded worlds for transitive frames (see Boolos ^{\underline{Boo93}} [6, p. 75f] and Corollary ^{\underline{undef}} 4.7).

Since the transitive closure of R can be defined in L_{□}, the argument can be generalised to non-transitive frames. ⊣

Although we are not completely free to evaluate p in any world of a converse illfounded model in any arbitrary way, we can use p in order to express certain features of the frame (for instance, we can force a frame to branch). Here we do not explore what can be expressed with additional vocabulary, but it should be obvious that interesting conditions are expressible with more propositional parameters and by quantifying over these parameters.

If we allow also for additional objects in every world beyond the natural numbers and we change our setup accordingly, we shall encounter the usual problems of quantified modal logic. In particular, the Barcan formula will fail if we allow for increasing domains etc.

Each of these extensions is worth to be studied and philosophically relevant – indeed these extensions are more relevant than the setting that we have followed: it is certainly not satisfying, from a philosophical point of view, to concentrate on worlds which are standard models of arithmetic with an additional interpretation of the necessity predicate. But independent of what language is chosen and what the set of worlds looks like semantically, if a modality is to be expressed by a predicate, then every world has to have an interpreted theory of syntax in the background, and that means that every world has to comprise arithmetic (modulo coding). Thus, we have actually concentrated on the minimal prerequisites of a possible worlds semantics for predicates, and that is why our results also apply to the philosophically more relevant cases.

§9. Some Preliminary Conclusions. In this final section we try to draw some conclusions from our results.

We have shown how all limitative results of § ^{\underline{limit}} 3 may finally be reduced to a single limitative result. The possible worlds analogues of Tarski’s, Montague’s, McGee’s, Visser’s theorems, which have been mentioned in § ^{\underline{limit}} 3, as well as the analogues of some results not mentioned here like those by Thomason ^{\underline{Tho80}} [32] and partially those by Friedman and Sheard \underline{Fri87} [11] may be reduced to the single condition on frames in Theorem ^{\underline{atleastnt}} 6.1. Löb’s Theorem is the origin of all the inconsistency and ω-inconsistency results. On the semantical side this is mirrored by the condition that any converse illfounded world must have a large depth; this condition excludes all simple loops, reflexive frames etc. from being frames that admit a PW-model. Thus we conclude that the mentioned paradoxes flow from a common source.

Our semantical investigations underline the central role of converse wellfoundedness of frames. Provability logic (see, e.g., Boolos ^{\underline{Boo93}} [6]) thus appears in a new light, at least to us. The main results of provability logic might be understood as suggesting that there is a profound relation between provability and converse wellfoundedness. In contrast, our results show that, if one sets up possible worlds semantics for predicates, converse wellfoundedness always plays an important role. All frames supporting a PW-model have to be converse wellfounded — except for worlds of great depth. Thus all predicates with reasonable possible worlds semantics are much like the provability predicate. This holds even in the absence of the transitivity axiom as Theorem ^{\underline{atleastnt}} 6.1 shows.

Surprisingly the condition of Theorem ^{\underline{atleastnt}} 6.1 does not rule out all converse illfounded models. As Theorem ^{\underline{delta12}} 7.7 shows, our completeness result Corollary ^{\underline{K}}7.5 for K would fail, if we restricted our attention to converse wellfounded models only. That is, K is incomplete with respect to the class Φ^{κ}(Ø)^{◇} of all converse wellfounded models. Consequently there are sentences that hold in all converse wellfounded models but fail at some converse illfounded model and are therefore not theorems of K. This shows that the common semantical source of the paradoxes is not precisely converse illfoundedness of the frames but rather the failure of the more complex condition stated in Theorem ^{\underline{atleastnt}} 6.1.

The condition of Theorem ^{\underline{atleastnt}} 6.1 implies that many frames familiar from operator modal logic do not support PW-models. In particular, the frames for T, S_{4} and S_{5}, i.e., all reflexive frames do not admit a valuation. It seems that we have to sacrifice the core systems of modal logic for the predicate approach. We do not conclude from this, however, that the predicate approach is mistaken altogether. We recommend to approach necessity and other notions much like truth in order to ban inconsistency from these notions. For truth a wide array of semantical and axiomatic approaches has been offered in the literature. For necessity there should be even more.

REFERENCES

[1] Peter Aczel and Wayne Richter, Inductive definitions and reflecting properties of admissible ordinals, Generalized recursion theory (Jens E. Fenstad and Peter Hinman, editors), North Holland, 1973, pp. 301–381.

[2] Nicholas Asher and Hans Kamp, Self-reference, attitudes, and paradox, Properties, types and meaning (Gennaro Chierchia, Barbara H. Partee, and Raymond Turner, editors), vol. 1, Kluwer, Dordrecht, 1989, pp. 85–158.

[3] Jon Barwise, Admissible sets and structures, Perspectives in Mathematical Logic, Springer Verlag, Berlin, 1975.

[4] George Bealer, Quality and concept, Clarendon Press, Oxford, 1982.

[5] Nuel Belnap and Anil Gupta, The revision theory of truth, MIT Press, Cambridge, 1993.

[6] George Boolos, The logic of provability, Cambridge University Press, Cambridge, 1993.

[7] Andrea Cantini, A theory of truth formally equivalent to ID_{1}, The Journal of Symbolic Logic, vol. 55 (1990), pp. 244–259.

[8] , Logical frameworks for truth and abstraction. an axiomatic study, Studies in Logic and the Foundations of Mathematics, vol. 135, Elsevier, Amsterdam, 1996.

[9] Alexander Chagrov and Michael Zakharyaschev, Modal logic, Oxford Logic Guides, Oxford University Press, Oxford, 1997.

[10] Solomon Feferman, Reflecting on incompleteness, The Journal of Symbolic Logic, vol. 56 (1991), pp. 1–49.

[11] Harvey Friedman and Michael Sheard, An axiomatic approach to selfreferential truth, Annals of Pure and Applied Logic, vol. 33 (1987), pp. 1–21.

[12] Patrick Grim, The incomplete universe: Totality, knowledge, and truth, MIT Press, Cambridge (Mass.), 1991.

[13] Anil Gupta, Truth and paradox, Journal of Philosophical Logic, vol. 11 (1982), pp. 1–60.

[14] Volker Halbach, A system of complete and consistent truth, Notre Dame Journal of Formal Logic, vol. 35 (1994), pp. 311–327.

[15] , Truth and reduction, Erkenntnis, vol. 53 (2000), pp. 97–126.

[16] , Semantics and deflationism, Habilitationsschrift, Universität Konstanz, 2001.

[17] Volker Halbach, Hannes Leitgeb, and Philip Welch, Possible worlds semantics for modal notions conceived as predicates, in preparation.

[18] Hans Herzberger, Notes on naive semantics, Journal of Philosophical Logic, vol. 11 (1982), pp. 61–102.

[19] G. E. Hughes and M. J. Cresswell, A new introduction to modal logic, Routledge, London and New York, 1996.

[20] Hannes Leitgeb, Theories of truth which have no standard models, Studia Logica, vol. 21 (2001), pp. 69–87.

[21] Vann McGee, How truthlike can a predicate be?, Journal of Philosophical Logic, vol. 14 (1985), pp. 399–410.

[22] Richard Montague, Syntactic treatments of modality, with corollaries on reflexion principles and finite axiomatizability, Acta Philosophica Fennica, vol. 16 (1963), pp. 153–167.

[23] Yiannis Moschovakis, Elementary induction on abstract structures, North-Holland, Amsterdam, 1974.

[24] Willard Van Orman Quine, Three grades of modal involvemen, The ways of paradox, Harvard University Press, Cambridge, Mass., revised and enlarged ed., 1976, pp. 158–176.

[25] , Intensions revisited, Contemporary perspectives in the philosophy of language (French, Uehling, and Wettstein, editors), University of Minnesota Press, Minneapolis, 1977, pp. 5–11.

[26] Michael Rathjen, Proof theory of reflection, Annals of Pure and Applied Logic, vol. 68 (1994), pp. 181–224.

[27] Jim des Rivières and Hector J. Levesque, The consistency of syntactical treatments of knowledge, Theoretical aspects of reasoning about knowledge: Proceedings of the 1986 conference (Los Altos) (Joseph Y. Halpern, editor), Morgan Kaufmann, 1986, pp. 115–130.

[28] Hartley Rogers, Theory of recursive functions and effective computability, McGraw–Hill Book Company, New York, 1967.

[29] Kurt Schütte, Proof Theory, Springer, Berlin , 1970.

[30] Michael Sheard, A guide to truth predicates in the modern era, The Journal of Symbolic Logic, vol. 59 (1994), pp. 1032–1054.

[31] Barry Hartley Slater, Natural language’s semantic closure, forthcoming.

[32] Richmond H. Thomason, A note on syntactical treatments of modality, Synthese, vol. 44 (1980), pp. 391–396.

[33] Albert Visser, Semantics and the liar paradox, Handbook of philosophical logic, vol. IV, Reidel, Dordrecht, 1989, pp. 617–706.

UNIVERSITÄT KONSTANZ

FACHGRUPPE PHILOSOPHIE

POSTFACH 5560 D 21

78434 KONSTANZ, GERMANY

E-mail: Volker.Halbach@uni-konstanz.de

UNIVERSITÄT SALZBURG

INSTITUT FÜR PHILOSOPHIE

FRANZISKANERGASSE 1

5020 SALZBURG, AUSTRIA

E-mail: Hannes.Leitgeb@sbg.ac.at

DEPARTMENT OF MATHEMATICS

UNIVERSITY OF BRISTOL

BRISTOL BS8 1TW, ENGLAND and

GRADUATE SCHOOL OF SCIENCE & TECHNOLOGY KOBE UNIVERSITY

ROKKO-DAI, NADA-KU KOBE 657, JAPAN

Current address: Institut für formale Logik, Währinger Str. 25, 1090 Wien, Austria E-mail: welch@kobe-u.ac.jp