POSSIBLE-WORLDS SEMANTICS FOR MODAL NOTIONS CONCEIVED AS PREDICATES

VOLKER HALBACH, HANNES LEITGEB, AND PHILIP WELCH

Abstract. If □ is conceived as an operator, i.e., an expression that gives applied to a formula another formula, the expressive power of the language is severely restricted when compared to a language where □ is conceived as a predicate, i.e., an expression that yields a formula if it is applied to a term. This consideration favours the predicate approach. The predicate view, however, is threatened mainly by two problems: Some obvious predicate systems are inconsistent, and possible-worlds semantics for predicates of sentences has not been developed very far. By introducing possible-worlds semantics for the language of arithmetic plus the unary predicate □, we tackle both problems. Given a frame ⟨W, R⟩ consisting of a set W of worlds and a binary relation R on W, we investigate whether we can interpret □ at every world in such a way that □⌜A⌝ holds at a world w ∈ W if and only if A holds at every world v ∈ W such that wRv. The arithmetical vocabulary is interpreted by the standard model at every world. Several ‘paradoxes’ (like Montague’s Theorem, Gödel’s Second Incompleteness Theorem, McGee’s Theorem on the ω-inconsistency of certain truth theories etc.) show that many frames, e.g., reflexive frames, do not allow for such an interpretation. We present sufficient and necessary conditions for the existence of a suitable interpretation of □ at any world. Sound and complete semi-formal systems, corresponding to the modal systems K and K4, for the class of all possible-worlds models for predicates and all transitive possible-worlds models are presented. We apply our account also to nonstandard models of arithmetic and other languages than the language of arithmetic.

Received by the editors October 9, 2002. Key words and phrases. Possible worlds, modal logic, necessity, paradox. We have presented parts of the paper in several talks; some of the results are pub-

lished in [19] without proofs. We thank the audiences and the referee of the latter paper for numerous suggestions and hints. We are also indebted to Christopher von Bülow for his suggestions and for correcting many typographical errors. The work of Volker Halbach was sponsored by the Department of Logic and Philosophy at the University of California at Irvine and the research group Logic in Philosophy at the University of Constance. Philip Welch would like to acknowledge the support of the Institut für Formale Logik, Vienna, where he held a Guest Professorship during the preparation of part of the paper.

2 VOLKER HALBACH, HANNES LEITGEB, AND PHILIP WELCH

[ …] semper denotatur quod talis modus verificetur de propositione illius dicti, sicut per istam ‘omnem hominem esse animal est necessarium’ denotatur quod iste modus ‘necessarium’ verificetur de ista propositione ‘omnis homo est animal’ cuius dictum est hoc quod dicitur ‘omnem hominem esse animal’[.]

William of Ockham, Summa Logicae II.9

§1. Predicates and Operators. Predicates applied to singular terms yield formulae, while operators need to be combined with formulae to give new formulae. Roughly speaking, in natural language and in the case of necessity “necessarily” and “it is necessary that” are operators, whereas “is necessary” is a predicate. Whether necessity, knowledge, belief, future and past truth, obligation and other modalitities should be formalised by operators or by predicates was a matter of dispute up to the early sixties between two almost equally strong parties. Then two technical achievements helped the operator approach to an almost complete triumph over the predicate approach that had been advocated by illustrious philosophers like Quine.

Montague [33] provided the first result by proving that the predicate version of the modal system T is inconsistent if it is combined with weak systems of arithmetic. From his result he concluded that “virtually all of modal logic … must be sacrificed”, if necessity is conceived as a predicate of sentences. Of course, Montague’s verdict does not imply that necessity cannot be treated as a predicate of objects different from sentences, e.g., propositions conceived as language-independent entities, but the result clearly restricted the attractiveness of the predicate approach.

The majority of philosophers and logicians have opted to spare modal logic and to reject the predicate view altogether. The prevailing general attitude is expressed by the following quote from Slater [43]:

Since Montague, we surely now know that syntactic treatments of modality must be replaced by operator formulations.

The other technical achievement that brought about the triumph of the operator view was the emergence of possible-worlds semantics. Hintikka, Kanger and Kripke provided semantics for modal operator logics, while nothing similar seemed available for the predicate approach.

Ever since possible-worlds semantics has reigned as the main tool in the analysis of necessity and the notions mentioned above. Today sacrificing possible-worlds semantics for the predicate conception of necessity etc. would mean sacrificing a huge body of philosophical logic and of analytic metaphysics, epistemology, ethics and computer science.

Nevertheless the operator approach suffers from a severe drawback: it restricts the expressive power of the language in a dramatic way because it rules out quantification in the following sense: There is no direct formalisation of a sentence like “All tautologies of propositional logic are necessary”.

Proponents of the operator approach have proposed several strategies to overcome this problem. For instance, one might formalise the above sentence by a scheme and transfer quantification into the metalanguage. However, this strategy hardly will be satisfying if it is applied to more complex sentences where the quantifiers are deeply embedded in the sentence.

Alternatively, one might employ a special kind of quantification where the above sentence can be formalised as ∀A (P (A) → □A), where P (x) is a predicate while □ still is an operator. Then even ∀A(P (A) → A) would be well formed because the variable A can stand in place of a formula. This kind of quantification often is called substitutional quantification, sometimes even if it does not come with any semantics but only with axioms and rules. This terminology is surely confusing, but it has become almost standard terminology after Kripke [27] had shown how to apply a substitutional interpretation of quantification with the mentioned properties. Substitutional quantification in this sense is not simple propositional quantification because the new variables may appear in the place of normal first-order variables as well.

It seems arbitrary that some notions are formalised as predicates, while others are conceived as operators only. It also forces one to switch between usual first-order quantification and substitutional quantification without any real need. In natural language there are not these two different kinds of quantification. We shall give an example. “All true Σ-sentences are provable in PA” requires only a first-order quantifier because provability and truth are predicates. “All true Σ-sentences are provable in PA and necessary”, in contrast, is formalised with another kind of quantification. But it is completely unclear why we should assume that in the latter sentence we deal with a completely different kind of quantification than in the first sentence.

In most cases the above kind of substitutional quantification will be equivalent to a truth predicate. If a truth predicate is employed, then one could stick to an operator for necessity in many cases. Instead of saying “x is necessary”, one could say “x is necessarily true”. Thus □x where □ is a predicate might be replaced by □Tx where □ is an operator and T is a truth predicate. One could even reverse the order of the truth predicate and the necessity operator (see Kripke [26]). Thus only a truth predicate (or substitutional quantification) would be needed, but otherwise operators would suffice.

We have several qualms about this approach. As above, we do not see any good reason to treat truth and necessity (and the other predicates) differently on the syntactical level. Furthermore the theory of necessity and other notions would rest on truth-theoretic foundations which are threatened by the semantical paradoxes. In general, the theory of truth is far from being settled and the theory of necessity would inherit all semantical paradoxes.

We think that the operator approach might have some merits for instance in linguistics and computer science, but it fails at its main application in philosophical logic: it does not provide an illuminating analysis for necessity, knowledge, obligation and so on. For it does not allow for the formalisation of the most common philosophical claims such as “All laws of physics are necessary” or “There are true but unknowable sentences”.

Of course, the rejection of substitutional quantification and the other strategies mentioned requires a more detailed discussion. However, we do not present it here but proceed to our own constructive proposals.

Even for those who adhere to the operator view our results might be interesting because the difficulties we encounter will show up in a different form if a proper account of substitutional quantification or a theory of truth is used in order to express quantification.

Our general reservations against the operator approach are shared by some philosophers (see also Bealer [4] for an overview). Thus along the main stream of the operator conception with its possible-worlds semantics there always has been a tiny but steady rill of work on the predicate view by authors like Germano [15], Skyrms [42], Asher and Kamp [2], McGee [32], Schweizer [41], Gupta and Belnap [5, chapter 6].

Some of these papers have unmasked several of the alleged arguments against the predicate view as untenable prejudices. In the first place, everything that can consistently be said in an operator language can be consistently said in the language with a predicate instead. More precisely, sentences of modal operator systems can be translated into sentences of a rich predicate system in a natural way such that provability is preserved. The resulting system with □ as a predicate is consistent with systems that allow for a proof of the Diagonalisation Theorem. Under this translation, operator sentences become sentences where the modal operator is replaced by a corresponding predicate. This argument can be taken as a proof that one does not have to sacrifice anything for the predicate view (see des Rivières and Levesque [38] and Gupta and Belnap [5, p. 240 ff]).

Only if the provability of axiom schemata 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’ sentences, that is, roughly speaking, sentences whose semantical evaluation hinges on nonsemantical facts; more exactly, they are sentences that arise from sentences without □ by finite applications of □. Sentences like the liar sentence that yield the inconsistencies are typical examples of ungrounded sentences; they do not have counterparts in the operator language.

In this paper we investigate the second main argument against the predicate approach which says that possible-worlds semantics is not feasible for predicates. Asher and Kamp [2] and Gupta and Belnap [5, chapter 6] have already refuted this view by providing possible-worlds semantics for modal predicate languages in certain special cases. But although in some cases possible-worlds semantics can be provided, there are also well-known severe restrictions. We want to explore in which cases problems arise.

We shall stick as closely as possible to the common possible-worlds semantics for operators, and we shall not apply tricks to avoid paradoxes. That is, we shall use classical logic throughout, in contrast to other authors who have applied the techniques known from the theory of truth, e.g., partial or many-valued logic, to the theory of necessity and similar concepts.

However, there is one fundamental decision we have to make which is avoided on the operator approach. If necessity, truth, belief and the like are predicates, then they must apply to objects of a certain kind. Propositions, tokens or types of sentences, utterances, mental objects or the like have been used for this purpose. The different choices have been discussed for a long time. Here we are not able to go into this discussion and mention just one aspect.

The problem of the choice between the different categories of objects is connected to a family of arguments that have been employed against necessity, truth and belief as predicates of sentences (e.g., the so-called Church–Langford argument; see [4]). According to these arguments, the meaning of a linguistic expression is always contingent. Thus, for instance, it is never necessary that “All men are men” is necessary, because the expression “All men are men” could have meant something else; it could have meant “It is raining”. Therefore the expression “All men are men” is not necessarily necessary; it is only contingently necessary, namely contingently on the assumption that the string of symbols has its actual meaning. Only the proposition expressed by “All men are men” is necessarily necessary.

Arguments of this kind have lead philosophers to the claim that truth, belief etc. are predicates of propositions (e.g., in the case of Bealer and Pap [36]), while others have claimed that truth is not a predicate at all (e.g., Strawson [44] and Grover, Camp & Belnap [16]). Still others (like Field [13]) maintain that there are ‘deflationist’ uses of the truth predicate to which this kind of reasoning simply does not apply. We do not discuss these arguments here.

It is compatible with our account to conceive □ either as a predicate of sentences or as a predicate of propositions—as long as the latter share the structure of sentences. If we opt for sentences as objects to which necessity, truth etc. is ascribed, then we have to say that we deal with ‘deflationist’ uses of these predicates. At any rate we keep the interpretation of the vocabulary fixed that talks about the objects to which truth, necessity and so on is ascribed. So the argument involving the contingency of meanings is avoided.

In our technical treatment we shall apply the predicate □ to numerical codes of sentences (and we shall even identify expressions with their codes), although we do not think that this is actually the most satisfying approach. It allows us, however, to proceed to our main topic, possibleworlds semantics for predicates, without before developing a theory of propositions or other objects.

Our approach leaves room for several interpretations: the codes could be interpreted as types of sentences or as (language-independent) propositions. We shall discuss these issues in a separate paper and return to our main topic.

The core of possible-worlds semantics is the analysis of necessity (or the notions mentioned above) as truth in all accessible worlds (or situations or the like). That is, sentences □A (on the operator account) or □⌜A⌝ (on the predicate account) are true if and only if A is true in all accessible worlds. Here a fundamental difference shows up between possible-worlds semantics for modal operator and modal predicate languages. In the case of an operator conception, this analysis can be turned into a clause in the definition of validity of modal sentences. If a frame, i.e., a set of worlds with an accessibility relation, is given and a function that assigns a model for the □-free language to any world, then it is easy to define truth at a world for all sentences with □ as an operator. The definition proceeds by recursion on the complexity of the sentence. Thus one can build a model on every given frame.

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. Also there is no way to provide an amended definition of the complexity of a formula that allows for a recursive definition of truth at a world. Problems are posed, in particular, by self-referential sentences like the liar sentence.

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. Montague’s [33] Theorem, for instance, shows that one cannot build possibleworlds models on reflexive frames (see Example 5 below) if necessity is viewed as 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 all accessible worlds (and if some conditions are met which will be explained below). Another example is provided by McGee’s [31] Theorem on ω-inconsistent systems. It is a direct consequence of this theorem that a frame consisting in the natural numbers ordered by the successor relation (so that every world sees exactly one other world) does not support a possible-worlds model.

Although several further such restrictions on frames are known, the general problem has not been tackled so far: which frames support a possible-worlds model, if □ is a predicate?

A satisfying answer to this characterisation problem would exhibit a graph-theoretical description of the frames supporting possible-worlds models. The restriction imposed by theorems like those due to Montague and McGee should drop out as consequences of such a characterisation result.

Our development of possible-worlds semantics for predicates will also yield some further insights. It allows to model certain paradoxes and inconsistency results in a framework where are modalities are treated uniformly. Here we explicitly reckon—like Ockham did—-also truth, being known and other notions among the modalities.

Moreover our approach sheds a new light on hierarchies of metalanguages, and some results of provability logic and modal logic are generalised. Our treatment of transitive converse wellfounded frames can be seen as a variant or generalisation of the revision theory of truth.

Overview of the remaining sections. In section 2 we define the basic notions of possible-worlds semantics such as frames etc. and apply this account to predicates rather than operators of sentences. Some examples of frames that do not support a model are provided in section 3. We tackle the Characterisation Problem for transitive frames in sections 4 and 5, and provide some results on other frames in section 6. In section 7 we show that some frames support more than one model even in the absence of “contingent” vocabulary. We return to a classical topic of operator modal logic in section 8, namely completeness; we shall provide a completeness result by the method of canonical models. Sections 9 and 10 deal with the properties of a fixed point of an operator that arises in the construction of models. All our constructions so far are based on the standard model of arithmetic; we sketch some applications to nonstandard models and other models and languages in sections 11 and 12.

§2. Possible-Worlds Semantics. L_{PA} is the language of arithmetic; L_{□} is L_{PA} augmented by the one-place predicate symbol □. We shall identify L_{PA} with the set of all arithmetical formulae and L_{□} with the set of all formulae that may contain □. We do not distinguish between expressions (like formulae 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. In fact, our account can and should be applied to expansions of L_{PA}. In the main parts of this paper, however, we shall concentrate on the language L_{PA} because additional vocabulary would be idling and obstruct the view for the essentials. We shall discuss expansions of L_{PA} in section 12.

Except for section 11 we shall consider standard models only, i.e., models with the set of natural numbers as the domain and the standard interpretation of the arithmetical vocabulary. Hence models have the form (ℕ, X) where ℕ is the standard model of arithmetic and X ⊆ ω the extension for □. Since models differ only in the extension of □, we may identify 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.

Definition 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. World w sees v if and only if wRv.

Next we define PW-models. They must not be confused with the models of the form (ℕ, X). The latter are models in the usual sense and act, loosely speaking, as worlds in PW-models.

Definition 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. Thus a frame supports a model if and only if it admits a valuation.

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 were to include further ‘contingent’ vocabulary, the valuation V not only would have to interpret □ but also this additional vocabulary. We shall consider this situation in section 12.

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. 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 provide 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 [6]). These systems are closed under necessitation, and the necessity operator □ distributes over material implication. For the predicate account something similar can be shown.

Lemma 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))).

Here \overrightarrow{.} represents the function that yields, when applied to two codes of sentences, the code of their material implication (if no such function symbol is available it is to be expressed by a suitable predicate expression). 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. This does not make a difference because of the use of standard models.

§3. Some Limitative Results. As has been noted in the introduction, several restrictions on the class of frames supporting a PW-model are well known. These restrictions correspond to several inconsistency results. We begin with the most trivial example, namely the liar paradox or Tarski’s Theorem which shows that object- and metalanguage cannot coincide.

[figure: •]

Example 4 (Tarski). The above frame with one world that sees itself does not admit a valuation.

Montague’s Theorem is a generalisation thereof.

Example 5 (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. We present it in detail as an example.

Proof. Assume ⟨W, R, V ⟩ is a PW-model based on ⟨W, R⟩ which is reflexive. The liar sentence is a sentence such that PA ⊢ A ↔ ¬□⌜A⌝; it holds at any world. Pick an arbitrary world w ∈ W.

If V (w) ⊧ ¬A then also V (w) ⊧ □⌜A⌝ and thus by reflexivity V (w) ⊧ A. Therefore V (w) ⊧ A must hold and consequently there is a world u such that wRu and V (u) ⊧ ¬A and again V (u) ⊧ A. ⊣

The arguments showing that a frame does not admit a valuation proceed by diagonal arguments. In the above examples we employed the liar sentence. The next two examples require slightly more complex diagonal sentences.

\xymatrix{• \ar[r] & • \ar[l]}

Example 6. The frame ‘two worlds see each other’ displayed above does not admit a valuation.

The existence of a suitable valuation is refuted by the fixed point A ↔ ¬□⌜□⌜A⌝⌝.

This example can be generalised in the obvious way in order to refute the existence of valuations for loops of arbitrary finite length.

Now we turn to a frame with a dead end, i.e., a world which does not see any other world.

[figure: •; •]

Example 7. The frame ‘one world sees itself and one other world’ does not admit a valuation.

For the proof the fixed point A ↔ (□⌜A⌝ → □⌜¬A⌝) can be employed.

\xymatrix{• \ar[rr] &  & • \ar[ll] \\  & • \ar[ur] \ar[ul]}

Example 8. The above frame ‘one world sees two worlds that see each other’ does not admit a valuation.

One can show this by using the fixed point A ↔ ¬□⌜□⌜A⌝⌝ ∧ ¬□⌜A⌝. So far we have been dealing with transitive frames only. McGee’s main

theorem in [31] on the ω-inconsistency of a certain theory of truth imposes a restriction on the existence of PW-models based on a nontransitive frame. Pre is the predecessor relation: k Pre n if and only if n = k + 1.

\xymatrix{⋮ \\ 2 \ar[u] \\ 1 \ar[u] \\ 0 \ar[u]}

Example 9 (McGee, Visser). ⟨ω, Pre⟩ does not support a PW-model.

The proof relies on the following diagonal sentence involving a quantifier (see McGee [31]):

A ↔ ¬∀x □\begin{matrix}h \\ . \end{matrix}(x, ⌜A⌝).

Here \begin{matrix}h \\ . \end{matrix} represents a function satisfying the following equation:

h(n, ⌜B⌝) = ⌜\underbrace{□⌜□⌜…}_{n} ⌜B⌝ \underbrace{⌝ …⌝}_{n}⌝.

(See also Halbach [18, Lemma 4.1(iv)] for a proof of the example.) By a similar argument one can show that there is no PW-model based on ⟨ω, <⟩.

Instead of McGee’s theorem Visser’s theorem [45] on illfounded hierarchies of languages can be used for deriving the above result. The relations between the different ω-inconsistency results and their implications are studied by Leitgeb [29].

Also Gödel’s Second Incompleteness Theorem can be rephrased in terms of possible-worlds semantics. First we prove Löb’s Theorem, which will be very useful in later sections.

Transitivity yields the predicate analogue of the K4 axiom:

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

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

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

Lemma 11 (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⌝.

Proof. The proof is the usual proof of Löb’s Theorem with the provability predicate replaced by the primitive symbol □. The diagonalisation lemma yields a sentence K:

V (w) ⊧ K ↔ (□⌜K⌝ → A). (1)

Since this holds in any world, we may necessitate the sentence according to Lemma 3:

V (w) ⊧ □⌜K⌝ → (□⌜□⌜K⌝⌝ → □⌜A⌝)
V (w) ⊧ □⌜K⌝ → □⌜A⌝  Lemma 10
V (w) ⊧ (□⌜A⌝ → A) → (□⌜K⌝ → A)
V (w) ⊧ (□⌜A⌝ → A) → K  by (1)

Since this holds at all worlds w, we may necessitate the last sentence and obtain Löb’s Theorem by applying V (w) ⊧ □⌜K⌝ → □⌜A⌝. ⊣ Obviously Löb’s Theorem is a kind of an induction principle (see Boolos [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 the theorem:

Corollary 12. 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 11 (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. Obviously V (w) ⊧ □⌜⊥⌝ holds if and only if w is a dead end.

Example 13. 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 K4 axiom scheme holds. This suffices for a proof of the formalised Incompleteness Theorem and we obtain V (w) ⊧ □⌜⊥⌝ ∨ ◇⌜□⌜⊥⌝⌝. ⊣

In the sequel we shall provide a theorem (Theorem 32) that implies all the above results and does away with the need for all the different diagonal sentences, which have to be found for every frame separately. In the end all limitative results can be derived from Löb’s Theorem.

§4. The Characterisation Problem for Transitive Frames I. In the preceding section we have presented some examples of limitations on the existence of valuations. All frames discussed in the preceding section have infinite R-chains w_{1}Rw_{2}Rw_{3}R …, that is, they are not converse wellfounded. It is not hard to show that all converse wellfounded frames support a PW-model (see Theorem 31 below). However, also some converse illfounded frames admit valuations. Because of these frames the Characterisation Problem is nontrivial.

The following two sections are devoted to a special case of the Characterisation Problem, namely to the following question: Which transitive frames admit valuations? In the present section we provide sufficient conditions for the existence of a valuation; some (unfortunately inequivalent) necessary conditions are then given in the next section. Throughout both sections we assume that R is transitive. We give here a brief outline of the results of these two sections and (some) of Section 6.

It is natural to look first at frames with an accessibility relation that is a converse wellfounded ordering, indeed a converse wellorder. For these it is unproblematic to assign valuations (see Theorem 31). From these one considers orderings that have some co-initial wellfounded part (Definition 14), and we seek to characterise (first) those linear orderings that have some converse wellordered part, with a possibly illfounded initial part. We first analyse however how valuations are built up along converse wellorderings. It turns out that there is a natural operator, Φ, associated to the transition of the extension of the □ symbol from one world to its immediate predessor. This operator is decreasing, and hence, if the converse wellordering is sufficiently long, results in a fixed point after some least ordinal number κ, of stages of application. The main theorem of the section (Theorem 23) is a calculation of κ. It is not hard to imagine, for the first stages at least, that the extension of □ along the co-initial segment of an accessibility relation, being a predicate referring to truths at previous worlds, in fact contains sufficient information to amount to an iteration of a truth predicate. Indeed this is precisely what happens; and once into the transfinite the idea is that the extensions of □ (called X_{α+1} at the “α + 1’st world”) in fact code truth sets for the α’th level of the Gödel constructible hierarchy L_{α}. At a certain level of this hierarchy, γ, the structure ⟨L_{γ}, ∈⟩ is sufficiently closed that it becomes first-order reflecting (see the discussion before Theorem 23). It is precisely at this stage that we have our fixed point. The structure ⟨L_{γ}, ∈⟩ is a model of Kripke-Platek set theory, KP. Such a theory is important for us since our (simplest to state) sufficient condition on those linear orders that carry valuations, are as those that are isomorphic to (initial segments of) the ordinals of models of KP. Such models need not be wellfounded. This is done at Theorem 27. A more technical sufficient condition is that of Theorem 25; a more quotable version is the Corollary 26: essentially if a KP model A contains a linear frame ⟨W, R⟩ as an element of the model, then that frame supports a valuation if A is a model of the statement that “R is converse wellfounded” (irrespective of the truth of that statement in the real word – as A may itself be illfounded, and hence assess the truth value of this assertion incorrectly).

We are unable to give an exact characterisation of all linearly ordered frames that admit valuations, however the main result of section 5 gives a necessary condition on what those linear orders must look like: if they are converse illfounded, then the converse wellfounded part must have order type greater than κ or be an admissible ordinal ω < α ≤ κ (Lemma 30). (That there are such frames is a standard fact and an application of the Barwise Compactness theorem - cf Lemma 35 and the related Proposition 37 of section 7 where it is shown that there are frames with converse wellfounded part any countable admissible ordinal > ω, which admit a valuation containing a Φ-fixed point (necessarily by the above in the converse-illfounded part of the frame).)

It seems to us that the problem of finding which linear orders admit frames is a particular case of the problem “Along which linear orderings can one build L-hierarchies?”, or equally, hierarchies of ramified analysis. We make one simple conjecture here concerning just recursive linear orderings (at the end of section 4). This amounts to the claim that the sufficient condition of Theorem 27 is also necessary; but more generally it seemed to us at one point reasonable as a conjecture that one could build such a frame ⟨W, R⟩ with an associated valuation by piecing together pseudowellorders, whose converse wellfounded parts were of increasing admissible order type, as one descended through R.

We now proceed to the formal definitions. As above, a world w is converse wellfounded in a frame ⟨W, R⟩ if and only if every subset of w ↑ =_{df} { u ∈ W | wRu } has an R-maximal element. A set of worlds is converse wellfounded if and only if all its elements are converse wellfounded; thus a set S of worlds is converse wellfounded if and only if ⋃_{w∈S} w ↑ is wellfounded with respect to R^{−1}.

Definition 14. For any partial order ⟨X, T ⟩ we define the wellfounded part as WFP(X) = WFP(⟨X, T ⟩) =_{df} ⟨X′, T ↾X′×X′⟩ where X′ is the maximal set X′ ⊆ X, downwards closed under T, on which T is wellfounded.

Associated with any wellorder is the natural rank function defined by transfinite recursion. We define the rank of the wellfounded part of any partial order to be the supremum of the ordinal ranks of its elements.

Concerning our frames, the converse wellfounded part of a set of the form { v | wRv } is then 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 defined to be the rank of R^{−1} restricted to the converse wellfounded part of { v | wRv }. Thus a world does not have to be converse wellfounded to have a depth. (Later we shall need to apply this definition also to frames that are not transitive. If R is not transitive, we set the depth of w in ⟨W, R⟩ as the depth of w in ⟨W, R^{∗}⟩, where R^{∗} is the transitive closure of R.) If R is transitive and converse wellfounded, then V (w) is determined by the depth of w. Thus V may be defined inductively by an operator Φ, which we shall study now.

Φ will generate suitable extensions of □. Thus we start with the set L_{□} of all sentences (which, perforce, are all in the extension of □ at any dead end) and Φ will progressively remove sentences of L_{□} in order to define the extension of □ at worlds of larger depth. Thus the operator does not build up larger and larger sets from the empty set; it rather reduces L_{□}. We could work instead with an operator generating suitable extensions for ◇ from the empty set, which we did in [19], but this makes the notation awkward.

Definition 15. We set for any set X of natural numbers:

Φ(X) =_{df} X ∩ { A ∈ L_{□} | (ℕ, X) ⊧ A }.

In the following, Φ^{α}(X) designates the α-fold application of Φ to X; at limit ordinals λ, Φ^{λ}(X) is defined as the intersection ⋂_{α<λ} Φ^{α}(X) of all previous stages.

The following lemma is established by induction on the depth α of w (and is a special case of 31).

Lemma 16. Assume ⟨W, R, V ⟩ is a PW-model based on a transitive converse wellfounded frame. If w has depth α, then V (w) = Φ^{α}(L_{□}) holds for all ordinals α.

A set X ⊆ L_{□} is a fixed point (of Φ) if and only if Φ(X) = X. For any set Φ(X) ⊆ X holds and, consequently, Φ^{α}(L_{□}) ⊇ Φ^{β}(L_{□}) if α ≤ β. Thus by iterated applications of Φ to L_{□} we arrive at a fixed point:

Lemma 17. There is an ordinal κ such that Φ^{κ}(L_{□}) = Φ^{α}(L_{□}) for all α ≥ κ.

The operator Φ (as well as the corresponding operator for ◇) is not monotone, that is, X ⊆ Y does not generally imply Φ(X) ⊆ Φ(Y). Therefore the fixed point Φ^{κ}(L_{□}) need not be maximal (and the fixed point generated by the corresponding operator for ◇ need not be minimal).

The operator Φ compares with the revision operator Ψ of revision semantics as introduced by Gupta [17] and Herzberger [21] (see Gupta and Belnap [5]). The revision operator Ψ takes a set X to the new extension { A ∈ L_{□} | (ℕ, X) ⊧ A }. Since X ⊆ Ψ(X) does not obtain, at a limit level one cannot simply take the intersection of all levels up to the limit level. Several alternative treatments of limit stages have been proposed.

If we start with the set L_{□} of all sentences, apply Φ repeatedly to it and take intersections at limit stages, then the liar sentence L with L ↔ ¬□⌜L⌝ is in L_{□} but not in any Φ^{α}(L_{□}) for α ≥ 0. In revision semantics, in contrast, the liar sentence will always flip in and out of the extension of the truth predicate, thereby causing trouble with the definition of the extension at limit stages; in particular, as already noted, the revision process will never converge.

Fixed points of Φ can be characterised in the following way.

Lemma 18. X ⊆ L_{□} is a fixed point if and only if X ⊧ □⌜A⌝ → A for all A ∈ L_{□}.

The existence of fixed points implies that there are frames that are not converse wellfounded but which admit a valuation nevertheless.

Theorem 19. 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 16. If w ∈ W has depth at least κ we put V (w) = Φ^{κ}(L_{□}). This holds in particular for all converse illfounded worlds.

By Lemma 17 the condition

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

is satisfied by all worlds w ∈ W. ⊣

In the following, ω_{1} will always denote the first nonrecursive ordinal (see Rogers [39]). Using an ordinal notation system for the ordinals below ω_{1} it is possible to construct sentences that hold at a world w of a transitive frame if and only if w is converse wellfounded and has depth α < ω_{1}. However, in general one cannot express converse wellfoundedness in L_{□}.

Corollary 20. 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⟩.

Proof. According to Theorem 19 there are frames ⟨W, R⟩ with not converse wellfounded worlds that support a PW-model. If there were such a formula A,

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

would hold in every world w ∈ W. By Lemma 11 (Löb’s Theorem) □⌜A⌝ would hold in every world of W. But by assumption A does not hold in these converse illfounded worlds. Contradiction! ⊣

We determine the exact size of the closure ordinal κ of Φ and thereby show that there is a gap between ω_{1} and κ.

We abbreviate by setting X_{α} = Φ^{α}(L_{□}). The function δ ↦ X_{δ} can be defined by a Σ_{1}-recursion over the ordinals of M where the latter is any sufficiently closed model ⟨M, E⟩ 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. For background on the theory KP and on admissible sets, see Barwise [3]. We review some of this theory and these notions here. We shall assume the reader is familiar with Gödel’s constructible hierarchy, which can also be found in [3]. The theory of KP is expressed in the language of set theory, that is, with equality, and the single nonlogical symbol ˙∈.

Transitive models M = ⟨M, ∈⟩ of KP, with the symbol ˙∈ getting its standard interpretation, are called admissible sets. We shall have occasion to consider in the sequel nonwellfounded models of KP: that is, models of the form ⟨A, E⟩ where the epsilon relation E of A is not wellfounded. The wellfounded part of such a model WFP(A) =_{df} WFP(A, E) is defined in accordance with Definition 14, by considering E as a partial ordering on the domain of A.

If α is the ordinal rank of the wellfounded part WFP(A) (we shall write α = ρ(WFP(A))), then it is known that WFP(A) is a model of KP (the so-called “Truncation Lemma”, see [3, II 8.4]). In particular this lemma implies that the constructible part of WFP(A), which is isomorphic to ⟨L_{α}, ∈⟩, also is a model of KP. If A is a model of KP, On(A) denotes the class of ordinals in the sense of A. We adopt the convention that we identify the wellfounded part of On(A) with the standard ordinals to which they are order-isomorphic (and similarly we identify the E-relation restricted to the wellfounded part as the actual ∈-relation). Hence On(WFP(A)) ⊇ ω +1 holds if and only if the integers of A are standard. We shall only consider in what follows models of KP in which the integers are standard and moreover form a set.

The feature, and strength, of KP which we shall be exploiting is its ability to define functions by transfinite recursion along relations (usually the ordinals of the model, or its E-relation), if the defining clauses of the recursion are sufficiently simple: that is, have a form which is—provably in KP—equivalent to a Σ_{1}-form. Thus ordinal arithmetic, and in particular the Gödel L-hierarchy, can be defined by suitable Σ_{1}-recursions over any model A of KP. Hence such models A have versions of the L-hierarchy contained inside them as “inner models” of KP. Thus if the model A is illfounded, the L-hierarchy of A coincides with L_{α} on the wellfounded part of A (by our convention) but there will also be sets Z ∈ A that are the levels L_{a} of the constructible hierarchy of A where a is a nonstandard ordinal in the illfounded part of A. Another example is the operation of Φ: this can be defined by a Σ_{1}-recursion inside any KP-model A using as frame the converse of the A-ordinals, ⟨On(A), E^{−1}↾On(A)^{2}⟩. The latter may be illfounded, and if so, the result will be an illfounded frame with a valuation defined in A. (It is to be emphasised that A of course thinks its ordinals are wellfounded: only in the “real world” of all sets do we see that there is a counterexample to wellfoundedness: that is, a nonempty set X ⊆ On(A) which has no E-minimal element. It is a consequence of KP that there is no such X ∈ A.)

We shall always assume that the Axiom of Infinity is part of KP. An ordinal is admissible if ⟨L_{α}, ∈⟩ is a model of KP. For R ∈ 2^{ω} (or equivalently R ⊆ ω) we let ω_{1}^{R} denote the supremum of the ranks of all wellorderings of ω that are recursive in R. ADM is the class of all admissible ordinals, which by this assumption are all greater than ω. ADM is not a closed class; we thus define ADM^{∗} as ADM together with all of its limit points.

The idea of the proof of the following theorem is that below the closure ordinal κ of the operation Φ, the sets X_{δ+1} (for δ ≥ ω) 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, ∈⟩). This ordinal is in some senses a large one: it is recursively Mahlo (indeed a fixed point in a recursively “hypermahlo” hierarchy). It is easy to see that L_{γ} ⊧ ∀x(|x| = ω). Further one may show the following:

Proposition 21. γ is the least ordinal for which ⟨L_{γ}, ∈⟩ ≺_{Σ_{1}} ⟨L_{γ+1}, ∈⟩ holds.

Actually we could have used this as our definition of γ in the sequel. From this it follows that γ is less than the least ordinal ν so that L_{ν} ⊧ KP + Σ_{1}-separation.

Lemma 22. 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 latter property fails first at L_{γ+1}. We sketch a proof of the lemma.

Proof. That L_{γ} ⊧ KP is fairly immediate. (If, for example, some instance of Δ_{0}-comprehension failed, one obtains a function g: x → On, for some x ∈ L_{γ}, with g Σ_{1}-definable over L_{γ}, that is, unbounded in γ. However L_{γ+1} believes ran(g)is bounded, and this Σ_{1}-statement transfers down to L_{γ}—a contradiction.) If the Skolem Hull property failed for some set x ∈ L_{γ} we may use a function F that is Δ_{1}^{L_{γ}}-definable and is a bijection between γ and L_{γ}, to assume, without loss of generality, that some least ordinal δ < γ fails to be Σ_{1}-definable. But then no ordinal η with δ < η < γ can be Σ_{1}-definable over L_{γ} without parameters. If η were a counterexample, then we use the fact that in L_{η+1} there is a least (in the canonical wellorder of L_{η+1}) wellorder of ω, S say, in order type η. There must be such a wellorder: otherwise η is a cardinal inside L_{η+1} and then it can be shown there are chains of fully elementary chains of models of ZF^{−}-models of the form L_{γ_{n}}≺ L_{γ_{n+1}} with all γ_{n} < η < γ. Thus δ would be Σ_{1}-definable from this wellordering S (as being isomorphic to the “rank of k in S” for some k ∈ ω) in L_{γ}. Putting this together with the Σ_{1}-definition of η, and the further Σ_{1}-definition of L_{η+1} from η, would constitute a parameter-free Σ_{1}-definition of δ—a contradiction.

Now it can easily be shown that L_{δ} ≺_{Σ_{1}} L_{γ}. If this failed, then for some Σ_{0}-formula ψ(v_{0}, v_{1}) we should have L_{γ} ⊧ ∃x ψ[x, y] but L_{δ} ⊧ ∃x ψ[x, y] fails for some set y ∈ L_{δ}. But y has a Σ_{1}-parameter-free definition in L_{γ}, so in effect we can drop y by rewriting the definition ∃v_{0} ψ(v_{0}, v_{1}) as ∃v_{0} ψ′(v_{0}). Now γ is a limit ordinal, hence the “least ordinal η so that L_{η} ⊧ ∃x ψ′[x]” is a Σ_{1}-definition of an ordinal greater than δ. Contradiction!

But γ was least so that L_{γ} had a Σ_{1}-end extension! Hence there is no such δ. ⊣

The two facts from Proposition 21 and Lemma 22 above from the folklore are used in the proof of Theorem 23 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 [1]):

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

(As indicated above, L_{γ} is a model of a strong extension of KP—stronger than the theory KPi which is proof-theoretically equivalent to ACA + Bar Induction + Δ_{2}^{1}-Comprehension Scheme; however, it is known, by consideration of (i) above, that it is weaker than the latter strengthened with the Π_{2}^{1}-Comprehension Scheme—see Rathjen [37].)

Theorem 23. γ = κ.^{1}

In particular, this shows that κ > ω_{1} (like any admissible ordinal, ω_{1} is Π_{2}-reflecting but it is not Π_{3}-reflecting). We shall prove this theorem after a preliminary lemma.

We shall let Σ_{n}-Th(L_{β}) denote the set of Σ_{n}-sentences true in ⟨L_{β}, ∈⟩. We use lower-case Greek letters φ, ψ etc. for formulae in the set-theoretic language possibly expanded by additional parameters. Note if Σ_{1}-Th(L_{δ}) is Σ_{k}-definable over (ℕ, X_{δ}), say,

φ ∈ Σ_{1}-Th(L_{δ}) ⟺ (ℕ, X_{δ}) ⊧ C_{1}(⌜φ⌝), (2)

then it is well known that Σ_{n}-Th(L_{δ}) is Σ_{k+n}-definable over (ℕ, X_{δ}) in a definition effectively obtainable from that of C_{1}. We shall see by the following Lemma that we may take here k = 1 and thus we shall have for a suitable formula C_{n}(x):

φ ∈ Σ_{n}-Th(L_{δ}) ⟺ (ℕ, X_{δ}) ⊧ C_{n}(⌜φ⌝). (3)

Lemma 24. Σ_{1}-Th(L_{δ}) is Σ_{1}-definable over ⟨ℕ, X_{δ}⟩ (and thus is recursively enumerable in X_{δ}). The definition is uniform for all δ + 1, that is, it is independent of δ. It is similarly uniform for all limits δ.

Proof. We prove the lemma by induction on δ.

If δ is a limit ordinal, we have the following by the upwards persistence of Σ_{1}-sentences:

Σ_{1}-Th(L_{δ}) = ⋃_{α<δ} Σ_{1}-Th(L_{α}).

Thus we arrive at the following:

φ ∈ Σ_{1}-Th(L_{δ}) ⟺ ∃α < δ φ ∈ Σ_{1}-Th(L_{α})
⟺ ∃α < δ (ℕ, X_{α}) ⊧ C_{1}(⌜φ⌝)  by (2)
⟺ ∃α < δ (C_{1}(⌜φ⌝)) ∈ X_{α+1}
⟺ (C_{1}(⌜φ⌝)) ∈ X_{δ}.

Therefore Σ_{1}-Th(L_{δ}) is Σ_{1} over (ℕ, X_{δ}).

We turn to the successor case. Assume φ is Σ_{1} and L_{δ+1} ⊧ φ. Suppose φ ≡ ∃y ψ(y) where ψ(v_{0}) is Σ_{0} with just v_{0} free. Let y ∈ L_{δ+1} be a witness to this. Hence L_{δ+1} ⊧ ψ(\overline{y}). By construction y ∈ Def(⟨L_{δ}, ∈⟩) and has therefore a first-order definition:

y = \{ z ∈ L_{δ} | L_{δ} ⊧ χ(\overline{z}) \}.

By our assumption on γ (Fact (ii) above), we can assume all parameters that would normally be required in such a defining formula χ(v) have in fact been replaced by Σ_{1}-defining terms. We may thus assume χ(v) has just the one free variable shown, and no other parameters from L_{δ}. Let ψ(χ) be the Σ_{m}-formula (for some m) obtained by replacing each mention of v in ψ(v) by { u | χ(u) }. For any formula ζ of set theory set lh(ζ) to be the smallest n such that ζ is in Σ_{n}. We thus have

1The closure ordinal γ for the operator Φ was independently suggested to Volker Halbach by Peter Aczel, and by Philip Welch. [V.H.]

φ ∈ Σ_{1}-Th(L_{δ+1}) ⟺ L_{δ+1} ⊧ ∃y ψ
⟺ ∃χ (ψ(χ) ∈ Σ_{lh(ψ(χ))}-Th(L_{δ}))
⟺ ∃χ (C_{lh(ψ(χ))}(⌜ψ(χ)⌝) ∈ X_{δ+1}).

The last line follows from (3) and our inductive hypothesis. ⊣

Proof of Theorem 23. We prove κ ≤ γ first. Suppose γ < κ for a contradiction. Then X_{γ} ≠ X_{γ+1}. Let A ∈ X_{γ+1} \ X_{γ}. Suppose that A ∈ Σ_{k}. Then recall that

{ A | A ∈ Σ_{k} ∧ (ℕ, X_{γ}) ⊧ A }

is recursive in X′_{γ}^{(k)} (the k’th Turing jump of X_{γ}). By the preliminary remarks above, as L_{γ} is a KP-model, X_{γ} = ⋃_{α<γ} X_{α} is Σ_{1}^{L_{γ}}-definable.

Then X′_{γ}^{(k)} is Σ_{k+1}^{L_{γ}}-definable, and is in L_{γ+1}. Thus γ is Σ_{1}-definable in L_{γ+1} as “the least γ̄ so that n ∈ X′ ; γ̄^{(k)} ”. But then L_{γ} cannot be a Σ_{1}-substructure of L_{γ+1}. Thus we have κ ≤ γ.

It remains to show κ ≥ γ. We derive a contradiction from κ < γ by assuming the following:

φ ∈ Σ_{1}-Th(L_{κ+1}) \ Σ_{1}-Th(L_{κ}).

Such a φ exists, since otherwise L_{κ} ≺_{Σ_{1}} L_{κ+1}, whereas γ is the least ordinal with this property. Thus by Lemma 24 we arrive at the following:

∃χ (C_{lh(ψ(χ))}(⌜ψ(χ)⌝) ∈ X_{κ+1} \ X_{κ}),

whereas κ is the closure ordinal for this operation and X_{κ} is a fixed point. Contradiction! ⊣ Thus the characterisation of the class of transitive frames admitting valuations yielded by Lemma 32 and Theorem 19 is incomplete because it does not say whether worlds of depth α with ω_{1} ≤ α ≤ κ have to be converse wellfounded. We shall now show that these worlds may be illfounded, too.

We note that if we concentrate on countable frames ⟨W, R⟩, then we may without loss of generality assume that R is a binary relation on W = ω. If R is such a binary relation, its characteristic function r ∈ 2^{ω} is defined as follows:

for all n, m: r(⟨n, m⟩) = 1 ↔ nRm.

We add a symbol \overline{r} to the language of KP and numerals \overline{n} for all natural numbers. Diag(R) contains the sentence \overline{r} ∈ 2^{ω} as well as all sentences \overline{r}(⟨\overline{n}, \overline{m}⟩) = \overline{k} such that r(⟨n, m⟩) = k. For A a KP-model we let κ_{A} ≃ the closure ordinal of the operation Φ—as defined inside A—if it exists; otherwise it is undefined.

Theorem 25. Assume ⟨ω, R⟩ is transitive and the theory KP+Diag(R) does not prove in ω-logic the following conjunction:

(i)“\overline{r} codes a converse illfounded relation R̄ on ω,” and:

(ii) “if κ̄, the closure ordinal of Φ, exists, then there exists a converse illfounded world w with depth(w) < κ̄.”

Then ⟨ω, R⟩ admits a valuation V and thus is a frame with a PW-model.

Proof. As the quoted assertion is not provable, let A be a KP-model containing r, in which the integers are standard, and in which the quoted assertion is false. Note that κ̄_{A}, if it exists, could be a nonstandard ordinal of A.

It suffices to note that A ⊧ “Z =Φ(X)” if and only if Z = Φ(X). Thus in A the Σ_{1}-function F (w) = X_{w} is defined along the part of the relation R̄^{−1} that A believes to be wellfounded. The function so defined in A satisfies these defining clauses for w ↦ V (w) in the real world. If κ_{A} = κ̄ exists, as long as A believes the converse wellfounded part has length κ̄, one may assign V (w) = Φκ̄(L_{□}) for those w in R^{−1} of depth ≥ κ̄. ⊣

We obtain the following corollary from the proof of the last theorem. (Compare this with Theorem 19):

Corollary 26. Let ⟨W, R⟩ be transitive, A be a model of KP, R ∈ A and suppose if A ⊧ “⟨W, R⟩ has a converse illfounded world w”, then A ⊧ “κ_{A} exists, and depth(w) ≥ κ_{A}”. Then ⟨W, R⟩ admits a valuation.

We can add a somewhat more perspicuous example in the case of linear orderings.

Theorem 27. Let R be a linear ordering of ω. Let ⟨W, R⟩ be the frame with W = ω. Then

⟨W, R⟩ admits a valuation if ⟨W, R^{−1}⟩ is a pseudo-wellordering.

We make some remarks on the notions involved. ⟨ω, S⟩ is a pseudowellorder if (a) it is a linear ordering and (b) if X ⊆ ω is an S-descending chain, then X is not hyperarithmetic in S. Thus, in particular, a recursive pseudo-wellorder can have no hyperarithmetic descending chains; pseudowellorders for recursive S were introduced by Spector and Feferman [12] and studied by J. Harrison who showed in [20] the following:

Theorem 28 (Harrison). Let η be the order type of the rationals. Let ⟨ω, S⟩ be a linear ordering. This ordering is a pseudo-wellordering if and only if it has order type ω_{1}^{S}(1+η) + α where α ≤ ω_{1}^{S}.

(In [20] again, only the special case of S a recursive linear ordering is studied, but the argument straightforwardly relativises.) Pseudowellorders characterise the order types of countable models of KP. One may show the following fact: ⟨ω, S⟩ is a pseudo-wellorder if and only if there is a countable model A of KP with ⟨ω, S⟩ order-isomorphic to an initial segment of On(A). The character of a pseudo-wellorder is essentially the admissible ordinal ω_{1}^{S}.

Proof of Theorem 27. Let ⟨ω, R⟩ be a frame with R^{−1} a pseudowellordering. Let B be a KP-model with ⟨ω, R^{−1}⟩ isomorphic to an initial segment of On(B). (If R^{−1} is not a wellorder, we construct such a B below at Proposition 37 with WFP(On(B)) isomorphic to ω_{1}^{R}.) But now arguing as in Theorem 25 we can establish a valuation function F (w) = X_{w} on this initial segment. This suffices. ⊣

Conjecture. Let R be a recursive linear ordering of ω. Then ⟨ω, R⟩ is a frame admitting a valuation if and only if R^{−1} is a pseudo-wellorder.

Note that in this case, as R is recursive, ω_{1}^{R} = ω_{1}. We could have made a more general conjecture about the totality of countable pseudowellorders: it seems to us that, ignoring the final short ordinal part of a pseudo-wellordering, it should be possible to assemble a converse linear ordering admitting a valuation that is built from pseudo-wellorders of increasing character. However we rest content with the above conjecture.

§5. The Characterisation Problem for Transitive Frames II. We now turn to necessary conditions for the existence of a valuation.

As above, ADM^{∗} is the class ADM of all admissible ordinals (without ω) together with its limit points.

Theorem 29. 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 α ≥ κ.

This follows by general considerations, and a similar argument leads to the following lemma, that proves essentially this result restricted to linear orders.

Lemma 30. Suppose ⟨W, R⟩ is a frame with R^{−1} an illfounded linear ordering which admits a valuation V. Then R^{−1} has an initial wellordered segment of order type α ∈ ADM or α ≥ κ.

Proof. By Example 13, R^{−1} has a nonempty wellordered initial segment. The maximal wellordered initial segment of R^{−1} is isomorphic to an ordinal ⟨α, <⟩. We identify this initial wellordered part with α itself. We suppose from now on that R^{−1} has an illfounded part beyond this segment and that α < κ. Thus we need to prove α ∈ ADM.

First we show that α cannot be a successor ordinal β + 1. In order to arrive at a contradiction, assume that β is the maximal element of the wellordered initial segment. Since α < κ, there is a sentence B ∈ L_{□} satisfying the following condition:

V (β) ⊧ □⌜B⌝ ∧ ¬B. (4)

For δ ≤ β we have:

V (δ) ⊧ □⌜B⌝. (5)

Assume w ∈ W is converse illfounded. Since there are infinitely many worlds between w and the wellordered initial segment, we conclude from (4) the following:

V (w) ⊧ ¬□⌜□⌜B⌝⌝. (6)

Together, (5) and (6) yield the following for every world w ∈ W:

V (w) ⊧ □⌜□⌜B⌝⌝ → □⌜B⌝.

Löb’s Theorem (Corollary 12) yields V (w) ⊧ □⌜B⌝. But this is a contradiction because □⌜B⌝ fails at all converse illfounded worlds.

Therefore α has to be a limit number and, by assumption, α is inadmissible over ⟨L_{α}, ∈⟩. Hence by Theorem 23 for the closure ordinal κ there is a function that has domain ω, is cofinal in the ordinal α, and is Σ_{1}- definable over L_{α}. Let us suppose it is defined by the formula ψ(n, γ). As α < κ we need no parameters in this definition. We employ the formula C_{1}(x) used in the proof of Lemma 24 and define the sentence D as

∃n ¬C_{1}(⌜∃y ψ(ṅ, y)⌝).

As in the successor case, we shall show for the sentence D defined in this way that the following holds at all worlds w ∈ W:

V (w) ⊧ □⌜□⌜D⌝⌝ → □⌜D⌝. (7)

In order to show

∀β < α V (β) ⊧ □⌜D⌝, (8)

consider any β < α; as ψ does not define a total function over L_{β}, we have

∃n (∃y ψ(\overline{n}, y)) ∉ Σ_{1}-Th(L_{β}).

But, using (2) in the proof of Theorem 23, this is equivalent to

(ℕ, X_{β}) |̸= ∀n C_{1}(⌜∃y ψ(ṅ, y)⌝)

and (8) follows. (7) will be established, if we have shown that for all converse illfounded worlds w ∈ W the following holds:

V (w) ⊧ ¬□⌜□⌜D⌝⌝. (9)

This may be seen as follows:

∀n ∈ ω (∃y ψ(\overline{n}, y)) ∈ Σ_{1}-Th(L_{α})  definition of ψ(n, γ)
∀n ∈ ω (ℕ, X_{α}) ⊧ C_{1}(⌜∃y ψ(\overline{n}, y)⌝)  by (2)
(ℕ, X_{α}) ⊧ ∀n C_{1}(⌜∃y ψ(ṅ, y)⌝)
(ℕ, X_{α}) ⊧ ¬D.

Since w can see all converse wellfounded worlds β < α, we have V (w) ⊆ X_{α} = ⋂_{β<α} X_{β} and also (9) obtains because there are infinitely many (and thus at least two) worlds between w and the wellfounded part of R^{−1}.

⊣

The partial characterisation of the class of transitive frames admitting valuations yielded by Lemma 29 and Theorem 19 is incomplete because it does not say whether worlds of depth α with ω_{1} ≤ α ≤ κ have to be converse wellfounded. Proposition 37 below will show that for any admissible ordinal α > ω, there exist frames with converse illfounded worlds of depth α.

To summarise: For transitive frames ⟨W, R⟩: (i) If every world w ∈ W has a depth α < ω_{1} 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 ≥ κ) then the frame admits a valuation. Thus for frames where all depths are smaller than ω_{1} 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 29. The problem of finding which, say, linearly ordered frames admit models appears to be part of a more general underlying question: which linear orderings support “constructible” hierarchies?

§6. The General Characterisation Problem. We now turn to the general Characterisation Problem, that is, we drop the assumption that the frames are transitive.

If ⟨W, R⟩ is converse wellfounded, then one can easily define a valuation for ⟨W, R⟩ by induction along R in the following way:

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

Obviously there is no choice in the definition of V. This implies the following sufficient condition for the existence of a valuation, which was proved by Gupta and Belnap in [5, Theorem 6E.5] in a slightly different form.

Theorem 31 (Gupta & Belnap). Every converse wellfounded frame admits exactly one valuation.

The necessary condition Theorem 29 for the existence of a valuation can be generalised in the following way:

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

Proof. There exists a two-place recursive function f that yields applied to a number n and a sentence A the sentence A itself preceded by n necessity predicates, i.e.:

f(y, ⌜A⌝) = \underbrace{□⌜□⌜… □}_{y times}⌜A⌝ …⌝.

Instead of □f(y, ⌜A⌝) we write □^{y}⌜A⌝. Thus □^{0}⌜A⌝ is □⌜A⌝.

We define a new modal predicate corresponding to the transitive closure of that accessibility relation:

□^{∗}x :⟺ ∀n □^{n}x. (11)

Clearly, V (w) ⊧ □^{∗}⌜A⌝ holds if and only if V (v) ⊧ A for all v with wR^{∗}v, where R^{∗} is the transitive closure of R.

Applying Theorem 29 to □^{∗} yields the claim. ⊣ Theorem 32 can be used for demonstrating that the frame ⟨ω, Suc⟩

in Example 9 does not admit a valuation. Thus Theorem 32 implies all negative results in section 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 section 8 we shall show how to get from these analogues back to ω-inconsistency results.

By Theorem 19 a transitive frame admits a valuation if every converse illfounded world w ∈ W has at least depth κ. One might hope to generalise Theorem 19 by showing that a frame admits a valuation if all not converse wellfounded 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. This is shown in the next theorem.

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

Proof. We add to the frame (κ + 1, <) a world w that sees only the fixed-point world κ and itself, but not any worlds α < κ. We call this frame ⟨W, R⟩.

The frame is not transitive because w cannot see the worlds seen by κ. By Theorem 19 the transitive closure of the extended frame admits a

valuation because the only converse illfounded world w of ⟨W, R^{∗}⟩ has depth κ + 1.

D is the usual liar sentence with

D ↔ ¬□⌜D⌝.

We shall show that the assumption that this frame admits a valuation leads to a contradiction.

Since κ sees a dead end, D holds at κ:

V (κ) ⊧ D. (12)

We show that both V (w) ⊧ D and V (w) ⊧ ¬D lead to a contradiction.

1. Case: V (w) ⊧ D. Then we have also V (w) ⊧ ¬□⌜D⌝ and ¬D must hold either at κ or at w, because w does not see any further world. From (12) we conclude V (w) ⊧ ¬D, which contradicts the assumption.

2. Case: V (w) ⊧ ¬D. From V (w) ⊧ □⌜D⌝ and the supposition that wRw we derive a contradiction again. ⊣ 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 Φ^{κ}(L_{□}). However, other fixed points of Φ are required for valuations of certain frames that are not transitive. We give an example.

Proposition 34. There is a model with two reflexive worlds v and w such that V (v) ≠ V (w).

Proof. The set of worlds is defined as follows:

W = { ⟨α, k⟩ | α ≤ κ and k ∈ {0, 1} }.

A world ⟨α_{1}, k_{1}⟩ can see a world ⟨α_{2}, k_{2}⟩ iff one of the following conditions is satisfied:

(i) k_{1} = k_{2} and α_{2} < α_{1}; (ii) α_{1} = 0, k_{1} = 1, α_{2} = κ and k_{1} = 0; (iii) α_{1} = κ and α_{2} = κ and k_{1} = k_{2}. Both copies ⟨κ, 0⟩ and ⟨κ, 1⟩ of κ can see themselves.

A valuation V is easily construed: it is the same as the valuation for the converse wellfounded frame (where ⟨κ, 0⟩ and ⟨κ, 1⟩ cannot see themselves) that is obtained by dropping clause (iii) above. For the κ of the first copy we have V (⟨κ, 0⟩) ⊧ ◇⌜0 ≠ 0⌝ while for the κ of the second copy we have V (⟨κ, 1⟩) ⊧ ¬◇⌜0 ≠ 0⌝ because ⟨κ, 1⟩ cannot see the world ⟨0, 0⟩, which is a dead end. Clearly both ⟨κ, 0⟩ and ⟨κ, 1⟩ can see themselves and are evaluated differently. ⊣

§7. Uniqueness of Valuations. Are there two distinct PW-models based on the same frame? That is, are there frames that admit distinct valuations? Converse wellfounded frames have exactly one valuation by Theorem 31; thus the valuation is always unique. Therefore two valuations for the same frame can differ only on converse illfounded worlds.

The technique developed in the previous section yields an example of a frame that admits two distinct valuations. In order to construct the two valuations, we need an illfounded model of KP.

Lemma 35. There is a nonwellfounded model of KP with

On(WFP(A)) = κ.

Proof. This is a reasonably standard argument, but we explicitly give it here. For the unexplained notions the reader may consult [3]. By Theorem 23, L_{κ} is a union of KP-models: there are unboundedly many α < κ with L_{α} ⊧ KP (for otherwise if α is the largest such, κ is Σ_{1}- definable in L_{κ+1} using the parameter α as “the least β > α so that L_{β} ⊧ KP”). Now let T be the following theory in the infinitary language L_{κ,ω} with constant symbols x̄ for each x ∈ L_{κ} and a further named constant symbol c̄. The theory T comprises the following sets of sentences:

(1) KP + V =L.

(2) The diagram of L_{κ}: { x̄ = ȳ | x = y ∈ L_{κ} }; { x̄ ∈ ȳ | x ∈ y ∈ L_{κ} }.

(3) For each β < κ the sentence “β̄ ≤ c̄ ∧ c̄ is an ordinal”.

(4) The sentence “∀v_{0} ≤ c̄ v_{0} is not the closure ordinal of Φ”. Then every T_{0} ⊆ T with T_{0} ∈ L_{κ} has a model: just take the least α with L_{α} ⊧ KP and T_{0} ∈ L_{α}, and interpret c̄ as any ordinal < α larger than any ordinal mentioned in T_{0}, and interpret the other constant symbols occurring in T_{0} as the corresponding actual sets. By the Barwise Compactness Theorem [3, Theorem 5.6], T has a model A which properly end extends L_{κ} by (2) and (3) (as c̄_{A} is interpreted as something greater than all α < κ); but κ is not in the wellfounded part of A: otherwise it would be ≤ c̄_{A}, and so there would be a closure point of Φ which is an initial segment of On(A) below c̄_{A}, contradicting (4). ⊣

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

Proof. To see this, let A be an admissible set whose wellfounded part has ordinal rank exactly κ. Such a set exists according to the previous lemma. The frame for which we construct two valuations V and V′ is ⟨On(A), <_{A}⟩ where On(A) is the set of ordinals of A (including the nonstandard ordinals) ordered in the sense of A.

Let R^{−1} be an initial segment of the ordinals of A of length b ∈ Ord_{A} where the latter is in the illfounded part of A and A ⊧ b<κ_{A} (if A thinks the latter exists). Define inside A the valuation V by recursion along <_{A}. As κ ∉ A the latter thinks that the closure ordinal κ_{A} (if it exists) is in the illfounded part of A. Hence between κ and b there is no fixed point of the operator Φ. But now let V′ be the valuation obtained by letting V (w) = V′(w) = X_{α} for w of rank α < κ, and V′(w) = X_{κ} otherwise. V and V′ are both valuations admitted by ⟨On(A), <_{A}⟩ (in the real world), but they are clearly different. ⊣

We conclude this section with a remark that actually belongs in section 5, for it complements Theorem 29. However, because we employ methods similar to those of the proof of Lemma 35, we have placed it here.

Proposition 37. For any countable α ∈ ADM there is a linearly ordered frame ⟨W, R⟩ with R^{−1} nonwellfounded, with WFP(R^{−1}) ≅ α and V (w) is a fixed point for some w ∈ W.

Proof. It clearly suffices to assume that α < κ. Apart from the last requirement of a fixed point, this would follow immediately from the standard construction of a nonwellfounded model A of KP with WFP(A) ≅ α—which can be effected by an omitting-types argument. We give a short proof here using a result of Friedman–Jensen, and of Sacks. This runs as follows:

Theorem 38 (Friedman–Jensen; Sacks [40]). Let α ∈ ADM. Then there is x ⊆ ω so that ω_{1}^{x} = α.

Now let A_{0} = L_{δ}[x] the δ’th level of the constructible hierarchy using x as predicate. Let δ > κ be chosen least so that L_{δ}[x] ⊧ KP. Consider the following theory T in the language L_{α,ω}:

(1) KP + V =L[ẋ] + “ẋ⊆ω”.

(2) The diagram of L_{α}[x]:

{ x̄ = ȳ | x = y ∈ L_{α}[x] } ∪ { x̄ ∈ ȳ | x ∈ y ∈ L_{α}[x] }.

(3) For each β < α the sentence “β̄ ≤ c̄ ∧ c̄ is an ordinal”.

(4) The sentence “∀v_{0} ≤ c̄ ⋁⋁_{ψ∈KP} L_{v_{0}}[x] ⊧ ¬ψ”.

(5) “The closure ordinal of Φ exists.” Then every T_{0} ⊆ T with T_{0} ∈ L_{α}[x] has a model: choose η < α so that any β mentioned in T_{0} from the collection specified at (3) is less than η. Then an interpretation of c̄ is afforded by η, and thus ⟨L_{δ}[x], ∈, x, η⟩ is a model of T_{0}. (4) holds since η is less than the first ordinal that is the height of an admissible set containing x. The theory T is Σ_{1}-definable over L_{α}[x] and so the Barwise Compactness Theorem again applies: so let A be a model of T. Then we claim that WFP(On(A)) = α. By (1) and (2) A ⊇ L_{α}[x]. Hence WFP(On(A)) ≥ α. But (3) ensures α ≤ c̄_{A}, and (4) that α cannot be in the wellfounded part of A. ⊣

In particular, it follows that the minimal depth of an illfounded world in any model is exactly ω_{1}.

§8. Completeness. Theorem 32 imposes very strong limitations on frames that support PW-models. The examples in Section 3 illustrate the restrictions. Does this show that possible-worlds semantics does not reach far, that is, that there are no possible-worlds models where models ought to exist? In this section we show that our semantics is not to be blamed for these limitations because there is a PW-model for any set of sentences consistent in ω-logic.

In operator 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 [6]).

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.

Definition 39. A set Th of sentences of L_{□} is □-closed if and only if it satisfies the following conditions:

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

\frac{A(¯0), A(¯1), …}{∀x A(x)}

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

the formalised ω-rule) are in Th for all formulae A(v) of L_{□}.

Theorem 40 (Completeness). If Th is □-closed and consistent, then there is a PW-model ⟨W, R, V ⟩ such that for all sentences A ∈ L_{□} the following equivalence holds: A ∈ Th iff A holds in ⟨W, R, V ⟩ at any world.

Our completeness proof resembles the usual proofs for operator modal logic (see, e.g., Chagrov and Zakharyaschev [10, chapter 5]) by the method of canonical models. However, since we are dealing with standard models only, we employ ω-logic rather than pure first-order logic.

The worlds of the model constructed in the proof are just the possible extensions of the box. Thus one might think of the worlds as the standard models for Th.

For a set Th of sentences of L_{□} we write (ℕ, S) ⊧ Th if for all sentences A ∈ L_{□}, (ℕ, S) ⊧ A holds.

Proof. Assume that Th is consistent and define W as the following set:

W =_{df} { S ⊆ ω | (ℕ, S) ⊧ Th }.

W is not empty since Th is consistent in ω-logic (see Barwise [3, Corollary 3.6]). Thus every world of W is a possible extension S of □ and we interpret □ at a world by S. We define the valuation V by setting V (w) = w. Therefore (ℕ, V (w)) ⊧ Th holds for all w ∈ W.

The accessibility relation R is defined in the following way:

wRv :⟺ (ℕ, v) ⊧ w.

Here w is conceived as a set of sentences of L_{□}.

It remains to check whether ⟨W, R, V ⟩ is a PW-model, that is, we have to show

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

The left-to-right inclusion follows directly from the definition of R.

In order to prove the other direction, assume ∀u(wRu ⇒ (ℕ, u) ⊧ A). By inserting the definition of R we obtain the following:

∀u((ℕ, u) ⊧ w ⇒ (ℕ, u) ⊧ A). (13)

That is, A holds in all ω-models of w.

Since (ℕ, w) ⊧ Th and Th is □-closed, w contains all logical truths and all true atomic and negated atomic sentences of L_{PA} by (i) above; w is closed under logic and the ω-rule because of (ℕ, w) ⊧ Th and (iii). This allows us to apply the ω-Completeness Theorem in the form of Barwise’s [3, Theorem 3.5] 𝔐-Completeness Theorem to (13), which implies A ∈ w.

⊣

Corollary 41. A □-closed set Th of sentences is consistent iff it is satisfied by the dead end model, in which there is just one world and the accessibility relation is empty.

Proof. From left to right: If Th is consistent, it has a PW-model by the Completeness Theorem 40. But by Theorem 32 every frame supporting a PW-model has dead ends. Thus every dead end satisfies Th. The other direction is obvious. ⊣

From the Completeness Theorem we can also derive several inconsistency results. For instances, we can prove that the theory FS of truth in Halbach [18], which is equivalent to a system introduced by Friedman and Sheard [14], is inconsistent in ω-logic. Here we present 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_{□}. The following example might also the viewed as a variant of McGee’s theorem.

Example 42. D is inconsistent.

Proof. For every tautology ⊤ we can derive ◇⌜⊤⌝ in D. But ◇⌜⊤⌝ is not satisfied in a dead end and thus D is inconsistent by our previous corollary. ⊣

We define the predicate counterparts of the operator modal systems K and K4.

Definition 43. K is the smallest □-closed set. K4 is the smallest □- closed set that contains all instances of □⌜A⌝ → □⌜□⌜A⌝⌝.

By applying the theorem to Th = K and Th = K4 we get the following two corollaries:

Corollary 44. 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 K4:

Corollary 45. 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 transitive PW-models ⟨W, R, V ⟩ and w ∈ W.

(ii) A is in K4.

Not all completeness theorems known from operator modal logic carry over to their predicate counterparts. For instance, the logic G obtained from K4 by adding the operator version □(□p → p) → □p is complete with respect to the class of all transitive converse wellfounded frames. The predicate system K4 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 in the next section.

In possible-worlds semantics for operators of sentences one can build PW-models on all frames. We have proved that there are very strong limitations on possible-worlds semantics for predicates (Theorem 32). In particular, the frames of the modal systems T, S5 and D do not feature dead ends and therefore they do not admit valuations. Thus the predicate approach seems to rule out the most important kinds of modality.

Does this not show that the operator approach is superior? We do not think so. It is not our possible-worlds semantics that is to be blamed. Obviously, the predicate analogues of T and S5 are inconsistent, and the analogue of D becomes inconsistent if some natural closure conditions are added (Example 42). Thus the fact that there are no predicate PWmodels based on T, S5 and D mirrors only these inconsistency results. In general, the Completeness Theorem shows that there is a PW-model in our sense for any set of sentences that is consistent in the logic described in Definition 39.

Even if we generalise our present account and allow for nonstandard models, we will not be able to provide valuations for reflexive frames (see section 11). In general, our results make the limitations imposed by Löb’s Theorem and its relatives explicit.

§9. The Fixed Point Φ^{κ}(L_{□}). By Corollary 45, K4 is the set of sentences valid in all transitive PW-models; Φ^{κ}(L_{□}) is the set of all sentences valid in a all transitive converse wellfounded PW-models. Therefore Φ^{κ}(L_{□}) is a subset of K4. 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 45 does not hold if (i) is restricted to converse wellfounded frames.

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

Theorem 46. The set Φ^{κ}(L_{□}) is Δ_{2}^{1} but neither Σ_{1}^{1} nor Π_{1}^{1}.

Proof. Φ is a Δ_{1}^{1}-operator; hence its fixed point Φ^{κ}(L_{□}) is Δ_{2}^{1} (see, for example, Hinman [22, Theorem 3.10]).

As (3) before Lemma 24 shows, Φ^{κ}(L_{□}) is essentially the Σ_{1}-theory of a reasonably high countable level of the Gödel hierarchy, well beyond the first admissible level. Its complexity is thus well beyond Π_{1}^{1}. This will have been amply demonstrated to those familiar with the Gödel hierarchy, or the ramified analytical hierarchy. However, we can now give a direct demonstration of this fact.

In order to show that Φ^{κ}(L_{□}) is not Π_{1}^{1} we use the match between X_{α} = Φ^{α}(L_{□}) and Σ_{1}-Th(L_{α}) established in Lemma 24.

We show that Φ^{κ}(L_{□}) is at least Π_{1}^{1} in a complete Π_{1}^{1}-set of integers (so of the degree O^{O} where O is Kleene’s ordinal notation system for ordinals up to ω_{1}. O^{O} is Kleene’s set of ordinal notations relativised to the set O, and hence is a complete Π_{1}^{1}(O)-set of integers.

Let B be a sentence with B ∈ X_{ω_{2}+1} \ X_{ω_{2}} where ω_{2} is the second admissible ordinal.

We define the following recursive function f for Σ_{1}-sentences τ of the language of set theory:

f(τ) := (C_{1}(⌜τ⌝) ∧ (C_{1}(⌜τ⌝) ↔ (¬B ∧ ¬◇⌜B⌝))).

Put f(n) = 0 for other n that are not Σ_{1}-sentences of the language of set theory.

Then f^{−1}′′(X_{κ}) is the set Σ_{1}-Th(L_{ω_{2}}). The latter is known to be (recursively isomorphic to) O^{O} (see [23]). Thus, O^{O} is recursively reducible to X_{κ}. Hence X_{κ} cannot be Π_{1}^{1}, or else so would O^{O}. ⊣

The method for establishing the lower bound is general and can be applied also to admissibles greater than ω_{2}.

The previous theorem shows explicitly that Φ^{κ}(L_{□}) is complex and hence cannot be equal to K4. We can exhibit an explicit sentence that is true in all converse wellfounded worlds, but fails to be in K4.

Let A be in X_{ω_{1}+1}\X_{ω_{1}} (any such will do for the proof). For the sake of definiteness we can obtain one as follows:

There is a Π_{3}-sentence τ in L_{{ ˙∈}} so that L_{ω_{1}} ⊧ τ but for no smaller β does L_{β} ⊧ τ. For example it can be shown there are monotone total functions on ω cofinally increasing into ω_{1} which are Σ_{2}-definable over L_{ω_{1}}; the statement that such a function is cofinal and defined on all of ω yields such a τ.

Thus τ is in the Π_{3}-Th(L_{ω_{1}}). Let A = C_{4}(⌜τ⌝). Now let A be an illfounded KP-model of τ with WFP(On(A)) = ω_{1} (an adaptation of the argument of Proposition 37 gives us such an A). Let e ∈ ω be an index for a recursive linear order (in fact a pseudo-wellorder) that A thinks is wellfounded, but is in fact illfounded. (Such an e must exist as τ is true in A only at A’s first “admissible” ordinal, b say, so first at (L_{b})_{A}; A however thinks that b is the supremum of all recursive wellorders: hence there is an index e for a recursive linear ordering e which is isomorphic to an initial segment of On(A) but is in fact illfounded.)

Let n be the code of the sentence expressing that {e} is illfounded.

Theorem 47. ◇⌜A⌝ ⟶ C_{1}(n) is not provable in K4, but it is true in all converse wellfounded worlds.

Proof. In A we can define a model ⟨W, R, V ⟩ and with A thinking that the frame is converse wellfounded and that ◇⌜A⌝ is true in some world w ∈ W. (It suffices to have ⟨W, R^{−1}⟩ isomorphic to an initial segment of On(A) containing b and some w with wRb.) However we could not have that C_{1}(n) were true at w, as this would mean that A recognised e’s illfoundedness—which it cannot. Thus K4 does not prove the displayed sentence.

Let ⟨W, R, V ⟩ be any model and w any converse wellfounded world in W with ◇⌜A⌝ holding at w. L_{ω_{1}+1} realises that {e} is truly illfounded: the wellfounded part of {e} is mapped by its ranking function onto ω_{1} by a Σ_{1}-recursion over L_{ω_{1}}. Hence the rest of the field of {e}—that is, its illfounded part, U say, is definable over L_{ω_{1}} and hence is a set in L_{ω_{1}+1}, and the latter is a model of “U has no {e}-minimal element” (a Σ_{1}-statement: ∀k ∈U ∃m∈U[{e}(⟨m, k⟩) = 1]—the bracketed matrix expressing that “m is {e}-below k”). Therefore ◇⌜A⌝ ⟶ C_{1}(n) holds at w. ⊣

§10. Theories for Φ^{κ}(L_{□}). Investigations into axiomatic theories based on PA plus an additional truth or necessity predicate axiomatised by suitable axioms turned out to be interesting and fertile (see, e.g., Cantini [9] for an overview). In many cases these theories are supposed to capture a semantical construction like Kripke’s [26] theory. In this tentative section we explore the prospects of a strong theory for Φ^{κ}(L_{□}).

We introduce some new notation. The quantifiers ∀a and ∀b range over sentences of the language L_{□}; they can be defined in the usual way in L_{PA}. The quantifier ∀a(v) ranges over all formulae of L_{□} with at most one free variable. The function sending the code of a formula to the code of its negation is expressed in L_{PA} by ¬., and similarly for other connectives and quantifiers. For the notation see also Feferman [11].

The following sentences are valid in Φ^{κ}(L_{□}), that is, for any sentence A below we have (ℕ, Φ^{κ}(L_{□})) ⊧ A: A1 All axioms of PA including all induction axioms in L_{□} A2 ∀a (Bew_{PA}(a) → □a) A3 ∀a, b (□(a\overrightarrow{.}b) → (□a → □b)) A4 ∀a (□□ .ȧ ↔ □a) A5 ∀a (□¬.a → ¬□a) A6 ∀a(v) (□∀.v a(v) ↔ ∀x □a(ẋ/v)) A7 ∀x (□⌜A(ẋ)⌝ → A(x)) for all A(v) ∈ L_{□} The theory given by A1–A7 is at least as strong as ID_{1}. This follows from results proved by Friedman and Sheard [14].

By Theorem 46 the fixed point Φ^{κ}(L_{□}) is more complex than the minimal fixed point of Kripke’s construction (see Burgess [7, 8] for more on the complexity of truth-theoretic constructions). We are unable to say whether the theory A1–A7 as it stands is already a correspondingly stronger one than ID_{1}. The scheme A7 already represents the full reflection property of γ.

To find a theory that more aptly describes Φ^{κ}(L_{□}) and has greater proof-theoretic strength than the simple axioms A1–A7 perhaps one has to add axioms expressing this reflection more fully. We can express that γ is a limit of Π_{n}-reflecting ordinals by adding the following. We let Form_{n} be a recursive one-place predicate enumerating the Π_{n}-formulae of L_{□} with one free variable. Define

Φ_{n}: ∀x ∀a(v) (Form_{n}(a) → (□a(ẋ/v) → a(x/v))).

Then define the following scheme:

∀b(□(⌜Φ_{n}⌝\overrightarrow{.}□ .b) → □b). (A8_{n})

This scheme is true in Φ^{κ}(L_{□}) also, for each n. Similarly one could express that γ is a limit of points, each of which was, for all n, a limit of Π_{n}-reflecting ordinals, but it is not clear whether this process carries us any further forward. It is also worth noting that at each world of a valuation along a converse wellorder shorter than κ, one may use Gödel numbers of sentences that become true at worlds accessible to it, as “labels” of those worlds, and indeed to reconstruct the whole of the ordering above any world, together with the valuations associated to those worlds.

§11. Nonstandard PW-Models. So far we have concentrated on models of the form (ℕ, S) where ℕ is the standard model of L_{PA} and S is a set of standard numbers. As a consequence, the Barcan formula is valid in all worlds on our approach.

In the following two sections we sketch alternative approaches where some other model than ℕ is used. While the next section is concerned with models for other languages than L_{PA}, we consider nonstandard models of L_{PA} in the present section, more precisely, instead of (ℕ, S) we employ certain models of the form (M, S) where M is a model of full arithmetic, i.e., of all arithmetical truths. Of course, there are further options, like arbitrary models of PA, but we will not explore them in the present paper.

By invoking nonstandard models we shall be able to construct valuations for the frame ⟨ω, Suc⟩ of Example 9, which does not admit a valuation if the PW-model is based on the standard model ℕ. Thus we shall be able to construct valuations for frames without dead ends, whereas on the standard account all frames admitting valuations must have a dead end according to Theorem 32.

In a standard model (ℕ, S) the extension S of □ is a set of numbers. If we pass to nonstandard models (M, S), we have to decide whether we shall admit nonstandard numbers in S as well. In a nonstandard model M the syntactical predicates expressible in L_{PA} (like “x is a propositional tautology”) apply to standard as well as to nonstandard elements of M. Thus if we want to have sentences like “All propositional tautologies are necessary”, i.e., ∀a(Taut(x) → □x) as valid, then S must comprise also nonstandard elements of M.

This poses a problem for the applicability of our Definition 2, which says that the extension of □ at a world w is just the set of sentences true at all worlds seen by w. If this condition is reformulated for the nonstandard case, we have to say what it means for a nonstandard sentence, i.e., a sentence in the sense of M, to be true at a world. There are several ways of defining truth for nonstandard sentences. Here we use (a slight modification of) the notion of a satisfaction class (see Kaye [24] and Kotlarski [25] for overviews).

Let a model M be given. And let S_{1} be a set of elements of M. Then S_{2} is a satisfaction class for (M, S_{1}) if and only if the following conditions are met:

(i) All elements of M which are true atomic sentences in the sense of M are in S_{2}. (These are the elements a such that M ⊧ Tr_{0}(ā), where Tr_{0}(x) is a truth definition for atomic sentences of L_{□}.)

(ii) S_{2} commutes with all quantifiers and connectives in the sense of M. For instance, the negation of a sentence in the sense of M is in S_{2} if and only if the sentence itself is not in S_{2}.

According to results by Kotlarski, Krajewski and Lachlan [25, 28] and assuming that M is a countable nonstandard model of PA, there is a satisfaction class for (M, S_{1}) if and only if (M, S_{1}) is recursively saturated. Every countable recursively saturated model has uncountable many satisfaction classes.

The following is a modification of Theorem 2 of Leitgeb [30]:

Theorem 48. There is a model M elementarily equivalent to ℕ and a function V on ω such that V (n) is a satisfaction class for (M, V (n+1)). Moreover all induction axioms hold in all models (M, V (n)).

V may be seen as a valuation for the frame ⟨ω, Suc⟩ where a world n sees a world k if and only if k = n + 1. For every n, V (n) contains all (standard) sentences true at all immediately preceding worlds, i.e., true in (M, V (n + 1)). In addition V (n) is a satisfaction class for (M, V (n + 1)). In this sense V (n) is a set comprising all L_{□}-sentences in the sense of M that are true at all preceding worlds. However, V (n) is only one of many such classes because there are many different satisfaction classes.

§12. 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.

Definition 49. 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 Section 4 can be used to show the following. Let M be a countable acceptable structure (in the sense of [35], 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}}(L_{□}) 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 [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 32 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 sections 4 & 5 go through mutatis mutandis. The formulae 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 is interpreted at every world by the standard model. Also the domain stays constant throughout all worlds.

As announced above, we show how to extend our account to languages with contingent vocabulary whose interpretation varies from world to world. The domains of the worlds are allowed to differ as long as they contain the natural numbers. We shall still keep the interpretation of the arithmetical vocabulary fixed; it has thus the status of ‘logical’ vocabulary. The problems (e.g., the Church–Langford argument) connected with this assumption have been touched upon in the first section and will be discussed in another paper.

In order to expand our account to languages with contingent vocabulary, we redefine the language L_{□}. In this section L_{□} is assumed to contain all arithmetical vocabulary, a relativizing predicate N, □ and arbitrary further constants, function and predicate symbols. L_{PA} is the sublanguage of L_{□} containing only arithmetical vocabulary where all quantifiers are relativised to Nx. The relativization of the quantifiers is needed because the domains of our models may contain objects beyond the numbers.

A standard model for L_{□} (redefined in this way) is a model of L_{□} that interprets the sublanguage L_{PA} of L_{□} in the standard way. Thus the standard model of arithmetic is a submodel of every standard model of L_{□} and Nx applies in every standard model of L_{□} exactly to all (standard) numbers. A standard model of L_{□} also needs to fix the interpretation of the arithmetical functions applied to objects that are not numbers.

Definition 2 is then modified in the following way:

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

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

Thus V does not only interpret □ at every world but it covers also the contingent vocabulary, i.e., the vocabulary not in L_{PA}.

If the notion of a PW-model is extended in this way, the main arguments of the paper still go through. In particular, our partial solutions of the Characterisation Problem and the Completeness Theorem 40 still apply. Valuations, however, are no longer unique because even converse wellfounded frames admit valuations that interpret the contingent vocabulary in different ways (and consequently also □).

The interpretation of the contingent vocabulary is not completely arbitrary. In a converse illfounded model there cannot be a sentence that is true at all converse wellfounded worlds and false at all converse illfounded worlds because Löb’s Theorem rules out such valuations. Therefore there are restrictions on the interpretation of the contingent vocabulary.

In such PW-models the Barcan formula for arithmetical quantifiers, i.e., those restricted by Nx, will still obtain. In order to formulate the Barcan formula and its converse also for unrestricted quantifiers we would have to appeal to assignments and we would have to conceive □ as a binary predicate. In contrast to operator quantified modal logic, the converse Barcan formula does not drop out from our framework as a logical truth. Furthermore shrinking domains are allowed, i.e., a world may see another world with a smaller domain.

With contingent vocabulary we can express further conditions on frames. The following axiom forces infinite branching, that is, every world where it holds is either a dead end or sees infinitely many other worlds:

□⌜⊥⌝ ∨ ∀x(Nx → ◇⌜Gẋ ∧ ∀y(Gy → ẋ=y ∨ ¬Ny)⌝).

G is here a predicate symbol distinct from □ and not in the arithmetical language.

We plan to treat canonicity and further classical topics of operator modal logic as applied to our framework in a future paper.

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] John P. Burgess, The truth is never simple, The Journal of Symbolic Logic, vol. 51 (1986), pp. 663–81.

[8] , Addendum to ‘The truth is never simple’ , The Journal of Symbolic Logic, vol. 53 (1988), pp. 390–92.

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

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

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

[12] Solomon Feferman and Clifford Spector, Incompleteness along paths in progressions of theories., The Journal of Symbolic Logic, vol. 27 (1962), pp. 383– 390.

[13] Hartry Field, Disquotational truth and factually defective discourse, The Philosophical Review, vol. 103 (1994), pp. 405–452.

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

[15] Giorgio Germano, Metamathematische Begriffe in Standardtheorien, Archiv für Mathematische Logik, vol. 13 (1970), pp. 22–38.

[16] Dorothy Grover, Joseph Camp, and Nuel Belnap, A prosentential theory of truth, Philosophical Studies, vol. 27 (1975), pp. 73–125.

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

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

[19] Volker Halbach, Hannes Leitgeb, and Philip Welch, Possible worlds semantics for predicates, Intensionality (Los Angeles) (Reinhard Kahle, editor), Association for Symbolic Logic, 2002, to appear.

[20] Joseph Harrison, Recursive pseudo-well-orderings., Transactions of the American mathematical Society, vol. 131 (1968), pp. 526–543.

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

[22] Peter Hinman, Recursion theoretic hierarchies, Springer, Berlin, 1978.

[23] Carl Jockusch and Stephen Simpson, A degree theoretic definition of the ramified analytical hierarchy, Annals of Mathematical Logic, vol. 10 (1975), pp. 1– 32.

[24] Richard Kaye, Models of Peano arithmetic, Oxford Logic Guides, Oxford University Press, 1991.

[25] Henryk Kotlarski, Stanislav Krajewski, and Alistair Lachlan, Construction of satisfaction classes for nonstandard models, Canadian Mathematical Bulletin, vol. 24 (1981), pp. 283–293.

[26] Saul Kripke, Outline of a theory of truth, Journal of Philosophy, vol. 72 (1975), pp. 690–712.

[27] , Is there a problem about substitutional quantification?, Truth and meaning: Essays in semantics (Gareth Evans and John McDowell, editors), Clarendon Press, Oxford, 1976, pp. 325–419.

[28] Alistair Lachlan, Full satisfaction classes and recursive saturation, Canadian Mathematical Bulletin, vol. 24 (1981), pp. 295–297.

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

[30] , Truth as translation - part B, Journal of Philosophical Logic, vol. 30 (2001), pp. 309–328.

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

[32] , Truth, vagueness, and paradox: An essay on the logic of truth, Hackett Publishing, Indianapolis and Cambridge, 1991.

[33] Richard Montague, Syntactical treatments of modality, with corollaries on reflexion principles and finite axiomatizability, Acta Philosophica Fennica, vol. 16 (1963), pp. 153–67, Reprinted in [34, 286–302].

[34] , Formal philosophy: Selected papers of richard montague, Yale University Press, New Haven and London, 1974, Edited and with an introduction by Richmond H. Thomason.

[35] Yiannis N. Moschovakis, Elementary induction on abstract structures, Studies in Logic and the Foundations of Mathematics, no. 77, North-Holland and Elsevier, Amsterdam, London and New York, 1974.

[36] Arthur Pap, Analytische Erkenntnistheorie, Springer, Wien, 1955.

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

[38] 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.

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

[40] Gerald E. Sacks, Countable admissible ordinals and hyperdegrees, Advances in Mathematics, vol. 99 (1976), pp. 213–262.

[41] Paul Schweizer, A syntactical approach to modality, Journal of Philosophical Logic, vol. 21 (1992), pp. 1–31.

[42] Brian Skyrms, An immaculate conception of modality, Journal of Philosophy, vol. 75 (1978), pp. 368–387.

[43] Barry Hartley Slater, Paraconsistent logics?, Journal of Philosophical Logic, vol. 24 (1995), pp. 451–454.

[44] Peter Strawson, Truth, Analysis, vol. 9 (1949), pp. 83–97.

[45] Albert Visser, Semantics and the liar paradox, Handbook of philosophical logic (Dov Gabbay and Franz Günthner, editors), vol. 4, Reidel, Dordrecht, 1989, pp. 617–706.

UNIVERSITÄT KONSTANZ

FACHGRUPPE PHILOSOPHIE

POSTFACH 5560 D 21

78434 KONSTANZ, GERMANY and

DEPARTMENT OF LOGIC & PHILOSOPHY OF SCIENCE

UNIVERSITY OF CALIFORNIA 3151 SOCIAL SCIENCE PLAZA IRVINE, CA 92697-5100, U.S.A.

Current address: Universität Göttingen, Philosophisches Seminar, Humboldtallee 19, 37073 Göttingen, 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

UNIVERSITÄT WIEN

INSTITUT FÜR FORMALE LOGIK WÄHRINGER STRASSE 25 1090 WIEN, AUSTRIA

Current address: Universität Bonn, Mathematisches Institut, Beringstraße 6, 53115 Bonn, Germany

E-mail: p.welch@bristol.ac.uk