Higher-Order Contingentism, Part 1: Closure and Generation

Abstract

This paper is a study of higher-order contingentism – the view, roughly, that it is contingent what properties and propositions there are. We explore the motivations for this view and various ways in which it might be developed, synthesizing and expanding on work by Kit Fine, Robert Stalnaker, and Timothy Williamson. Special attention is paid to the question of whether the view makes sense by its own lights, or whether articulating the view requires drawing distinctions among possibilities that, according to the view itself, do not exist to be drawn. The paper begins with a non-technical exposition of the main ideas and technical results, which can be read on its own. This exposition is followed by a formal investigation of higher-order contingentism, in which the tools of variable-domain intensional model theory are used to articulate various versions of the view, understood as theories formulated in a higher-order modal language. Our overall assessment is mixed: higher-order contingentism can be fleshed out into an elegant systematic theory, but perhaps only at the cost of abandoning some of its original motivations.

1 Introduction

Higher-order contingentism is the view, roughly, that it is a contingent matter what propositions, properties, and relations there are. This paper aims to clarify, motivate, develop and critically assess a version of higher-order contingentism which we call the Fine-Stalnaker view, which, drawing on Fine [5] and Stalnaker [18], is motivated and articulated in terms of the notion of automorphisms of modal space.¹

Propositions draw distinctions among possibilities by being true in some of them but not in others. Properties of individuals (hereafter understood as including polyadic relations) draw distinctions both among possibilities and among possible individuals by applying to certain possible individuals, but not others, in certain possibilities, but not in others. Higher-order properties (again, understood as including polyadic relations) likewise draw distinctions both among possibilities and among possible propositions and possible properties of lower types. Higher-order contingentism therefore raises the prospect of it being a contingent matter which such distinctions there are to be drawn.²

The view does not entail that it is a contingent matter which distinctions among possibilities and possibilia there are to be drawn. This is because the relation between higher-order entities and the modal distinctions they draw may be many-one, as will be the case if necessarily equivalent propositions, and necessarily co-extensive properties, sometimes fail to be identical. In other work we discuss the possibility of accepting a hyperintensional theory of properties and propositions that, although a version of higher-order contingentism, nevertheless entails that it is a non-contingent matter what modal distinctions there are to be drawn.³ But we will not discuss such eccentric views here. Instead, we take as a working hypothesis the widely held assumption that, if it is contingent what higher-order entities there are, then it is likewise contingent what distinctions among possibilities and possibilia there are to be drawn – this assumption will normally be left implicit. In Section 3.4 we show how to make this assumption formally precise without begging the question of whether properties and propositions are individuated hyperintensionally.

Our initial characterization of higher-order contingentism was ‘rough’ in the following respect. Although we have spoken of propositions, and of properties of different ‘orders’/‘types’, such talk should be understood as our a way of communicating in English claims we think are more perspicuously formulated in a higher-order language. For example, talk of ‘propositions’ is our way of communicating claims we will go on to formalize using quantification into sentence position; talk of ‘properties of individuals’ is our way of communicating claims we will formalize using quantification into predicate position; and talk of properties ‘of higher types’ (e.g., ‘properties of propositions’) is our way of communicating claims we will formalize using quantification into corresponding syntactic positions (e.g., the position of sentential operators). Here is not the place to discuss the status of such higher-order languages as tools for metaphysical theorizing.⁴ Although much is contentious, it is widely held that such languages, whatever their appropriate interpretation, are the best available tools for bringing formal discipline to the metaphysical questions in the vicinity. While we believe such languages can be understood on their own terms, those who think otherwise can treat higher-order quantification as tacit first-order quantification over an appropriately abundant yet stratified realm of abstract objects.

With three significant exceptions, there has been hardly any systematic discussion of higher-order contingentism. The exceptions are Fine [5], Stalnaker [18, Chapters 1 and 2 and Appendix A], and Williamson [19, Sections 6.3–6.4], from which the name of the view is taken. Fine’s paper, which is by far the most systematic development of the view, seems to have gone almost completely unnoticed: Williamson cites it only in passing, and Stalnaker does not cite it at all. Its neglect is understandable: the paper is very difficult, containing only a brief philosophical preamble followed by an extensive but compressed technical development, in which the theory of higher-order contingentism is treated as a means to various other philosophical ends, and general principles are laid down without the examples needed to give a feel for their intuitive content. Stalnaker gives a more leisurely philosophical exposition, but the details of the view are likewise presented in an condensed appendix in which he sketches a formal model of contingency in what propositions there are; unlike Fine, purported examples of higher-order contingency are adduced without any general principles offered in their support. As for Williamson, the structure of his argument against higher-order contingentism is at times difficult to follow and the argument itself is highly condensed at crucial stages. A main aim of the present paper is to clarify, synthesize, and expand on the views and arguments of these three authors.

There are three main reasons to care about higher-order contingentism. The first is intrinsic interest – not only of the thesis itself, but also of the particular higher-order contingentist theories we will be discussing, which offer mathematically elegant and philosophically enticing pictures of modal reality. The second reason is that higher-order modal languages are a rich and fruitful tool for metaphysical theorizing, so having a better understanding of higher-order contingentism is of foundational importance. The third and perhaps most significant reason is that the question of higher-order contingentism is connected to the question of first-order contingentism – the view that it is a contingent matter what individuals there are. Its negation – first-order necessitism – is a radical, some would say incredible, position. Yet many have thought that first-order contingentism leads inexorably to higher-order contingentism, making the tenability of the latter a necessary condition on the tenability of the former. Others have taken the opposite perspective, and argued that first-order contingentists had better be higher-order necessitists. They are moved by the worry that, without all of the modal distinctions higher-order necessitism guarantees, first-order contigentism falls victim to a charge of expressive inadequacy. We discuss these issues in other work.⁵

We will begin with a non-technical exposition of our technical results and their philosophical significance. In Section 2.1 we explain the motivations for higher-order contingentism. In Section 2.2 we consider how best to develop the view into a systematic theory, drawing on the ideas of Fine and Stalnaker. In Section 2.3 we argue that this view stands up to Williamson’s main challenge to higher-order contingenism. In Section 2.4 we point out a fundamental problem for the versions of higher-order contingentism under discussion – namely, that their formulation requires drawing modal distinctions that, according to the theories themselves, do not exist to be drawn – and explain how the Fine-Stalnaker view must be modified in order avoid such incoherence. In Section 2.5 we show that the modification in question has serious philosophical costs. Apart from the conclusion, the remainder of the paper is an extended model-theoretic investigation of higher-order contingentism, in which the arguments and theories outlined informally in Section 2 are articulated more precisely and in much greater detail.

2 Informal Exposition

2.1 Motivating Higher-Order Contingentism

The basic idea behind higher-order contingentism is that contingency in what individuals there are leads to contingency in what properties and propositions there are. Consider the proposition that you exist and the property of being identical to you. Now suppose you had never been born. The first-order contingentist thinks that, had you never been born, there would have been no such thing as you. The higher-order contingentist thinks that, moreover, there would have been no such thing as the proposition that you exist or the property of being identical to you. Indeed, most of them think that there would have been no proposition necessarily equivalent to the proposition that you exist, nor any property necessarily co-extensive with being identical to you. In this sense the proposition that you exist and the property of being identical to you each draws a modal distinction that, had you never been born, there would not have been to be drawn. Even Williamson, who rejects higher-order contingentism, thinks that first-order contingentism is more plausibly combined with higher-order contingentism than with higher-order necessitism.

This motivation of higher-order contingentism suggests a deductive argument for the view, based on the premises of first-order contingentism and the claim that necessarily, every individual is such that, necessarily, there is a property necessarily co-extensive with being identical to that individual only if there is such a thing as that individual. However, this claim is implausible. Consider a spare handle and blade that could easily have been (but never will be) joined to form a knife. It is natural to think that, although nothing there is could have been such a knife, nevertheless the property of being something that actually would have been a knife made from the handle and the blade had the two been joined is a property that, had such a knife been made, would have been necessarily co-extensive with being identical to that knife. Since there actually is such a property, it is not the case that any property that possibly ‘singles out’ an individual must actually single out some individual (where a property F singles out x just in case being F is necessarily co-extensive with being identical to x). In other words, it is not in general true that every haecceitity is the haecceity of something, where F is a haecceity just in case it is possible that there be an individual that it singles out. So, had such a knife been made, then it would have been a counterexample to the above principle, since it would then be possible (because actually the case) that it have a haecceity without there being any such thing as it. (An analogous point applies concerning propositions that are possibly such that some individual’s existence is necessarily equivalent to their truth.)

Fine, Stalnaker and Williamson are sensitive to this point. Stalnaker’s endorsement of higher-order contingentism – and Williamson’s conditional acceptance of it on the assumption of first-order contingentism – are not based on any such deductive argument. Rather, they are based on particular judgements concerning what properties there would have been in specific counterfactual circumstances in which certain individuals were absent. By contrast, Fine’s motivation for higher-order contingentism is more systematic, and is driven by a general principle connecting which individuals there are to which properties and propositions there are (although the principle is more subtle than the one discussed in the previous paragraph). In the next section we outline Fine’s motivating idea.

2.2 The Fine-Stalnaker View

Fine’s central principle is the claim that necessarily, there are all and only the modal distinctions that can be drawn in terms of existing individuals and certain necessarily existing qualitative properties of individuals. The key question for his view is how to understand a modal distinction’s being ‘able to be drawn’ in certain terms, and hence how the view is going to vindicate our purported pre-theoretical higher-order-contingentist judgments about cases. It will help to start by considering the following example. (The example will be couched using talk of possible worlds – we will return shortly to the question of whether such talk is legitimate in the present context.)

Consider a world w ₁ in which there exist two hydrogen atoms a ₁ and a ₂ in otherwise empty space. Suppose further that none of the particles composing a ₁ or a ₂ actually exists, and that the atoms are, respectively, in different energy states E ₁ and E ₂. Now consider a second world w ₂, qualitatively identical to w ₁, but in which a ₁ is in energy state E ₂ and a ₂ is in energy state E ₁. The higher-order contigentist will deny that there are actually any propositions that distinguish w ₁ from w ₂, or properties that are haecceities of a ₁ or of a ₂. This result is predicted by Fine’s view, since we seem to have no way to distinguish w ₁ from w ₂ or a ₁ from a ₂ in qualitative terms or in terms of individuals that actually exist.

Fine formalizes this idea using the resources of variable-domain intensional model theory for a modal higher-order language, described in Section 3. The central notion, described in Section 4.1, is that of an automorphism of modal space: a function that permutes all ‘worlds’ and all ‘possible individuals’ in a model such that, if it maps a world w to v and a possible individual x to y, then x exists in w if and only if y exists in v.⁶ Such an automorphism is fixed on a world w just in case it maps w to itself and maps every possible individual that exists at w to itself.⁷ For any automorphism, we can ask whether it preserves a certain property, where properties are modeled as intensions – functions from worlds to the set of tuples of entities that at those worlds satisfy the property. For illustration, we will consider propositions (which we may think of as zero-place properties) and monadic properties of individuals, although the notion is well defined for properties of all types. An automorphism preserves a proposition p just in case, if it maps a world w to a world v, then p is true in w if and only if it is true in v; it preserves a monadic property of individuals F just in case, if it maps a world w to v and a possible individual x to y, then x has F at w if and only if y has F at v. Fine’s idea is that the properties (modeled as intensions) that exist at a world w are those that are preserved by all automorphisms fixed on w that preserve certain qualitative properties of individuals. Let us assume that there is an automorphism of modal space fixed on the actual world that preserves the relevant qualitative properties of individuals yet permutes w ₁ and w ₂ and a ₁ and a ₂. It then follows from Fine’s proposal, by the definition of preservation, that no actually existing proposition is true at w but not at v (or vice versa), and no actually existing property applies to a ₁ at w ₁ but not to a ₂ at w ₂ (and hence no actually existing property is a haecceity of a ₁).

In the interest of conveying Fine’s basic idea, the above description is somewhat sloppy in failing to sharply distinguish models from the modal reality they model. The model theory is described precisely in Sections 3 and 4. As for the picture of modal reality the proposal is meant to capture, consider the following analogy. Let the vertices of a cube represent points in modal space. For any vertex v, we can distinguish certain of the vertices in terms of their geometric relations to v. But we cannot distinguish all such vertices – e.g., we cannot in this way distinguish two vertices adjacent to v. The distinctions among vertices we can draw in this way are exactly those that remain invariant when we rotate the cube about its axis through v. This fact corresponds to the idea that the automorphisms of modal space fixed on a point in it preserve exactly the modal distinctions that can be drawn at that point. Which such distinctions we can draw clearly depends on our choice of v. This fact corresponds to higher-order contingency.

We can see Fine’s view as a reductive account of higher-order being: there are exactly those properties and propositions that respect the identities of all existing individuals and of certain (perhaps all) qualitative properties. Call this the qualitative generation view. The view admits of variations. For example, in place of the qualitative ones, we might formulate the view in terms of a different class of underlying properties and propositions. It turns out, for example, that it makes a difference to the resulting higher-order modal logic if we allow third- and higher-order properties to figure in the ‘generating base’, or if we allow that the ‘generating’ properties can themselves have contingent being (as Stalnaker suggests qualitative properties do) – see Section 4.4 for discussion.

More drastic departures from the Finean picture are also possible. Suppose, following Stalnaker, that we reject the qualitative/non-qualitative distinction, or at any rate reject the idea that qualitative properties, or any other independently specifiable class of properties, serves as a ‘generating’ basis in terms of which we can formulate a reductive theory of higher-order being. We might still appeal to automorphisms of modal space in fleshing out a theory of higher-order contingency. Suppose we simply eliminate the restriction to qualitative properties in the specification of which properties and propositions there are. The resulting view says that there are at a world w exactly those properties and propositions that are preserved by all automorphisms of modal space that are fixed on w and preserve all the properties and propositions there are at w. This view is non-reductive, since which properties and propositions there are at a world is specified in terms of the properties and propositions there are at that world. But it is far from trivial. In fact, as we show in Section 4.3, the model-theoretic constraint corresponding to this weaker view is satisfied by all and only those possible world models which satisfy the model-theoretic constraint corresponding to qualitative generation, at least if generating base is allowed to contain arbitrary relations and allowed to vary between worlds; we call such models closed. Henceforth, we will therefore refer to the general automorphism-based approach as the Fine-Stalnaker view of higher-order contingency, keeping in mind that Fine endorses qualitative generation while Stalnaker seems to accept only the idea of higher-order closure.

2.3 Comprehension Principles

Williamson [19, Sections 6.3–6.4] discusses two restricted higher-order comprehension principles, which he argues must come out valid on any good theory of higher-order contingentism. We agree with this claim, since these principles are exceedingly plausible and are needed to license patterns of modal reasoning in which we regularly engage. We therefore take them to be good test-cases for the variants of higher-order contingentism under consideration.

Williamson’s first comprehension principle is an ‘extensional’ comprehension schema Comp⁻. A comprehension schema is a principle that, for a schematically specified condition of a certain sort, says that there is a property the having of which corresponds to satisfying the condition. Such principles differ as regards what sorts of conditions are allowed and what sort of correspondence is ensured. Comp⁻ places no restriction whatsoever on the allowable conditions, but ensures only the weakest sort of correspondence: material equivalence. In the case of conditions with no free variables, the principle entails only that there is some proposition materially equivalent to the condition, which is of course trivial. In the case of conditions with a single free first-order variable, the principle is more substantive: it say, in effect, that for any (perhaps empty or singleton) plurality of individuals there is a property that is satisfied by each of them and by nothing else.⁸ A parallel point applies concerning pluralities of ordered pairs of individuals and conditions with two free first-order variables. The principle is ‘extensional’ because it tells us nothing about the behavior in counterfactual circumstances of the propositions and properties whose existence it guarantees. As such, it doesn’t guarantee our ability to draw any interesting modal distinctions.

The more interesting principle for our purposes is Williamson’s second condition of adequacy on any reasonable higher-order modal logic, Comp _C . Unlike Comp⁻, Comp _C only ensures the existence of properties and propositions corresponding to conditions that, roughly, are specified in terms of parameters all of which exist, where ‘existence’-talk is shorthand for existential quantification of the appropriate type. But unlike Comp⁻, Comp _C ensures intensional, not merely extensional, correspondence: that is, it ensures the existence of a property necessarily co-extensive with satisfying the relevant condition (or, in the case of conditions with no free variables, the existence of a proposition necessarily equivalent to the condition’s being the case). In a slogan: Comp _C guarantees the existence of properties and propositions corresponding to conditions that are specified only in terms of existent individuals, properties and propositions. (This gloss slides over the issue of hyperintensionality; a precise statement of the schema is given in Section 5.1.) For example, it guarantees that every proposition has a negation, in the sense that, for every proposition, there is another proposition that is necessarily equivalent to the first proposition not being the case. The same goes for any definable operation on properties and propositions.

As we show in Section 5.1, the qualitative generation view and the higher-order closure view, as formalized model-theoretically in Sections 3 and 4, stand up well to the test of validating Comp⁻ and Comp _C , as both schemas hold on all of the relevant models.

In his discussion, Williamson turns the requirement to support Comp⁻ and Comp _C into an argument for higher-order necessitism, by arguing that Comp⁻ and Comp _C cry out for a unified explanation, and so lend abductive support to an unrestricted comprehension principle Comp which entails higher-order necessitism. The fact that both the higher-order closure and qualitative generation views support Comp⁻ and Comp _C but not Comp undermines this conclusion.

(It might seem that Comp _C is strictly stronger than Comp⁻, in which case there would seem to be no question of the two principles crying out for a unifying explanation. Mustn’t any extensional distinction ‘among’ things there are be ‘specifiable’ in terms of those very things? The answer is negative if we assume a finitary language, although it becomes somewhat subtle if we move to an infinitary language.⁹ These issues are explored further in Section 5.2.)

2.4 Taking Higher-Order Contingency Seriously

It is time to be more careful in distinguishing models from the reality they model. We explained the Fine-Stalnaker view by glossing certain set theoretic structures as representing modal space, certain elements of those structures as representing possible individuals, and certain set theoretic constructs – intensions – as representing properties and propositions. But the higher-order contingentist denies that there really are all the individuals, properties, and propositions that there could be. So how are they to make sense of the models in terms of which they articulate their view?¹⁰

There are certain familiar strategies for making quantification over ‘merely possible’ individuals, properties, and propositions respectable. For example, existential quantification over ‘possible individuals’ can be eliminated by paraphrasing ‘for some possible individual x …’ as ‘possibly, some individual x is actually such that …’. The same goes for quantification over possible properties and propositions.¹¹ This much is familiar.

But such manoevers do not allow us to make sense of the claim that there are properties and propositions corresponding to exactly those intensions that are preserved by all automorphisms of modal space satisfying certain conditions. In specifying the class of models, we quantified over all intensions in, and all automorphism of, those models. But not every intension in a model need be in the higher-order domain of some world of the model. A similar point applies to automorphisms: Permutations of possible individuals correspond to binary relations, which we are modeling as certain sorts of intensions. But not every permutation of the possible individuals in a model need correspond to an intension in the higher-order domain of some world of the model. Similarly, permutations of possible worlds can be thought of as binary relations on ‘world propositions’, relations which we are also modeling intensionally. But not every permutation of the worlds of a model need correspond to an intension in the higher-order domain of some world of the model. Informally: not all intensions in a model, and automorphisms of a model, will even possibly exist according to the model. After all, they correspond to the very sort of modal distinctions that higher-order contingentism claims have contingent being. So even if higher-order contingentists can help themselves to quantification over possible entities of all types, it is not clear that they have enough modal distinctions to make sense of their own model theory.

The severity of the problem only becomes apparent when we descend from the realm of model theory to consider how we might capture the Fine-Stalnaker view in our higher-order modal language. We can easily define what it is for a binary relation among individuals to be a permutation of all possible individuals, and what it is for a binary relation on propositions to be a permutation of all possible world-propositions. We can also define, for properties of all types, what it is for them to be preserved by a pair of such permutations. We can then take the infinite conjunction of such preservation claims for each type, thereby expressing the claim that an automorphism preserves the existing entities of all types. This allows us to capture the higher-order closure version of the Fine-Stalnaker view in the form of an object language comprehension schema that says, as regards any condition ϕ(v ₁,…, v _n ): there is a property intensionally equivalent to satisfying ϕ(v ₁,…, v _n ) just in case, for any possible permutations of possible individuals and of possible worlds that together constitute an automorphism of modal space fixed on the actual world that preserves all existing properties of all types, that automorphism preserves ϕ(v ₁,…, v _n ). Call this principle Comp _{F S} ; we characterize it more precisely in Section 5.3.

As we will prove in Section 5.4, Comp _{F S} is not valid on the class of models described in the previous section. This is for the reason described above: in defining that class of models we quantified over automorphisms of the models that did not even possibly exist according to the models. The invalidity of Comp _{F S} shows that we have not taken higher-order contingency seriously enough in formulating the view, since we have tacitly appealed to distinctions among possibilities that, according to the view itself, do not (and could not) exist to be drawn. The model theory needs revision if it is to do justice to the Fine-Stalnaker view characterized in terms of automorphisms of modal space.

Fortunately, the model theory can be straightforwardly modified so as to validate Comp _{F S} . Say that a model is internally closed just in case, for any world w, an intension is in the domain of w just in case it is preserved by all automorphisms of the model that are (i) fixed on w, (i i) preserve all intensions in the domain of w, and (i i i)possibly exist according to the model – where, as above, an automorphism of a model possibly exists according to it just in case the intensions corresponding to the world-permutation and to the possible-individual-permutation are each in the domain of some world of the model. The resulting model theory validates Comp _{F S} . In fact, it turns out to be a proper restriction of the class of models from the previous section, and hence validates Comp⁻ and Comp _C (as we show in Sections 6.1 and 6.2).

The resulting models of the qualitative generation and higher-order closure views should only be seen as one option for resolving the tension which comes with using closed models. Instead of quantifying over possible permutations of individuals and worlds, we could formulate variant views by quantifying only over existing permutations. We briefly discuss such variants in Section 6.6, and continue in Section 6.8 with the question whether any sense can be made of the idea of quantifying over impossible permutations. In both cases, we conclude that such variants are unlikely to be any more plausible than the ones on which we focus.

2.5 Implications of Internalization

We have argued that proponents of the Fine-Stalnaker view ought to accept Comp _{F S} as an object-language expression of their view, and, as a result, should restrict the class of admissible models to those that are internally closed. Let us now consider the philosophical ramifications of this restriction.

Luckily, there turn out to be a range of non-trivial internally closed models, so the view does not immediately collapse. However, as we show in section 6.4, the view does not have any realistic models that respect the requirement that properties hold only among existent entities, variously known as ‘serious actualism’, the ‘falsehood principle’, ‘negative free logic’, and the ‘being constraint’.¹² This is because there are pairs of incompossible possible individuals that are modally indistinguishable at some worlds.¹³ Given the Fine-Stalnaker view, as captured by Comp _{F S} , there must therefore be a possible permutation of all possible individuals that possibly maps one of the individuals to the other. But no possible relation can possibly relate incompossible individuals if we assume that, necessarily, all relations are existence entailing. The effect of the claim that all relations are existence entailing is that there won’t be enough non-trivial possible permutations of possible individuals for Comp _{F S} to achieve the desired effect: without the relevant permutations, the possible individuals will turn out to be distinguishable after all, contradicting the spirit of the view. We conclude that higher-order contingentists must deny that all relations are existence-entailing.¹⁴

A second consequence of the move to internally closed structures is that the idea of qualitative generation no longer makes sense as a reductive theory of higher-order being. This is because there are non-isomorphic internally closed models that are internally generated by the same pattern of qualitative properties holding among the same individuals at the same worlds – see Section 6.5. This ‘non-functionality’ of internal qualitative generation is a consequence of the self-referential character of the definition of internal closure: which automorphisms possibly exist according to a model is a matter of which world-proposition-permuting and possible-individual-permuting intensions are in the domain of some world of the model, which in turn depends on which automorphisms of the model possibly exist according to it. This result seems to stymie Fine’s reductive ambitions. Worse, the resulting class of models fails to validate Comp _C , further confirming that qualitative generation cannot be the whole story of higher-order being.

A third challenge raised by Comp _{F S} is that it fails to hold in very simple models one might have thought should surely be compatible with Fine’s and Stalnaker’s general vision about the nature of higher-order contingency. For example, as we show in Section 6.7, we cannot have a four-world model satisfying Comp _{F S} in which any three worlds are completely indistinguishable from the perspective of the fourth. Intuitively, that hypothesis might seem to be perfectly consistent with the general vision. But such thinking fails to take higher-order contingency seriously. In such a model, there would be no non-trivial permutations of worlds, and so any definable condition would be preserved by all automorphisms of modal space (since every condition is preserved by the identity automorphism), and so there would be no higher-order contingency according to Comp _{F S} , contradicting our assumption. One has the sinking feeling that the appealing vision of higher-order contingency suggested by Fine and Stalnaker’s motivating remarks in fact presuppose higher-order necessitism. The worry, in a nutshell, is that articulating that vision requires drawing modal distinctions that, according to the view itself, are not there to be drawn. Although the Comp _{F S} -based articulation of the view does not fall prey to that sort of incoherence, perhaps it is only at the cost of sacrificing the original motivating idea.¹⁵

Of course, the Fine-Stalnaker view is not the only version of higher-order contingentism; moreover, there is nothing wrong with using closed structures in a purely instrumental capacity to demonstrate the consistency of Comp⁻ and Comp _C with higher-order contingentism. But if the model theory is being used in such a thin way, it would seem to be merely a mathematical gadget where one might have hoped for a unifying metaphysical vision of the sort provided by Comp _{F S} .¹⁶

The next four sections carry out the formal investigation sketched so far in detail. A concluding section summarizes the findings.

3 Variable Domain Type Theory

In this section, we lay out the variable domain intensional type theory in which we formalize the Fine-Stalnaker view. It is based on the constant domain type theory in Gallin [10] and the use of variable domains in Kripke [14].

3.1 Syntax

We use a relational type theory rather than a functional one. In such a setting, every expression of a complex type combines with a finite sequence of expressions of a lower type to form a sentential expression. The only simple type is e, expressions of which denote individuals. Complex types are sequences of simpler types; e.g., the type of expressions combining with two terms of type e to form a sentential expression is 〈e, e〉. Consequently, the type of sentential expressions – expressions combining with no terms to form sentential expressions – is 〈〉.

We include infinitary devices in our language, allowing us to form the conjunction $\bigwedge {\Phi }$ of any set of formulas Φ and to bind any set of variables V using a universal quantifier ∀V. (For a standard reference on such infinitary languages, see Dickmann [2]. For set-theoretic details on how to precisely formulate an appropriate theory of syntax, see Karp [12].) More formally, we define:

Definition 1

Types are defined inductively by stipulating that e is a type and that any finite sequence of types is a type. Let T be the set of types.

For any type t and natural number n, we write t ⁿ for the n-tuple 〈t,…, t〉.

We construct our formal language $\mathcal {L}$ relative to a signature. The vocabulary of this language consists of the non-logical constants supplied by the signature, a proper class of variables for each type, and the symbols =, ¬, $\bigwedge$, □ and ∀. We call the last five elements the logical vocabulary, and the rest the non-logical vocabulary. Here and in the following, we indicate tuples by bars, e.g., writing $\bar {x}$ for 〈x ₁,…, x _n 〉, and relying on context to determine the length n.

Definition 2

A signature is a function σ on the set of types which maps every type to a set, the set of non-logical constants of that type.

Let σ be a signature. Expressions of $\mathcal {L}(\sigma )$ of the various types are defined inductively using the following rules, calling an expression a formula if it is of type 〈〉:

• Every variable of some type is an expression of that type.

• Every non-logical constant in σ of some type is an expression of that type.

• If ε and η are expressions of type e, then ε = η is a formula.

• If ε is an expression of type 〈t ₁,…, t _n 〉 and for all i≤n, η _i is an expression of type t _i , then $\varepsilon \bar {\eta }$ is a formula.

• If φ is a formula, then ¬φ and □φ are formulas.

• If Φ is a set of formulas, then $\bigwedge {\Phi }$ is a formula.

• If φ is a formula and V is a set of variables (of any type), then ∀V φ is a formula.

Closed formulas are called sentences (where a formula is closed if it has no free variables, and free variables are defined as usual).

Note that all complex expressions are formulas. As usual, we treat other standard operators as syntactic abbreviations. In particular, we write $\bigvee {\Phi }$ for $\neg \bigwedge \{\neg \varphi :\varphi \in {\Phi }\}$, ∃V φ for ¬∀V¬φ and ◇φ for ¬□¬φ. Similarly, we use obvious notational variations such as writing $\bigwedge _{i\leq n}\varphi _{i}$ for $\bigwedge \{\varphi _{1},\ldots ,\varphi _{n}\}$, or ∀x φ for ∀{x}φ. A binary conjunction $\bigwedge \{\varphi ,\psi \}$ is written more familiarly as φ∧ψ, and other standard Boolean operators of finite arity are defined using conjunction and negation as usual. We sometimes indicate the type of an expression by writing it in the index of its first occurrence in a formula, as in ∀x ^e x = x.

3.2 Models

We capture necessity and possibility by quantification over a set of elements which are informally interpreted as representing possible worlds. For simplicity, we assume that the correct logic of necessity is S 5, and more generally, that we can adequately model modal reality without adding an accessibility relation to our models. Like Kripke, we capture contingency in what individuals there are by specifying a domain of individuals for each world. Of course, the abstract structures defined below need not in fact contain possible worlds and fill their domains with merely possible individuals, but for familiarity and simplicity, we will engage in this sloppy way of speaking about the model theory. Giving a complete account of the methodology of possible worlds model theory for contingentists, as discussed by Williamson [19, Chapter 3], is not the topic of this paper.

Since we are formalizing a higher-order contingentist view, our models also have to represent the contingent existence of relations (including 0-ary and 1-ary relations), for which we use domain functions as well. We first define them formally and then discuss their informal interpretation in Section 3.4. The most perspicuous way of constructing such domains is by first fixing a set of worlds and a set of individuals, constructing a maximally inclusive set of intensions on them, and then specifying constraints on admissible domain functions which map each world to a subset of this set. Interpreting a variable X of a complex type $\bar {t}$ using a higher-order entity o, we will need o to tell us the truth-value of combining X with expressions of types t ₁,…, t _n in any world. We can do so by letting o be a function mapping each world to the set of tuples of entities of types t ₁,…, t _n to which it is supposed to apply at that world.

We thus bundle the choice of a set of worlds and individuals into a frame $\mathfrak {F}$, and inductively construct the set $\iota (\mathfrak {F})(t)$ of entities of type t that can be constructed out of these materials. To specify this set, we adopt the following notational conventions: For any set X, $\mathcal {P}(X)$ is the power set of X. For any natural number n and sets X ₁,…, X _n , π _i≤n X _i is the Cartesian product of these sets, i.e., the set of sequences 〈x ₁,…, x _n 〉 such that x _i ∈X _i for all i≤n. For sets X and Y, we write X ^Y for the set of total functions from Y to X.

Definition 3

A frame is a tuple $\mathfrak {F}=\langle W,I\rangle$ such that W and I are sets. Define $\iota (\mathfrak {F})$ to be the function on the set of types such that

$$\iota(\mathfrak{F})(e)=I$$

and for all types $t=\bar {t}$

$$\iota(\mathfrak{F})(t)=(\mathcal{P}({\Pi}_{i\leq n}\iota(\mathfrak{F})(t_{i})))^{W}$$

For any set of types U, we write $\iota _{\mathfrak {F}}^{U}$ for $\bigcup _{t\in U}\iota (\mathfrak {F})(t)$; in the case of singletons, we omit set-brackets, writing $\iota _{\mathfrak {F}}^{t}$ for $\iota _{\mathfrak {F}}^{\{t\}}$.

As usual, we sloppily identify a set of one-tuples (a one-place relation in the mathematical sense) with the corresponding set of elements. We call an element of $\iota ^{t}_{\mathfrak {F}}$ for a complex type t an intension, and the relation it maps a world to its extension at that world. Note that the definition of frames allows for W and I to be empty. Intensions of type 〈〉 – the type of propositions – are functions from worlds to 0-ary relations. There are two 0-ary relations, ∅ and {〈〉}; if we take the first to correspond to falsity and the second to correspond to truth, we can think of such intensions as corresponding to functions from worlds to truth-values, and so as usual as corresponding to sets of worlds.

In the second step of defining the models of our semantics, we define structures by enriching a frame with a domain assignment, which tells us for every type and world which intensions of this type are in the domain of this world:

Definition 4

A domain assignment for a frame $\mathfrak {F}=\langle W,I\rangle$ is a function D mapping each type t to a function mapping each w∈W to a subset of $\iota _{\mathfrak {F}}^{t}$; i.e., $D(t)(w)\subseteq \iota _{\mathfrak {F}}^{t}$. For any set of types U and V ⊆ W, we write ${D^{U}_{V}}$ for $\bigcup _{t\in U}\bigcup _{w\in V}D(t)(w)$; in the case of singletons, we omit set-brackets, e.g., writing ${D^{t}_{w}}$ for $D^{\{t\}}_{\{w\}}$.

A structure is a tuple $\mathfrak {S}=\langle W,I,D\rangle$ such that 〈W, I〉 is a frame and D is a domain assignment for $\mathfrak {F}$.

We sometimes refer to the union of the domains of all worlds (of some specific types or one specific type) as the outer domain (of those types/this type).

As noted in Section 2.5, Williamson and Stalnaker both endorse the being constraint, the claim that necessarily everything could not have a property or stand in a relation without existing. (See Williamson [19, Section 4.1], Stalnaker [18, p. 139] and Stalnaker [17].) In the present setting, the natural type-theoretic generalization of this constraint corresponds to the following condition on domain functions: an intension of a complex type may only be in the domain of a world if at any world w, its extension relates only entities in the domains of w. As we will see later, the Fine-Stalnaker view of higher-order contingency is in conflict with this constraint. We therefore also consider a less restrictive class of structures, in which extensions are only required to be relations on the outer domains. Borrowing terminology from free logic, we call the first class of structures negative, and the second class of structures positive. Note that not all structures are positive. In particular, positive semantics rules out intensions whose extensions contain intensions which are not in the domain of any world. It would also be interesting to investigate the version of the model theory which allows all structures as defined above, but we don’t do so here.¹⁷ There are also interesting positions intermediate in strength between positive and negative semantics, and we briefly consider one such option in Section 6.4.

We capture the being constraint and its positive weakening by the notions of negative and positive support, which give rise to the notion of negative and positive structures. (Note that this terminology is unrelated to that of the support of a permutation, which will be introduced below.) To be able to talk about the two versions of the semantics in a succinct way, we use the two signs − and + as parameters, standing for negative and positive semantics, over which we quantify using × as a meta-language variable:

Definition 5

For any sign ×, frame $\mathfrak {F}=\langle W,I\rangle$, domain assignment D for $\mathfrak {F}$, type t and $o\in \iota _{\mathfrak {F}}^{t}$, we define D ×supporting o, written $D\boxtimes o$, as follows:

• If t = e, then $D\boxtimes o$ iff $o\in {D^{e}_{W}}$

• If $t=\bar {t}$, then

  $$\begin{array}{@{}rcl@{}} D\boxminus o\; \text{iff}\; o(w)\subseteq{\Pi}_{i\leq n}D^{t_{i}}_{w}\; \text{for all}\; w\in W\\ D\boxplus o\; \text{iff}\; o(w)\subseteq{\Pi}_{i\leq n}D^{t_{i}}_{W}\; \text{for all}\; w\in W \end{array} $$

Define 〈W, I, D〉 to be a ×structure if $D\boxtimes o$ for all $o\in {D^{T}_{W}}$.

Philosophically, distinct worlds represent different ways for things to be, so in any plausible structure, any distinct worlds differ in some way with respect to intensions in the domain assignment. Inspired by standard terminology in propositional modal logic (see, e.g., Blackburn et al. [1, p. 308]) and the related but importantly different notion in Fine [5, p. 148], we call such structures differentiated:

Definition 6

A structure 〈W, I, D〉 is differentiated if for all distinct w, v∈W, ${D^{T}_{w}}\neq {D^{T}_{v}}$ or there is a type t≠e and $o\in {D^{T}_{W}}$ such that o(w)≠o(v).

In the following, we will mostly restrict ourselves to differentiated structures. For the constant domain case, Gallin [10] contains a very thorough discussion of non-differentiated structures, showing that for model-theoretic purposes, non-differentiated structures can safely be ignored. Since it is clear that analogous considerations apply to the present case, we omit such a discussion here. We will briefly return to issues connected to differentiation in Section 5.2.

We are now finally ready to define the notion of a model in our semantics. One aspect of our definition worth highlighting is that we follow Kripke [14] in singling out one world as the actual one, and that we additionally take all non-logical constants to be interpreted as expressing entities in the domain of the actual world. As noted in footnote 14, negative semantics and propositional contingentism are inconsistent with there being a property of propositions intensionally equivalent to negation, so the restriction to non-logical constants is essential.

Definition 7

For any signature σ, a model for σ is a tuple $\mathfrak {M}=\langle W,I,D,V,w\rangle$ such that 〈W, I, D〉 is a differentiated structure, w∈W, and V is a function on $\bigcup _{t\in T}\sigma (t)$ mapping every element of σ(t) to an element of ${D^{t}_{w}}$. We say that such a model is is based on 〈W, I, D〉. For any sign ×, a ×model for σ is a model for σ based on a ×structure.

When it is clear from context, we omit the specification of a signature and simply speak of a model.

3.3 Truth

To define truth of a formula relative to a model, we have to interpret the variables. We do so using an assignment function, a function which maps variables to entities of the corresponding type. In the present setting, it is best to let this function be partial; on the one hand, this allows us to use a function in the sense of a set of tuples, rather than a proper class, and on the other hand, it allows us to have assignments for structures with empty sets of individuals. We can then give the usual recursive truth-conditions for formulas relative to a model, a world and an assignment. As a relation symbol may take a complex formula as an argument, it is best to recursively define the intension expressed by an expression relative to a model and assignment function, from which we can straightforwardly derive a definition of truth. Since assignments are partial, we have to require the domain of the assignment function to contain the free variables of the expression we are evaluating, in which case we call it admissible for the formula. To give this definition, we adopt the convention of writing, for any – possibly partial – function f from a set A to a set B, dom(f) for the domain of f, the set {x∈A:f(x) = y for some y∈B}.

Definition 8

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure. An assignment for $\mathfrak {S}$ is a partial function mapping variables of type t to elements of ${D^{t}_{w}}$. An assignment a is admissible for an expression ε if its domain includes all free variables in ε; it is admissible for a class of expression if it is admissible for all members of the class.

We are now ready to define the interpretation relation. This will be done relative to a sign and a signature, but to minimise notational clutter, we fix a sign × and a signature σ for the rest of this section and leave the relativisation implicit. The relativisation to a sign is important as identity is to be ‘existence entailing’ (in the sense made precise in the clause for identity in the following definition) in the negative but not the positive semantics.

Definition 9

We define a function [[⋅]] mapping each expression ε of type t of $\mathcal {L}(\sigma )$, model $\mathfrak {M}=\langle W,I,D,V,w\rangle$, and assignment a for $\mathfrak {S}=\langle W,I,D\rangle$ admissible for ε to an element $[{}[\varepsilon ]{}]_{\mathfrak {M},a}$ of $\iota ^{t}_{\langle W,I\rangle }$ such that for all u∈W:

${[{}[v]{}]}_{\mathfrak {M},a}=$ :

a(v) (v being a variable)

${[{}[c]{}]}_{\mathfrak {M},a}=$ :

V(c) (c being a non-logical constant in σ)

${[{}[\varepsilon =\eta ]{}]}_{\mathfrak {M},a}(u)=$ :

$\left \{\begin {array}{ll} \{\langle \rangle :[{}[\varepsilon ]{}]_{\mathfrak {M},a}=[{}[\eta ]{}]_{\mathfrak {M},a} \text { and } [{}[\varepsilon ]{}]_{\mathfrak {M},a}\in {D^{e}_{u}}\} & \quad \text {if } \times =-\\ \{\langle \rangle :[{}[\varepsilon ]{}]_{\mathfrak {M},a}=[{}[\eta ]{}]_{\mathfrak {M},a}\} & \quad \text {if } \times =+ \end {array}\right .$

${[{}[\varepsilon \bar {\eta }]{}]}_{\mathfrak {M},a}(u)=$ :

$\{\langle \rangle :\langle [{}[\eta _{i}]{}]_{\mathfrak {M},a}:i\leq n\rangle \in [{}[\varepsilon ]{}]_{\mathfrak {M},a}(u)\}$

${[{}[\neg \varphi ]{}]}_{\mathfrak {M},a}(u)=$ :

$\{\langle \rangle \}\backslash [{}[\varphi ]{}]_{\mathfrak {M},a}(u)$

${[{}[\bigwedge {\Phi }]{}]}_{\mathfrak {M},a}(u)=$ :

$\bigcap _{\varphi \in {\Phi }}[{}[\varphi ]{}]_{\mathfrak {M},a}(u)$

${[{}[\Box \varphi ]{}]}_{\mathfrak {M},a}(u)=$ :

$\bigcap _{u^{\prime }\in W}[{}[\varphi ]{}]_{\mathfrak {M},a}(u^{\prime })$

${[{}[\forall {\Lambda }\varphi ]{}]}_{\mathfrak {M},a}(u)=$ :

$\bigcap _{b\text { in }X}[{}[\varphi ]{}]_{\mathfrak {M},b}(u)$, where X is the class of assignments for $\mathfrak {S}$ such that

$$\begin{array}{@{}rcl@{}} b(x)&=&a(x)\; \text{for all}\; x\in\text{dom}(a)\backslash{\Lambda},\; \text{and}\\ b(x)&\in& {D^{T}_{u}}\; \text{for all}\; x\in{\Lambda} \end{array} $$

We derive the definition of a formula φ or class of formulas Φ being true relative to $\mathfrak {M}$, u∈W and an assignment a for 〈W, I〉 admissible for φ/ Φ as follows:

$$\begin{array}{@{}rcl@{}} \mathfrak{M},u,a&\vDash&\varphi\; \text{iff} \;\langle\rangle\in[{}[\varphi]{}]_{\mathfrak{M},a}(u).\\ \mathfrak{M},u,a&\vDash&{\Phi}\; \text{iff} \;\mathfrak{M},u,a\vDash\varphi\; \text{for all}\; \varphi \;\text{in}\; {\Phi}. \end{array} $$

Finally, we derive truth in a model for a sentence φ or class of sentences Φ as truth in the distinguished actual world of the model:

$$\begin{array}{@{}rcl@{}} \mathfrak{M}&\vDash&\varphi\; \text{iff} \;\mathfrak{M},w,\emptyset\vDash\varphi.\\ \mathfrak{M}&\vDash&{\Phi}\; \text{iff} \;\mathfrak{M}\vDash\varphi\; \text{for all}\; \varphi\; \text{in} \;{\Phi}. \end{array} $$

From this definition of truth, we derive notions of consequence and validity in the standard way. As the interpretation function [[⋅]] is relative to a sign and a signature, so are truth, consequence and validity, but as above, this is left implicit.

Definition 10

Let C be a class of models. A sentence or class of sentences Γ being a consequence of a sentence or class of sentences π over C, written ${\Pi }\vDash _{C}{\Gamma }$, is defined as follows:

$${\Pi}\vDash_{C}{\Gamma}\; \text{iff} \;\mathfrak{M}\vDash{\Gamma}\; \text{for all models} \;\mathfrak{M}\; \text{in}\; C\; \text{such that} \;\mathfrak{M}\vDash{\Pi}. $$

We derive Γ being valid on C, written $\vDash _{C}{\Gamma }$, as $\emptyset \vDash _{C}{\Gamma }$. In the case where C is the class of all models, we simply omit C.

Note that this is a multiple conclusion consequence relation according to which the truth of the premises guarantees the truth of all conclusions, rather than some conclusion.

The notion of truth relative to a model allows us to define a notion of two models being equivalent in the sense of satisfying the same closed formulas:

Definition 11

Let $\mathfrak {M}$ and $\mathfrak {M^{\prime }}$ models. $\mathfrak {M}$ and $\mathfrak {M}^{\prime }$ are equivalent, written $\mathfrak {M}\equiv \mathfrak {M}^{\prime }$, if for all sentences φ of $\mathcal {L}$, $\mathfrak {M}\vDash \varphi$ if and only if $\mathfrak {M^{\prime }}\vDash \varphi$.

3.4 Interpreting the Higher-Order Quantifiers of $\mathcal {L}$

Models assign domains of intensions to worlds; how does this correspond to the contingent existence of relations?¹⁸ Consider intensions of type 〈〉, i.e., functions from worlds to sets of 0-tuples, which, as usual, we can identify with sets of worlds. One might propose to understand these intensions as corresponding to unique 0-ary relations, i.e., propositions, but it is hard to see how this would go unless necessarily equivalent propositions are identical. (Recall that we use talk of propositions, properties and relations in English to gesture at claims which could be said more precisely in a language with explicit higher-order quantifiers, such as $\mathcal {L}$.) We want to stay neutral on the question whether necessarily equivalent propositions are identical, so we won’t take an intension of type 〈〉 as corresponding to a single proposition. Instead, we understand such an intension as corresponding to all the propositions which are true in exactly those worlds which the intension maps to {〈〉}. And we understand such an intension being in the domain of a world as representing that there is a proposition at this world to which the intension corresponds.

In addition to allowing that there are distinct but necessarily equivalent propositions, we want to allow at the same time that propositions are identical just in case they have the same properties. So we also don’t want to commit to the claim that necessarily equivalent propositions have the same properties. But the following sentence is easily seen to be valid on the class of all models:

$$\forall p^{\langle\rangle}q^{\langle\rangle}(\Box(p\leftrightarrow q)\to\forall F^{\langle\langle\rangle\rangle}(Fp\leftrightarrow Fq)) $$

We must therefore interpret the higher-order quantifiers in $\mathcal {L}$ as somehow restricted. In this section, we will define a condition we call ‘hereditary intensionality’, and argue that possible world models can be used to interpret $\mathcal {L}$ if its quantifiers are understood as restricted to hereditarily intensional relations.

Given the notion of hereditary intensionality, which we will define shortly, we can explain in general which intensions correspond to which relations: An intension o of type t corresponds to all the hereditarily intensional relations R of type t such that at each world, R applies to a sequence of hereditarily intensional relations just in case o applies to the corresponding sequence of intensions. To define which relations are hereditarily intensional, we simultaneously define the notion of two relations being hereditarily intensionally equivalent: A relation is hereditarily intensional if it does not possibly distinguish between any two sequences of possible hereditarily intensional entities which are pairwise hereditarily intensionally equivalent; two relations are hereditarily intensionally equivalent if they necessarily apply to the same sequences of possible hereditarily intensional entities. To ensure that these definitions are well-founded, we define all possible individuals to be hereditarily intensional, and individuals to be hereditarily intensionally equivalent just in case they are identical.

To make these informal definitions more perspicuous, we introduce a second language $\mathcal {U}$, whose quantifiers are interpreted unrestrictedly. To keep the quantifiers of $\mathcal {L}$ and $\mathcal {U}$ apart, we write the quantifier of $\mathcal {U}$ as $\forall ^{\mathcal {U}}$; otherwise, the languages are exactly the same. In $\mathcal {U}$, we can formally define hereditary intensionality and hereditary intensional equivalence as follows:

$$\begin{array}{@{}rcl@{}} \text{\textsc{hi}}(\varepsilon^{e})&:=& \top\\ \varepsilon^{e}{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]\sim\end{array}}}\eta^{e}&:=&\varepsilon=\eta\\ \text{\textsc{hi}}\left( \varepsilon^{\bar{t}}\right)&:=&\Box\forall^{\mathcal{U}}\! x_{1}^{t_{1}}\ldots\Box\forall^{\mathcal{U}}\! x_{n}^{t_{n}}\Box\forall^{\mathcal{U}}\! y_{1}^{t_{1}}\ldots\Box\forall^{\mathcal{U}} y_{n}^{t_{n}}\\ &&\Box\left( {\bigwedge}_{i\leq n}(\text{\textsc{hi}}(x_{i})\wedge\text{\textsc{hi}}(y_{i})\wedge x_{i}{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]\sim\end{array}}} y_{i})\to(\varepsilon\bar{x}\leftrightarrow\varepsilon\bar{y})\right)\\ \varepsilon^{\bar{t}}{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]\sim\end{array}}}\eta^{\bar{t}}&:=&\Box\forall^{\mathcal{U}}\! x_{1}^{t_{1}}\ldots\Box\forall^{\mathcal{U}}\! x_{n}^{t_{n}}\Box\left( {\bigwedge}_{i\leq n}\text{\textsc{hi}}(x_{i})\to(\varepsilon\bar{x}\leftrightarrow\eta\bar{x})\right) \end{array} $$

With this definition, we can specify a recursive translation ⋅^∗ from $\mathcal {L}$ to $\mathcal {U}$ which tells us exactly how to understand sentences formulated using the restricted quantifier ∀ of $\mathcal {L}$ using the unrestricted quantifier $\forall ^{\mathcal {U}}$ of ${\mathcal {U}}$. All recursion clauses of this definition are trivial, apart from the clause for ∀, which simply replaces ∀ by $\forall ^{\mathcal {U}}$ restricted to hi:

$$(\forall V\varphi)^{*}:=\forall^{\mathcal{U}}\! V\left( {\bigwedge}_{v\in V}\text{\textsc{hi}}(v)\to\varphi^{*}\right) $$

It may be worth illustrating the definition of hereditary intensionality using some specific cases. Consider a property of individuals F ^〈e〉. F is hereditarily intensional just in case for all possible individuals x ^e and y ^e which are hereditarily intensionally equivalent, necessarily F x if and only if F y. x and y are hereditarily intensionally equivalent just in case they are identical, so F is trivially hereditarily intensional. This reasoning generalizes to any relation among individuals, including propositions, so necessarily all such relations are trivially hereditarily intensional.

Consider now a property of properties of individuals Ξ^{〈〈e〉〉}. Ξ is hereditarily intensional just in case for all possible properties of individuals F ^e and G ^e which are hereditarily intensionally equivalent, necessarily ΞF if and only if ΞG. F and G are hereditarily intensionally equivalent just in case necessarily, they apply to the same possible individuals, so it is clearly not trivial for Ξ to be hereditarily intensional. If there are distinct properties F and G which necessarily apply to the same possible individuals, then there is the property of being identical to F, and so a property of properties of individuals which is not hereditarily intensional.

In the following, we will normally leave the restriction to hereditarily intensional relations implicit in the informal discussion. As we have just seen, this implicit restriction is only non-vacuous for types beyond the types of relations among individuals. Finally, it will be useful to be able to state in $\mathcal {L}$, rather than $\mathcal {U}$, that two relations are hereditarily intensionally equivalent. Since the definition of ${{\begin {array}{c}\text {\textsc {hi}}\\[-4pt]\sim \end {array}}}$in $\mathcal {U}$ involved only quantifiers restricted to hi, this is straightforward:

$$\begin{array}{@{}rcl@{}} \varepsilon^{e}{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]\sim\end{array}}}\eta^{e}&:=&\varepsilon=\eta\\ \varepsilon^{\bar{t}}{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]\sim\end{array}}}\eta^{\bar{t}}&:=&\Box\forall x_{1}^{t_{1}}\ldots\Box\forall x_{n}^{t_{n}}\Box(\varepsilon\bar{x}\leftrightarrow\eta\bar{x}) \end{array} $$

4 Generation and Closure

With a general framework of variable domain type theory in place, we can start to formalize the different versions of the Fine-Stalnaker view introduced in Section 2.2. We first formalize the intuitive idea of permutations of modal space, and then use this to formalize both the qualitative generation and higher-order closure views.

4.1 Automorphisms

In the possible-worlds model theory defined in the previous section, a permutation of modal space is naturally understood to determine a permutation of the possible worlds and the outer domains of that structure. (Mathematically, a permutation of a set is a bijection from this set to itself.) Clearly, we want the permutation to respect types: an entity of a given type should only be mapped to one of the same type. Permutations should also preserve facts about what applies to what: if an intension applies to a sequence of entities in a world, then its image (under the permutation) should apply to the image of the sequence in the image of the world, and vice versa. It turns out that for any permutation of worlds and permutation of the outer domain of individuals, there is only one way of permuting the elements of the outer domains of higher types that satisfies this constraint. It is therefore most convenient to take such pairs to represent permutations of modal space. Extending terminology from algebra, we call them automorphisms.

Definition 12

An automorphism of a frame $\mathfrak {F}=\langle W,I\rangle$ is a tuple 〈f, g〉 such that f is a permutation of W and g is a permutation of I. Let $\text {aut}(\mathfrak {F})$ be the set of automorphisms of $\mathfrak {F}$.

Writing ∘ for the composition of functions, ⋅⁻¹ for taking the inverse of an injection, and id _X for the identity function on a given domain X, we extend these notions in the straightforward way to automorphisms:

$$\begin{array}{@{}rcl@{}} &&\langle f,g\rangle\circ\langle f^{\prime},g^{\prime}\rangle=\langle f\circ f^{\prime},g\circ g^{\prime}\rangle\\ &&\langle f,g\rangle^{-1}=\langle f^{-1},g^{-1}\rangle\\ &&\text{id}=\langle\text{id}_{W},\text{id}_{I}\rangle \end{array} $$

In the following, we usually omit ∘, writing f f ^′ for f∘f ^′.

We will now note that $\text {aut}(\mathfrak {F})$ always forms a group with ∘. The definition of a group and an exposition of the basic group-theoretic tools we will use in the following can be found in standard references such as Rotman [16] and Dixon and Mortimer [3]. We adopt the convention of writing S _X for the symmetric group on X, i.e., the set of permutations of X with the operation of function composition.

Proposition 1

For any frame $\mathfrak {F}$ , $\text {aut}(\mathfrak {F})$ forms a group under ∘.

Proof

Let $\mathfrak {F}=\langle W,I\rangle$. The claim is immediate from the fact that S _W and S _I are groups. □

To extend the automorphisms of a frame to functions on intensions via the constraint motivated above, we make use of actions. An action α of a group G on a set X is a homomorphism from G to S _X ; i.e., a function mapping each element of G to a permutation of X such that for all g, f∈G, α(g f) = α(g)α(f). If it is clear from context that we are concerned with a specific action α of G on X, we simply say that G acts on X, and write g.x for α(g)(x). In our present application, we introduce an action for every type that maps every automorphism of a frame to a permutation of the intensions of the relevant type based on the frame. In the service of uniform notation, we do the same for worlds and individuals.

Definition 13

Let $\mathfrak {F}=\langle W,I\rangle$ be a frame. We define a function $\alpha ^{W}_{\mathfrak {F}}:\text {aut}(\mathfrak {F})\to W^{W}$ and a function $\alpha ^{t}_{\mathfrak {F}}:\text {aut}(\mathfrak {F})\to {\left (\iota ^{t}_{\mathfrak {F}}\right )}^{\iota ^{t}_{\mathfrak {F}}}$ for every type t such that for all $\xi =\langle f,g\rangle \in \text {aut}(\mathfrak {F})$:

$$\begin{array}{@{}rcl@{}} \alpha^{W}_{\mathfrak{F}}(\langle f,g\rangle)(w)&=&f(w)\\ \alpha^{e}_{\mathfrak{F}}(\langle f,g\rangle)(o)&=&g(o)\\ \alpha^{\bar{t}}_{\mathfrak{F}}(\xi)(o)(\alpha^{W}_{\mathfrak{F}}(\xi)(w))&=&\left\{\left\langle\alpha^{t_{i}}_{\mathfrak{F}}(\xi)(o_{i}):i\leq n\right\rangle:\bar{o}\in o(w)\right\} \end{array} $$

By a straightforward induction on the complexity of types, it can be verified that $\alpha ^{t}_{\mathfrak {F}}$ is well-defined.

Proposition 2

For any frame $\mathfrak {F}=\langle W,I\rangle$ , $\alpha ^{W}_{\mathfrak {F}}$ and $\alpha ^{t}_{\mathfrak {F}}$ , for some type t, are actions of $\text {aut}(\mathfrak {F})$ on W and $\iota ^{t}_{\mathfrak {F}}$ , respectively.

Proof

Routine. □

In keeping with our notation for actions, we write ξ.w for $\alpha ^{W}_{\mathfrak {F}}(\xi )(w)$, and similarly for $\alpha ^{e}_{\mathfrak {F}}$ and $\alpha ^{t}_{\mathfrak {F}}$, relying on the context to supply the omitted parameters. In the following, we will often need to extend a function on a set X to apply to subsets of X or sequences of elements of X. To keep notation simple, we do so implicitly in the obvious way. I.e., for any Y ⊆ dom(f), f(Y) = {f(x):x∈Y}, and for any 〈x ₁,…, x _n 〉∈dom(f)ⁿ, f(〈x ₁,…, x _n 〉)=〈f(x ₁),…, f(x _n )〉. (If X contains sets or tuples of some of its elements, this notation introduces ambiguity; in the following, the intended meaning will always be clear from context.) We adopt exactly the same convention for actions. With this, we can write the last condition of Definition 13 more concisely as follows: (ξ.o)(ξ.w) = ξ.(o(w)).

We can now define an automorphism of a structure to be an automorphism of the underlying frame which respects the domain assignment of the structure; i.e., for every type, we require the elements in the domain at any world to be mapped to the elements in the domain at the world to which the original world is mapped. We can prove that these form a subgroup of the automorphisms of the frame.

Definition 14

An automorphism ξ of a structure $\mathfrak {S}=\langle W,I,D\rangle$ is an automorphism of 〈W, I〉 such that for all types t and w∈W, $\xi .{D^{t}_{w}}=D^{t}_{\xi .w}$. Let $\text {aut}(\mathfrak {S})$ be the set of automorphisms of $\mathfrak {S}$.

Proposition 3

For any structure $\mathfrak {S}=\langle W,I,D\rangle$ , $\text {aut}(\mathfrak {S})$ is a subgroup of aut(〈W,I〉).

Proof

It suffices to prove that $\xi \zeta ^{-1}\in \text {aut}(\mathfrak {S})$ for all $\xi ,\zeta \in \text {aut}(\mathfrak {S})$. Consider any type t and w∈W. Since $\zeta \in \text {aut}(\mathfrak {S})$, $\zeta .D^{t}_{\zeta ^{-1}.w}=D^{t}_{\zeta \zeta ^{-1}.w}$, so $D^{t}_{\zeta ^{-1}.w}=\zeta ^{-1}.{D^{t}_{w}}$. Further $\xi .D^{t}_{\zeta ^{-1}.w}=D^{t}_{\xi \zeta ^{-1}.w}$, so $\xi \zeta ^{-1}.{D^{t}_{w}}=D^{t}_{\xi \zeta ^{-1}.w}$. Hence $\xi \zeta ^{-1}\in \text {aut}(\mathfrak {S})$. □

4.2 Generation and Closure of Structures

To capture the idea of qualitative generation, we need a way of generating a structure from a choice of individuals and relations. To keep the construction as flexible as possible, we don’t limit this choice to relations among individuals, and allow it to vary between worlds. We can thus use a structure to specify the materials from which we generate, with the domain assignment of higher orders containing the intensions corresponding to the relations from which we generate.

So, given a structure, one might suggest generating another structure by letting the domain function of the latter contain an intension at a given world if and only if it is mapped to itself by all automorphisms of the original structure which map the world and all elements of its domains to themselves. However, structures generated in this way need not satisfy the being constraint or its positive weakening. In fact, they will only do so under very special circumstances, as for all types, the trivial intension which applies to all tuples of intensions of the relevant type at all worlds is mapped to itself by all automorphisms, but will in many cases not satisfy the relevant constraint. Therefore, we have to distinguish between negative and positive generation, and in each case require an intension to be negatively or positively supported by the domain function to be included in the domain function of the generated structure.

Note that we do not require the generating structure to be negative or positive. This is not merely for technical generality, but also philosophically motivated. E.g., the generating relations might include a modality of nomological necessity, which in the present type hierarchy would be represented by an intension μ of type 〈〈〉〉. Presumably, the extension of μ at any world would include the propositional intension true in all worlds. Yet the propositional intension true in all worlds might well not be in the domain of any world in the relevant generating structure, and so this structure might be neither positive nor negative.

For the formal definition of qualitative generation, note that for a group G acting on a set X and x∈X, we write G _x for the set of elements of G which map x to itself; this is called the stabilizer of x, and can be shown to form a subgroup of G.

Definition 15

Let $\mathfrak {S}=\langle W,I,B\rangle$ be a structure. For any w∈W, define

$$\text{fix}(\mathfrak{S},w)=\text{aut}(\mathfrak{S})_{w}\cap{\bigcap}_{o\in {B^{T}_{w}}}\text{aut}(\mathfrak{S})_{o}. $$

For any sign ×, define the structure ×generated by $\mathfrak {S}$, written $\otimes \mathfrak {S}$, to be the structure 〈W, I, D〉 such that for all w∈W, ${D^{e}_{w}}={B^{e}_{w}}$ and for all types t≠e and $o\in \iota _{\langle W,I\rangle }^{t}$:

$$o\in {D^{t}_{w}}\; \text{iff}\; D\boxtimes o\; \text{and} \;\xi.o=o\; \text{for all}\; \xi\in\text{fix}(\mathfrak{S},w) $$

A few observations regarding this definition are straightforward, but helpful to note: First, since subgroups are closed under intersection, $\text {fix}(\mathfrak {S},w)$ is a subgroup of $\text {aut}(\mathfrak {S})$. Second, the condition defining the domains of complex type can also be stated as follows:

$$o\in {D^{t}_{w}}\; \text{iff}\; D\boxtimes o\; \text{and} \;\text{fix}(\mathfrak{S},w)\subseteq\text{aut}(\mathfrak{S})_{o} $$

Finally, we register that the addition of the support requirement has the desired effect and that generated structures are differentiated:

Proposition 4

For every sign × and structure $\mathfrak {S}$ , $\otimes \mathfrak {S}$ is a differentiated ×structure.

Proof

That $\otimes \mathfrak {S}$ is a ×structure is immediate by construction; that it is differentiated follows from the fact that every world w contains its world-proposition (the propositional intension which is only true at w). □

While this formalization of the qualitative generation view allows us to generate one structure from another, the formalization of the higher-order closure view should impose a constraint on structures. With the tools established so far, it is straightforward to state this constraint – we want to require the domain function for any type to map each world to the set of intensions of the relevant type which are supported by the domain function and mapped to themselves by all automorphisms of the structure which map all entities in the domains of the given world to themselves. As with generation, being closed must be relativized to a sign, as the notion of support is relative to a sign:

Definition 16

For any structure $\mathfrak {S}=\langle W,I,D\rangle$ and sign ×, $\mathfrak {S}$ is ×closed if for all w∈W, types t≠e and $o\in \iota _{\langle W,I\rangle }^{t}$:

$$o\in {D^{t}_{w}}\; \text{iff} \;D\boxtimes o\; \text{and} \;\xi.o=o\; \text{for all} \;\xi\in\text{fix}(\mathfrak{S},w) $$

The definitions of generation and closure are evidently closely related:

Proposition 5

Let × be a sign. A structure $\mathfrak {S}$ is × closed just in case $\mathfrak {S}=\otimes \mathfrak {S}$.

Proof

Immediate by the definitions of closure and generation. □

The definitions of generation and closure constrain only higher-order domains. One might consider a view on which the existence of individuals obeys a similar constraint: if an individual can be singled out from a certain world, it must exist in it. It would be straightforward to adapt the formal definitions of generation and closure to formalize such a strengthened version of the generation and closure thoughts. In the following, we don’t consider these variants.

4.3 A Structure is Closed if and Only if it is Generated

Proposition 5 tells us that a structure being closed is for it to be generated by itself, and therefore that all closed structures are generated by some structure. The converse of this implication is harder to see, but we show in this section that it also holds: any generated structure is closed. To carry out this proof, we first establish a number of lemmas.

Lemma 1

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure and $\xi \in \text {aut}(\mathfrak {S})$.

• (i) For all $o\in \iota ^{T}_{\langle W,I\rangle }$ , $\xi .\text {aut}(\mathfrak {S})_{o}=\text {aut}(\mathfrak {S})_{\xi .o}$.

• (ii) For all w∈W, $\xi .\text {fix}(\mathfrak {S},w)=\text {fix}(\mathfrak {S},\xi .w)$.

Proof

(i) follows from a general principle about stabilizers. So does the fact that $\xi .\text {aut}(\mathfrak {S})_{w}=\text {aut}(\mathfrak {S})_{\xi .w}$, for any w∈W, given which (ii) follows from (i). □

Lemma 2

Let × be a sign, $\mathfrak {S}=\langle W,I,B\rangle$ a structure and $\otimes \mathfrak {S}=\langle W,I,D\rangle$ . For all types t,

• (i) For all $\xi \in \text {aut}(\mathfrak {S})$ and $o\in \iota ^{T}_{\langle W,I\rangle }$ , $D\boxtimes o$ iff $D\boxtimes \xi .o$.

• (ii) For all $\xi \in \text {aut}(\mathfrak {S})$ and w∈W, $\xi .{D^{t}_{w}}=D^{t}_{\xi .w}$.

Proof

By induction on types. The base case is trivial, so consider a complex type $\bar {t}$. (i): For any $\xi \in \text {aut}(\mathfrak {S})$ and $o\in \iota ^{\bar {t}}_{\langle W,I\rangle }$, it is routine to show using induction hypothesis (ii) that $D\boxtimes o$ entails $D\boxtimes \xi .o$. The converse direction follows using ξ ⁻¹. (ii): For any $\xi \in \text {aut}(\mathfrak {S})$ and w∈W, $o\in \xi .D^{\bar {t}}_{w}$ iff $\xi ^{-1}o\in D^{\bar {t}}_{w}$, which is the case iff $D\boxtimes \xi ^{-1}.o$ and $\text {fix}(\mathfrak {S},w)\subseteq \text {aut}(\mathfrak {S})_{\xi ^{-1}.o}$. By induction hypothesis (i), the former is the case iff $D\boxtimes o$. By Lemma 1, the latter is the case iff $\text {fix}(\mathfrak {S},\xi .w)\subseteq \text {aut}(\mathfrak {S})_{o}$. Thus $o\in \xi .D^{\bar {t}}_{w}$ iff $o\in D^{\bar {t}}_{\xi .w}$. □

Lemma 3

Let × be a sign and $\mathfrak {S}=\langle W,I,B\rangle$ a structure.

• (i) $\text {aut}(\mathfrak {S})\subseteq \text {aut}(\otimes \mathfrak {S})$.

• (ii) For all w∈W: $\text {fix}(\mathfrak {S},w)\subseteq \text {fix}(\otimes \mathfrak {S},w)$.

Proof

(i) follows from Lemma 2 (ii). For (ii), let $\otimes \mathfrak {S}=\langle W,I,D\rangle$, and consider any w∈W and $\xi \in \text {fix}(\mathfrak {S},w)$. Then ξ.w = w, and by (i), $\xi \in \text {aut}(\otimes \mathfrak {S})$. For any $o\in {D^{T}_{W}}$, $\text {fix}(\mathfrak {S},w)\subseteq \text {aut}(\mathfrak {S})_{o}$, so ξ.o = o. Hence $\xi \in \text {fix}(\otimes \mathfrak {S},w)$. □

Proposition 6

For any sign ×, any structure is ×closed if and only if it is ×generated by some structure.

Proof

By Proposition 5, any ×closed structure is ×generated by some structure. So consider any structure $\otimes \mathfrak {S}=\langle W,I,D\rangle \times$ generated by a structure $\mathfrak {S}=\langle W,I,B\rangle$. To prove that $\otimes \mathfrak {S}$ is closed, we show for any w∈W, type t≠e and $o\in \iota _{\langle W,I\rangle }^{t}$ that $o\in {D^{T}_{W}}$ iff $D\boxtimes o$ and ξ.o = o for all ξ∈fix(⊗S, w). Since $\otimes \mathfrak {S}$ is a ×structure, $o\in {D^{T}_{W}}$ entails that $D\boxtimes o$, hence the left-to-right direction is immediate. So assume that $D\boxtimes o$ and ξ.o = o for all $\xi \in \text {fix}(\otimes \mathfrak {S},w)$. We can prove that $o\in {D^{T}_{W}}$ by showing that ξ.o = o for all $\xi \in \text {fix}(\mathfrak {S},w)$. This follows from Lemma 3 (ii). □

In the present formalization, the ideas of qualitative generation and higher-order closure thus coincide in the sense of determining the same class of structures.

A natural relation among structures on a given frame orders them according to containment of higher-order domains; this is easily seen to be a partial order. Proposition 6 establishes that the generation operator ⊗ on structures is idempotent (${\otimes }{\otimes }\mathfrak {S}=\otimes \mathfrak {S}$). One might conjecture that with respect to the order mentioned, it is also extensive (writing $\sqsubseteq$ for the order: if $\mathfrak {S}\sqsubseteq \mathfrak {S}^{\prime }$ then $\otimes \mathfrak {S}\sqsubseteq \otimes \mathfrak {S}^{\prime }$) and increasing ($\mathfrak {S}\sqsubseteq \otimes \mathfrak {S}$), and thus a closure operator on the class of structures ordered by it. However, ⊗ has neither of these further properties, as can be shown using relatively simple finite structures.

4.4 Closed and Finely Generated Models

We call a model closed or generated just in case it is based on a closed or generated structure.

Definition 17

For any sign ×, a model is ×c l o s e d just in case it is based on a ×closed structure. C× is the class of ×closed models.

Fine [5] essentially works with + closed models, apart for two differences. The first difference is that Fine includes extensional types in his type hierarchy; we won’t consider such types in the following. We can understand the second difference as consisting of three restrictions on the choice of relations from which higher-order domains are generated. First, he requires this choice to be constant across worlds. Second, he requires it to contain only relations among individuals. Third, he requires for any two distinct worlds with the same individuals that there be a generating relation which allows us to distinguish between these two worlds using only individuals which exist at those worlds. (It is this last existence condition which makes this a stronger restriction than being differentiated.) We can easily capture these restrictions in the present setting:

Definition 18

Let a structure $\mathfrak {S}=\langle W,I,D\rangle$ be Finely generated if there is a structure $\mathfrak {S}^{\prime }=\langle W,I,B\rangle$ such that $\mathfrak {S}=\oplus \mathfrak {S}^{\prime }$ and:

• (i) For all types t and such that t∉{e, e ⁿ:n<ω}, ${B^{t}_{W}}=\emptyset$.

• (ii) For all types t≠e and w, v∈W, ${B^{t}_{w}}={B^{t}_{v}}$.

• (iii) For all distinct w, v∈W such that ${B^{e}_{w}}={B^{e}_{v}}$, there is an $F\in B^{\bar {e}}_{W}$ and $\bar {o}\in {B^{e}_{w}}$ such that not $\bar {o}\in F(w)$ iff $\bar {o}\in F(v)$.

A model is Finely generated if it is based on a Finely generated structure.

Before turning to comprehension principles, we note that not every + closed structure is Finely generated. In fact, each of conditions (i) and (ii) alone restricts the class of structures that can be generated: in both cases, there are closed structures which are not generated by any structure satisfying the constraint. Since there are in particular finite such structures, and we can characterize every finite structure relative to the class of closed models up to isomorphism using a single sentence, this means that the classes of closed models satisfying one of these additional constraints validate sentences which are invalid on the class of all closed models. In contrast, it is easy to see that (iii) imposes no restriction on the class of generated structures, since every generating structure can be turned into one that satisfies (iii) and generates the same structure as the initial one, by adding to each world its world-proposition.

We only sketch proofs of the facts that (i) and (ii) restrict the class of generated structures. The proof for (i) is based on the fact that there are patterns of indistinguishability which cannot be reduced to the pairwise indistinguishability of worlds, which is discussed in more detail in Fritz [7]. We can use this observation for the present application by considering structures in which there necessarily exists one and the same individual. For (ii), consider a structure in which there are two worlds with the same individuals, a third world with no individuals which is able to distinguish them, and a fourth world which is unable to distinguish them. Such a structure can only be generated by a structure which does not have constant higher-order domains.

5 Comprehension

5.1 Williamson on Comprehension Principles

Williamson [19, Chapter 6] argues that a good higher-order contingentist theory has to entail adequate comprehension principles. On the one hand, these comprehension principles must be sufficiently strong. E.g., on the abundant conception of higher-order entities we are concerned with here, they should allow us to demonstrate that these entities are closed under complementation and intersection. On the other hand, the comprehension principles it satisfies must not be too strong – e.g., it must not entail higher-order necessitism.

More systematically, Williamson argues that a good higher-order contingentist theory should entail two restricted comprehension principles he calls Comp⁻ and Comp _C , while it should not entail the unrestricted comprehension principle he calls Comp, from which higher-order necessitism is easily derivable. We show that on the formalizations of the Fine-Stalnaker view presented above, the view stands up well to these constraints – they validate the first two principles and invalidate the third.

Since Williamson thinks that contingentists should accept the being constraint, his formulations of these principles are stated in a way that fits negative semantics. Here, we consider both negative and positive semantics, and consequently distinguish between negative variants −Comp _C and −Comp, and positive variants +Comp _C and +Comp. We can use the same version of Comp⁻ in both cases. As usual, these comprehension principles are schematic, and can be instantiated using an arbitrary formula; consequently, they are relative to the choice of a signature. To simplify the discussion in this section, we fix an arbitrary signature σ.

To state the comprehension principles, we first introduce a formula $E_{\varphi }^{\bar {v}}$ for any formula φ and sequence of variables $\bar {v}$ which expresses that the values of all constants in φ and free variables not among $\bar {v}$ in φ exist; to do so, we simply let it be the conjunction of $\exists v(v{{\begin {array}{c}\text {\textsc {hi}}\\[-4pt]\sim \end {array}}}\varepsilon )$for all ε which are a constant in φ or a free variable not among $\bar {v}$ in φ, where v is a variable of the same type as ε. We can now define the comprehension principles as follows:

$$\begin{array}{@{}rcl@{}} \text{Comp}^{-}&:&\exists V\forall\bar{v}(V\bar{v}\leftrightarrow\varphi)\\ -\text{Comp}_{C}&:&E^{\bar{v}}_{\varphi}\to\exists V\Box\forall\bar{v}(V\bar{v}\leftrightarrow\varphi)\\ +\text{Comp}_{C}&:&E^{\bar{v}}_{\varphi}\to\exists V\Box\forall v_{1}\ldots\Box\forall v_{n}\Box(V\bar{v}\leftrightarrow\varphi)\\ -\text{Comp}&:&\exists V\Box\forall\bar{v}(V\bar{v}\leftrightarrow\varphi)\\ +\text{Comp}&:&\exists V\Box\forall v_{1}\ldots\Box\forall v_{n}\Box(V\bar{v}\leftrightarrow\varphi) \end{array} $$

An instance of one of these comprehension schemas is obtained by letting φ be any formula not containing free occurrences of V, letting V be a variable of some type 〈t ₁,…, t _n 〉, and v ₁,…, v _n be variables of types t ₁,…, t _n , and prefixing the formula with any string of universal quantifiers and □ operators which renders the resulting formula closed. For the purposes of validity and consequence, we identify a schema with the class of its instances.

Before we show that both Comp⁻ and Comp _C are valid on closed models, it should be noted that Williamson’s discussion of these comprehension principles is couched in terms of unrestricted quantifiers. But since he assumes that all relations are hereditarily intensional (Williamson [19, p. 266]), this is dialectically unproblematic.

To prove the validity of the two comprehension principles on closed models, we introduce a way of specifying variants of assignments:

Definition 19

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure and a an assignment for $\mathfrak {S}$. For any variable v of type t and $o\in {D^{T}_{W}}$, we let a[o/v] be the assignment such that dom(a[o/v])=dom(a)∪{v}, a[o/v](v) = o, and a[o/v](x) = a(x) for all x∈dom(a)∖{v}. We extend this notation to finite sequences by defining $a[\bar {o}/\bar {v}]=a[o_{1}/v_{1}]\ldots [o_{n}/v_{n}]$.

Proposition 7

For each sign ×, $\vDash _{C\times }\text {Comp}^{-}$.

Proof

Consider any φ, V and $\bar {v}$ with which an instance of Comp⁻ can be obtained, ×closed model $\mathfrak {M}=\langle W,I,D,V,w\rangle$, v∈W and assignment a admissible for φ. Define o such that o(u) = ∅ for all u≠v and $o(v)=\{\bar {r}\in {\Pi }_{i\leq n}D^{t_{i}}_{v}:\mathfrak {M},v,a[\bar {r}/\bar {v}]\vDash \varphi \}$. By construction, $\mathfrak {M},v,a[o/V]\vDash \forall \bar {v}(V\bar {v}\leftrightarrow \varphi )$. Note that $D\boxtimes o$. Let $\mathfrak {S}=\langle W,I,D\rangle$, and consider any $\xi \in \text {fix}(\mathfrak {S},v)$. Since ξ.o ^′ = o ^′ for all $o^{\prime }\in {D^{T}_{v}}$ and ξ.v = v, $\xi \in \text {fix}(\mathfrak {S},o)$. As $\mathfrak {S}$ is ×closed, it follows that $o\in {D^{T}_{v}}$. Hence $\mathfrak {M},v,a\vDash \exists V\forall \bar {v}(V\bar {v}\leftrightarrow \varphi )$. Since v and a were chosen arbitrarily, any closure of this formula by universal quantifiers and □ operators is true in $\mathfrak {M}$ as well. □

To prove the validity of Comp _C , we first introduce a notation for the intension expressed by an open formula.

Definition 20

Let × be a sign, $\mathfrak {M}=\langle W,I,D,V,w\rangle$ a model and $\bar {t}$ a sequence of types. For any formula φ, sequence of variables $\bar {x}$ of types $\bar {t}$, and assignment a for 〈W, I, D〉 admissible for φ, define $\varphi (\bar {x})^{\times }_{\mathfrak {M},a}$ to be the element of $\iota ^{\bar {t}}_{\langle W,I\rangle }$ such that for all v∈W:

$$\begin{array}{@{}rcl@{}} \varphi(\bar{x})^{-}_{\mathfrak{M},a}(v)&=&\{\bar{o}\in{\Pi}_{i<n}D^{t_{i}}_{v}:\mathfrak{M},v,a[\bar{o}/\bar{x}]\vDash\varphi\}\\ \varphi(\bar{x})^{+}_{\mathfrak{M},a}(v)&=&\{\bar{o}\in{\Pi}_{i<n}D^{t_{i}}_{W}:\mathfrak{M},v,a[\bar{o}/\bar{x}]\vDash\varphi\} \end{array} $$

Further, we introduce a way of applying an automorphism of a structure to a model based on it and an assignment for it:

Definition 21

Let $\mathfrak {M}=\langle W,I,D,V,w\rangle$ be a model, a an assignment for $\mathfrak {S}=\langle W,I,D\rangle$ and $\xi \in \text {aut}(\mathfrak {S})$. Define $\xi .\mathfrak {M}=\langle W,I,D,\xi .V,\xi .w\rangle$, where ξ.V is the function on dom(V) such that (ξ.V)(c) = ξ.(V(c)) for all c∈dom(V), and define ξ.a to be the function on dom(a) such that (ξ.a)(v) = ξ.(a(v)) for all v∈dom(a).

With this, we can show that truth of a formula is invariant under applying an automorphisms to the parameters:

Lemma 4

For any model $\mathfrak {M}=\langle W,I,D,V,w\rangle$ , v∈W, formula φ, assignment a admissible for φ and ξ∈aut(〈W,I,D〉),

$$\mathfrak{M},v,a\vDash\varphi\text{ iff }\xi.\mathfrak{M},\xi.v,\xi.a\vDash\varphi.$$

Proof

By induction on the complexity of φ. □

Proposition 8

For each sign ×, $\vDash _{C\times }\times \text {Comp}_{C}$.

Proof

Consider any φ, V and $\bar {v}$ with which an instance of ×Comp _C can be obtained, ×closed model $\mathfrak {M}=\langle W,I,D,V,w\rangle$, v∈W and assignment a admissible for φ such that $\mathfrak {M},v,a\vDash E^{\bar {v}}_{\varphi }$. Let $o=\varphi ^{\times }_{\mathfrak {M},a}(\bar {v})$, so by construction, if ×=−, $\mathfrak {M},v,a[o/V]\vDash \Box \forall \bar {v}(V\bar {v}\leftrightarrow \varphi )$, and if ×=+, $\mathfrak {M},v,a[o/V]\vDash \Box \forall v_{1}\ldots \Box \forall v_{n}\Box (V\bar {v}\leftrightarrow \varphi )$. We show that $o\in {D^{T}_{v}}$. Since $D\boxtimes o$ and $\mathfrak {S}=\langle W,I,D\rangle$ is ×closed, it suffices to show that $\text {fix}(\mathfrak {S},v)\subseteq \text {aut}(\mathfrak {S})_{o}$. So consider any $\xi \in \text {fix}(\mathfrak {S},v)$. To show that $\xi \in \text {aut}(\mathfrak {S})_{o}$, we have to show that ξ.o = o, which is equivalent to the claim that ξ.(o(u)) = o(ξ.u) for all u∈W. So let u∈W. We distinguish two cases.

Case 1: ×=+.:

Then we can prove ξ.(o(u)) = o(ξ.u) by showing that for all $\bar {r}\in {\Pi }_{i\leq n}D^{t_{i}}_{W}$, $\mathfrak {M},u,a[\bar {r}/\bar {v}]\vDash \varphi$ iff $\mathfrak {M},\xi .u,a[\xi .\bar {r}/\bar {v}]\vDash \varphi$.

Case 2: ×=−.:

Then we can prove ξ.(o(u)) = o(ξ.u) by showing that for all $\bar {r}\in {\Pi }_{i\leq n}D^{t_{i}}_{u}$, $\mathfrak {M},u,a[\bar {r}/\bar {v}]\vDash \varphi$ iff $\mathfrak {M},\xi .u,a[\xi .\bar {r}/\bar {v}]\vDash \varphi$.

It suffices to show the first claim, as it entails the second. So consider any $\bar {r}\in {\Pi }_{i\leq n}D^{t_{i}}_{W}$. Since the values of all constants and free variables of φ apart from those in $\bar {v}$ under a are in ${D^{T}_{v}}$, they are mapped to themselves by ξ, so $\mathfrak {M},\xi .u,a[\xi .\bar {r}/\bar {v}]\vDash \varphi$ is the case iff $\xi .\mathfrak {M},\xi .u,\xi .(a[\bar {r}/\bar {v}])\vDash \varphi$. Hence the claim to be proven follows by Lemma 4.

Therefore, if ×=−, $\mathfrak {M},v,a\vDash E^{\bar {v}}_{\varphi }\to \exists V\Box \forall \bar {v}(V\bar {v}\leftrightarrow \varphi )$, and if ×=+, $\mathfrak {M},v,a\vDash E^{\bar {v}}_{\varphi }\to \exists V\Box \forall v_{1}\ldots \Box \forall v_{n}\Box (V\bar {v}\leftrightarrow \varphi )$. As in the proof of Proposition 7, the claim to be proved follows. □

Comp _C is a very strong comprehension principle. In the present infinitary setting, we can even show that it entails Comp⁻.

Proposition 9

For each sign ×, $\times \text {Comp}_{C}\vDash \text {Comp}^{-}$.

Proof

Consider any φ, V and $\bar {v}$ with which an instance of Comp⁻ can be obtained, model $\mathfrak {M}=\langle W,I,D,V,w\rangle$ such that $\mathfrak {M}\vDash \times \text {Comp}_{C}$, v∈W and assignment a admissible for φ. We prove that $\mathfrak {M},v,a\vDash \exists V\forall \bar {v}(V\bar {v}\leftrightarrow \varphi )$. Let $X=\{\bar {o}\in {\Pi }_{i\leq n}D^{t_{i}}_{v}:\mathfrak {M},v,a[\bar {o}/\bar {v}]\vDash \varphi \}$. Let ν be an injection from ${D^{T}_{v}}$ to the class of variables, such that for all types t and $o\in {D^{T}_{v}}$, ν(o) is of type t, and define $\psi =\bigvee _{\bar {o}\in X}\bigwedge _{i\leq n}v_{i}=\nu (o_{i})$. Then by ×Comp _C , $\mathfrak {M},v,\nu ^{-1}\vDash \exists V\Box \forall \bar {v}(V\bar {v}\leftrightarrow \psi )$. So there is an $o\in {D^{T}_{v}}$ such that $o(v)\cap {\Pi }_{i\leq n}D^{t_{i}}_{v}=X$ and $\mathfrak {M},v,a[o/V]\vDash \forall \bar {v}(V\bar {v}\leftrightarrow \varphi )$, from which the claim follows. □

Comp _C also entails that the intensions at any world are closed under conjunction in the sense made precise in Williamson [19, p. 281]. More generally, we can adapt the proof in Fine [5, pp. 154–155] to show that the higher-order domain of any world in any closed structure forms a complete atomic Boolean algebra.

According to the Fine-Stalnaker view of higher-order contingency, higher-order entities have to satisfy certain non-trivial conditions to exist at a world. It is therefore unsurprising that the unrestricted comprehension principle Comp is not valid on the class of closed models.

Here and in the following, it will be helpful to have a concise way of specifying the intensions of type 〈〉 which are true in a certain set of worlds or a certain world (a world-proposition). We therefore give a general definition:

Definition 22

Let $\mathfrak {F}=\langle W,I\rangle$ be a frame. For any X ⊆ W and w∈W, define $X^{\langle \rangle }_{\mathfrak {F}}$ and $w^{\langle \rangle }_{\mathfrak {F}}$ to be the elements of $\iota ^{\langle \rangle }_{\mathfrak {F}}$ such that for all v∈W:

$$\begin{array}{@{}rcl@{}} X^{\langle\rangle}_{\mathfrak{F}}(v)&=&\{\langle\rangle:v\in X\}\\ w^{\langle\rangle}_{\mathfrak{F}}(v)&=&\{\langle\rangle:v=w\} \end{array} $$

We call such an intension the representation of the relevant set of worlds or world in the relevant frame. Specifying the type in the index is necessary in general, as we will later introduce representations of other kinds of entities, but in cases where it is clear from context, we will drop it.

Proposition 10

For each sign ×, $\nvDash _{C\times }\times \text {Comp}$.

Proof

Let $\mathfrak {S}=\langle W,I,B\rangle$ be the structure such that W = {1,2,3}, I = ∅ and B is the domain assignment such that ${B^{t}_{W}}=\emptyset$. Let $\otimes \mathfrak {S}=\langle W,I,D\rangle$. It is easy to check that 1_{〈W, I〉}, the intension which is only true in 1, is in $D^{\langle \rangle }_{1}$ but not in $D^{\langle \rangle }_{2}$, and therefore for any model $\mathfrak {M}$ based on $\mathfrak {S}$, $\mathfrak {M}\nvDash \forall p\Box \exists q\Box (q\leftrightarrow p)$. Since this is an instance of ×Comp, this comprehension principle is invalid on C×. □

As far as the three comprehension principles discussed so far are concerned, the Fine-Stalnaker view holds up well to the challenges raised in Williamson [19] – any version of the model theory considered here satisfies both restricted comprehension principles but invalidates the unrestricted comprehension principle.

5.2 World-Propositions

Both forms of the Fine-Stalnaker view address Williamson’s challenge concerning unification, since they are based on a single unified principle governing the existence of relation which validates both Comp _C and Comp⁻ without validating Comp. Given Proposition 9, one might wonder whether a theory which consisted solely of all instances of Comp _C would not also meet these demands. Williamson seems to think not, since he points out that contingentists might have to postulate Comp⁻ in addition to Comp _C , as Comp⁻ is not derivable from Comp _C . (See Williamson [19, p. 285]; note that Williamson does not make the notion of derivability formally precise.)

However, Williamson’s appeal to a notion of derivability also shows that the unrestricted comprehension principle Comp he advocates may be less powerful than he himself makes it out to be, since from the finitary instances of Comp, we cannot derive (in a certain natural proof system) the claim that necessarily, there is a true proposition which strictly entails every proposition or its negation. Formally, this claim can be stated as follows:

$$\text{Atom}: \Box\exists p^{\langle\rangle}(p\wedge\forall q^{\langle\rangle}(\Box(p\to q)\vee\Box(p\to\neg q))) $$

That Atom is not derivable from finitary Comp was proven in Gallin [10, p. 113, Theorem 15.1], adapting the technique of Boolean-valued models from the literature on forcing in set theory. (In the context of propositional quantifiers, such a principle was missing in an axiomatization suggest by Kripke [13], as noted in Kaplan [11].)

Gallin’s result is essentially an underivability result in a finitary language. If we instead consider the model-theoretic consequence relation among sentences of the infinitary language $\mathcal {L}$, it seems safe to conjecture that Atom does in fact follow from Comp _C (at any world, take the conjunction of all existing true propositions and negations of existing false propositions) and therefore from Comp.

The upshot is that neither a model-theoretic nor a proof-theoretic notion of entailment does the work required to make Williamson’s unification challenge pressing: On the first, Comp⁻ and Atom follow from Comp _C (and all of these follow from Comp), so in this sense neither the higher-order contingentist nor the higher-order necessitist faces any disunity. On the second, Comp⁻, Comp _C and Atom are pairwise independent, and the Fine-Stalnaker view is in this sense disunified, but so is the view of the higher-order necessitist who advocates Comp, since Atom does not follow from it. In the second case, one might appeal to the number of independent principles favoring higher-order necessitism, but this would clearly require a more systematic way of selecting the principles used to compare the two theories.

We now turn to a second issue concerning world-propositions. In the next section, we will consider ways of capturing the Fine-Stalnaker view using object-language comprehension principles. To do so, it will be crucial to be able to rely on every world containing its world-proposition. This is a stronger condition than being differentiated; following Fine [5, p. 163], we adopt the following terminology:

Definition 23

A structure 〈W, I, D〉 is world-selective if $w^{\langle \rangle }_{\langle W,I\rangle }\in D^{\langle \rangle }_{w}$ for all w∈W. A model is world-selective if it is based on a world-selective structure.

Verifying Atom does not suffice for being world-selective. Given the expressive limitations of $\mathcal {L}$ which will be discussed in Part 3, it even seems plausible that there are models which are not world-selective despite verifying Comp _C (which semantically entails Atom over the class of all models) and the fact that all models are based on differentiated structures. In the presence of Comp _C , we can impose the condition of being world-selective by adding the following strengthened version of Atom:

$$\text{Atom}^{*}:\Box\exists p^{\langle\rangle}\left( p\wedge{\bigwedge}_{\bar{t}\text{ types}}\Box\forall X^{\bar{t}}\Box\forall x^{t_{1}}_{1}\ldots\Box\forall x^{t_{n}}_{n}(\Box(p\to X\bar{x})\vee\Box(p\to\neg X\bar{x}))\right) $$

Proposition 11

Let × be a sign and $\mathfrak {M}$ a × model verifying ×Comp _C . $\mathfrak {M}$ is world-selective if and only if $\mathfrak {M}\vDash \textnormal {Atom}^{*}$.

Proof

The ‘only if’ direction is immediate. For the ‘if’ direction, assume $\mathfrak {M}=\langle W,I,D,V,w\rangle$ satisfies Atom^∗, and consider any v∈W. Let $P\in \iota ^{\langle \rangle }_{\mathfrak {F}}$ witness the existential claim of Atom^∗ at v. Consider any u∈W∖{v}. By differentiation, either ${D^{T}_{v}}\neq {D^{T}_{u}}$ or there is a type t≠e and $o\in {D^{T}_{W}}$ such that o(v)≠o(u). In the first case, let o be a member of exactly one of ${D^{T}_{v}}$ and ${D^{T}_{u}}$. Then by ×Comp _C , $D^{\langle \rangle }_{W}$ contains a propositional intension which is true in a world if and only if o exists at it, and so by Atom^∗, P is false in u. In the second case, let $o\in D^{\bar {t}}_{W}$ and $\bar {o}\in {\Pi }_{i\leq n}D^{t_{i}}_{W}$ such that not $\bar {o}\in o(v)$ iff $\bar {o}\in o(u)$. Using Atom^∗, o and $\bar {o}$ witness that P is false in u. Therefore $P=w^{\langle \rangle }_{\langle W,I\rangle }$, as required. □

5.3 A Comprehension Principle for Closure

Williamson discusses higher-order contingentist theories in the form of comprehension principles; in contrast, we have discussed the Fine-Stalnaker view in terms of a class of models. However, in the very rich type-theoretic setting we are working in, this is not the only option. We can also try to capture the ideas behind qualitative generation and higher-order closure with object-language comprehension principles. Structurally, the resulting principles are analogous to Comp _C ; we only replace the existence condition for parameters E _φ with a condition stating that φ has the property of invariance under the relevant permutations. For simplicity, we will first consider the case of + closure in detail, and return to negative semantics in Section 6.4 and to generation in Section 6.5.

To be able to formulate a comprehension principle for + closure, we successively define the relevant concepts. We first have to define how to express quantification over possible entities. Following Fine [4], we start with defining what it is for a proposition to be a world-proposition – a proposition which is true in only one world. We can then define what it is for a formula to be true at a world:

$$\begin{array}{@{}rcl@{}} \text{\textsc{world}}(w^{\langle\rangle})&:=&\Diamond\forall p^{\langle\rangle}(p\leftrightarrow\Box(w\to p))\\ \text{\textsc{at}}(w^{\langle\rangle},\varphi)&:=&\textsc{world}(w)\wedge\Box(w\to\varphi) \end{array} $$

Note that these definitions do not express the intended conditions on all models. E.g., a propositional intension o may satisfy world while being true in more than one world if the propositional domain is sparse enough. This is where the assumption of being world-selective comes into play: from now on, we will only consider world-selective models. As shown above, since all models are by definition based on differentiated structures, this can be enforced in the object language using Comp _C and Atom^∗.

World-propositions allow us to define quantifiers ranging over possible entities, sometimes called outer quantifiers, for which we use π and Σ. The idea behind the definitions of these complex quantifiers is to bind a variable w to the actual world; then we can – in the case of the universal quantifier – express outer quantification by “necessarily for all”, using at and w to evaluate the complement clause of the quantified claim in the world at which we started. For any variable v of type t and formula φ, we therefore define:

$$\begin{array}{@{}rcl@{}} {\Pi} v^{t}\varphi&:=&\exists w^{\langle\rangle}(\textsc{world}(w)\wedge w\wedge\Box\forall v\text{\textsc{at}}(w,\varphi))\\ {\Sigma} v^{t}\varphi&:=&\exists w^{\langle\rangle}(\text{\textsc{world}}(w)\wedge w\wedge\Diamond\exists v\text{\textsc{at}}(w,\varphi)) \end{array} $$

Without being very precise about it, we will assume that the variable w used in the definition of such an outer quantification does not occur in the relevant formula φ. As they will occur repeatedly, we introduce abbreviations for propositional outer quantifiers restricted to world-propositions:

$$\begin{array}{@{}rcl@{}} {\Pi}^{\text{\textsc{world}}} w^{\langle\rangle}\varphi&:=&{\Pi} w^{\langle\rangle}(\text{\textsc{world}}(w)\to\varphi)\\ {\Sigma}^{\text{\textsc{world}}} w^{\langle\rangle}\varphi&:=&{\Sigma} w^{\langle\rangle}(\text{\textsc{world}}(w)\wedge\varphi) \end{array} $$

Since this definition straightforwardly generalizes to finite strings of outer quantifiers, we will write any such string πv ₁…πv _n as πv ₁…v _n . The fact that such definitions cannot be extended to infinite sets of variables will play a crucial role in Part 3.

To be able to capture closure in the formal language, we have to be able to talk about permutations of worlds and permutations of possible individuals. Such permutations are themselves higher-order entities. In the present setting, we may treat them as functional binary relations. Since there is also no type for worlds, we can understand a permutation of worlds to be a functional relation among world-propositions. Thus to talk about permutations of worlds and permutations of possible individuals, we will use variables of type 〈〈〉,〈〉〉 and 〈e, e〉. Given the fact that intensions can have different extensions at different worlds, there are different ways of understanding permutations as relations. Here, we take the simplest option of requiring representations of permutations to have the same extension at every world. We will reconsider this decision in Section 6.3. Formally, we define what it is for a relation of the relevant type to be a permutation as follows:

$$\begin{array}{@{}rcl@{}} \text{\textsc{wperm}}(X^{\langle\langle\rangle,\langle\rangle\rangle})&:=&\\&&{}{\Pi} w^{\langle\rangle}v^{\langle\rangle}(\Diamond Xwv\to(\text{\textsc{world}}(w)\wedge\textsc{world}(v)))\wedge\\&&{} {\Pi}^{\text{\textsc{world}}} w(\\&&{}{\Sigma}^{\text{\textsc{world}}} v\Box({\Pi}^{\text{\textsc{world}}} uXwu\leftrightarrow v{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]{\sim}\end{array}}} u)\wedge\\&&{}{\Sigma}^{\text{\textsc{world}}} v\Box({\Pi}^{\text{\textsc{world}}} uXuw\leftrightarrow v{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]{\sim}\end{array}}} u)\\&&{})\\ \text{\textsc{iperm}}(X^{\langle e,e\rangle})&:=&{\Pi} x^{e}({\Sigma} y^{e}\Box({\Pi} z^{e}Xxz\leftrightarrow y=z)\wedge{\Sigma} y^{e}\Box({\Pi} z^{e}Xzx\leftrightarrow y=z)) \end{array} $$

Next, we define for any such permutations X ^{〈〈〉,〈〉〉} and Y ^{〈e, e〉} what it is for them to map one entity to another. As in the model-theoretic case, we do so by induction on the complexity of types:

$$\begin{array}{@{}rcl@{}} &&{}\text{\textsc{map}}(X^{\langle\langle\rangle,\langle\rangle\rangle},Y^{\langle e,e\rangle},v^{e},u^{e}):=Yvu\\ &&{}\text{\textsc{map}}(X^{\langle\langle\rangle,\langle\rangle\rangle},Y^{\langle e,e\rangle},V^{\bar{t}},U^{\bar{t}}):={\Pi} z^{t_{1}}_{1}{\ldots} z^{t_{n}}_{n}z^{\prime t_{1}}_{1}{\ldots} z^{\prime t_{n}}_{n}{\Pi}^{\text{\textsc{world}}} wv\\ &&\left( \left( Xwv\wedge{\bigwedge}_{i\leq n}\text{\textsc{map}}(X,Y,z_{i},z^{\prime}_{i})\right)\to(\text{\textsc{at}}(w,V\bar{z})\leftrightarrow\text{\textsc{at}}(v,U\bar{z}^{\prime}))\right) \end{array} $$

Using these definitions, we can express what it is for X and Y to constitute an automorphism; X must represent a permutation of worlds, Y a permutation of individuals, and for any type t and pair of worlds w and v such that X w v, X and Y must map the domain of type t at w to the domain of type t at v:

$$\begin{array}{@{}rcl@{}} \text{\textsc{aut}}(X^{\langle\langle\rangle,\langle\rangle\rangle},Y^{\langle e,e\rangle})&:=&\\&&{}\text{\textsc{wperm}}(X)\wedge\text{\textsc{iperm}}(Y)\wedge\\&& {}{\Pi}^{\text{\textsc{world}}} wv(Xwv\to{\bigwedge}_{t\in T}(\\&&{}\text{\textsc{at}}(w,\forall V^{t}{\Pi} U^{t}(\text{\textsc{map}}(X,Y,V,U)\to\text{\textsc{at}}(v,\exists T^{t}T{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]{\sim}\end{array}}} U)))\wedge\\&&{}\textsc{at}(v,\forall U^{t}\textsc{at}(w,\exists V^{t}(\textsc{map}(X,Y,V,U))))\\&&{})) \end{array} $$

Recall that we are only interested in the possible automorphisms of modal space that respect the identities of the actual world and the entities in it. We formalize this as follows:

$$\text{\textsc{fix}}(X^{\langle\langle\rangle,\langle\rangle\rangle},Y^{\langle e,e\rangle}):=\text{\textsc{aut}}(X,Y)\wedge{\Pi}^{\text{\textsc{world}}} w^{\langle\rangle}(w\to Xww)\wedge{\bigwedge}_{t\in T}\forall V^{t}\textsc{map}(X,Y,V,V) $$

We now need to formulate in $\mathcal {L}$ the claim that if fix holds of X and Y, then X and Y preserve the intension expressed by an open formula. That is, we have to write down the condition for an intension expressed by a formula φ (abstracting over a given sequence of variables $\bar {v}$) to be preserved by X and Y, i.e., to be mapped to itself by them. We can do so as follows:

$$\begin{array}{@{}rcl@{}} &&{\kern-1.5pc}\text{\textsc{pres}}(X^{\langle\langle\rangle,\langle\rangle\rangle},Y^{\langle e,e\rangle},\varphi,\bar{v}):={\Pi} z^{t_{1}}_{1}{\ldots} z^{t_{n}}_{n}z^{\prime t_{1}}_{1}{\ldots} z^{\prime t_{n}}_{n}{\Pi}^{\text{\textsc{world}}} wv\\ &&\left( \left( Xwv\wedge\bigwedge_{i\leq n}\text{\textsc{map}}(X,Y,z_{i},z^{\prime}_{i})\right)\to(\text{\textsc{at}}(w,\varphi[\bar{z}/\bar{v}])\leftrightarrow \text{\textsc{at}}(v,\varphi[\bar{z}^{\prime}/\bar{v}]))\right) \end{array} $$

As usual, $\chi [\bar {x}/\bar {y}]$ is the result of replacing free occurrences of y _i in χ by x _i , for all i≤n.

We can now put the pieces together to formulate the higher-order closure view as a comprehension principle. As discussed in Section 2.4, it is natural to formulate it by quantifying over possible permutations, and we follows this option here. In Section 6.6, we will briefly explore a variant view which is formulated using quantification over existing permutations, rather than possible permutations, and conclude that this variant has highly implausible consequences. We therefore state the comprehension principle as follows, where instances of this schema are obtained as from the other comprehension principles (F S stands for “Fine-Stalnaker”):

$$+\text{Comp}_{\mathit{FS}}:={\Pi} XY(\textsc{fix}(X,Y)\to\text{\textsc{pres}}(X,Y,\varphi,\bar{v}))\to\exists V\Box\forall v_{1}\ldots\Box\forall v_{n}\Box(V\bar{v}\leftrightarrow\varphi) $$

With +Comp _{F S} , we have a way of stating the Fine-Stalnaker view in its higher-order closure form in the formal object language (at least in a positive setting, where we don’t impose the being constraint).

5.4 Invalidity

How does +Comp _{F S} relate to C+, the class of world-selective + closed models? It turns out that it doesn’t define it; among world-selective + models, those verifying +Comp _{F S} are not all and only those that are + closed. This would not be too surprising if only the left-to-right direction failed, i.e., if some world-selective + model verifies +Comp _{F S} without being + closed. This kind of mismatch might be explained by the limited expressivity of $\mathcal {L}$ and therefore might not constitute a problem for the view under consideration; we will in fact establish exactly this kind of expressive limitations in a discussion of ×Comp _C in Part 3. However, we will now show that the right-to-left direction fails: there are world-selective + closed models which do not verify +Comp _{F S} . Since +Comp _{F S} is simply a formalized statement of the higher-order closure version of the Fine-Stalnaker view in a positive semantics, this result therefore also shows that the model theory of (world-selective) + closed models is inadequate for its intended purpose, since it fails to validate the formalized statement of the view.

Abstractly, it is not hard to see how C+ might fail to validate +Comp _{F S} . The semantic condition of + closure quantifies over all permutations of worlds and individuals of a model; in contrast, when we evaluate +Comp _{F S} on a model, the initial two outer universal quantifiers get interpreted as quantification over permutations whose representations exist at some world of the model. In this section, we show that this abstract possibility is realized, by exhibiting a world-selective + closed models which does not verify +Comp _{F S} .

We begin by retracing the steps in the sequence of definitions that allowed us to write down +Comp _{F S} and draw out their semantic consequences. The last step of this gives us the condition imposed by +Comp _{F S} . Since specifying the semantic conditions expressed by the syntactic constructions defined above is a routine exercise, we only give the details for the last step, the condition expressed by +Comp _{F S} . To be able to state it, we first define semantically how permutations of worlds and individuals can be represented as intensions of types 〈〈〉,〈〉〉 and 〈e, e〉, extending the notation of Definition 22. Since permutations are functions and we understand functions as functional relations, we state the definition more generally for relations among worlds and individuals:

Definition 24

Let $\mathfrak {F}=\langle W,I\rangle$ be a frame. For any R ⊆ I ² and Z ⊆ W ², define $R^{\langle e,e\rangle }_{\mathfrak {F}}\in \iota ^{\langle e,e\rangle }_{\mathfrak {F}}$ and $Z^{\langle \langle \rangle ,\langle \rangle \rangle }_{\mathfrak {F}}\in \iota ^{\langle \langle \rangle ,\langle \rangle \rangle }_{\mathfrak {F}}$ such that for all w∈W:

$$\begin{array}{@{}rcl@{}} R^{\langle e,e\rangle}_{\mathfrak{F}}(w)&=&R\\ Z^{\langle\langle\rangle,\langle\rangle\rangle}_{\mathfrak{F}}(w)&=&\{\langle v_{\mathfrak{F}},u_{\mathfrak{F}}\rangle:\langle v,u\rangle\in Z\} \end{array} $$

As with the representations defined in Definition 22, we drop the type index when it is clear from the context. It will be useful to note that in all four cases of representations in these two definitions, the function mapping the relevant set of entities to their representations is injective. Furthermore, we state the following very useful lemma:

Lemma 5

Let $\mathfrak {F}=\langle W,I\rangle$ be a frame and $\xi =\langle f,g\rangle \in \text {aut}(\mathfrak {F})$.

• (i) For any X⊆W, $\xi .X_{\mathfrak {F}}=(\xi .X)_{\mathfrak {F}}$.

• (ii) For any w∈W, $\xi .w_{\mathfrak {F}}=(\xi .w)_{\mathfrak {F}}$.

• (iii) For any R⊆I ² , $\xi .R_{\mathfrak {F}}=(g.R)_{\mathfrak {F}}$.

• (iv) For any Z⊆W ² , $\xi .Z_{\mathfrak {F}}=(f.Z)_{\mathfrak {F}}$.

Proof

Routine. □

We now state the model-theoretic condition expressed by +Comp _{F S} :

Lemma 6

Let $\mathfrak {M}=\langle W,I,D,V,w\rangle$ be a world-selective +model, $\mathfrak {S}=\langle W,I,D\rangle$ and $\mathfrak {F}=\langle W,I\rangle$.

Proof

Routine. □

This lemma shows that the condition expressed by +Comp _{F S} may differ from + closure, since it only concerns intensions expressible using some formula φ. Moreover, as advertised above, unlike + closure it concerns only permutations of worlds and individuals that are in the outer domain of 〈〈〉,〈〉〉 and the outer domain of 〈e, e〉, respectively, rather than all such permutations.

We now exhibit a world-selective + closed model that fails to satisfy the condition imposed +Comp _{F S} . The idea behind the model is to take a + closed model of the sort described in Section 2.5, based on four worlds and no individuals with a minimal higher-order domain function, in which, from any world, all other worlds look exactly alike. We then prove that only the identity permutation of worlds exists in the outer domain of the model, and derive from this fact that the structure does not validate +Comp _{F S} . We start with some notation and lemmas.

We use cycle notation to specify permutations; e.g., in the context of S _ω , we write (02)(345) for the permutation which maps 0 to 2 and 2 to 0; 3 to 4, 4 to 5 and 5 to 3; and all other natural numbers to themselves. Let G be a group. For all g∈G, the function mapping each f∈G to g f g ⁻¹ is a permutation of G; this is called conjugation by g. Moreover, the function mapping each g∈G to the conjugation by g is an action, which we call conjugation. Unless indicated otherwise, this is the only action of a group on itself considered below, so we will write g.f for g f g ⁻¹ without further elaborations.

To construct our example, let $\mathfrak {S}^{4}=\langle W,I,B\rangle$ be the structure such that W = {1,2,3,4}, I = ∅ and B is the domain assignment such that ${B^{t}_{W}}=\emptyset$. Let $\mathfrak {F}^{4}=\langle W,I\rangle$ and $\oplus \mathfrak {S}^{4}=\langle W,I,D\rangle$. Since this structure doesn’t contain any individuals, automorphisms are simply given by a permutation of worlds; thus, for any f∈S _W let f ^∅ = 〈f,id _∅ 〉. As B is empty, for any world w, $\text {fix}(\mathfrak {S}^{4},w)$ includes all automorphisms mapping w to itself:

Lemma 7

For all w∈W, $\text {fix}(\mathfrak {S}^{4},w)=\text {aut}(\mathfrak {S}^{4})_{w}=\{f^{\emptyset }:f\in {(S_{W})}_{w}\}$.

Proof

Immediate. □

However, only the trivial permutation among worlds is represented in the domain of any world in $\oplus \mathfrak {S}^{4}$:

Lemma 8

If f∈S _W and $f_{\mathfrak {F}^{4}}\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$ then f=id.

Proof

Consider any f∈S _W ∖{id} and w∈W; we show that $f_{\mathfrak {F}^{4}}\notin D^{\langle \langle \rangle ,\langle \rangle \rangle }_{w}$. Since f≠id, there is a v∈W such that f(v)≠v. Let u∈{v, f(v)}∖{w} and u ^′∈W∖{w, v, f(v)}; such elements clearly exist. It is routine to show that then, (u u ^′).f≠f, so by Lemma 5 (iv), $(uu^{\prime })^{\emptyset }.f_{\mathfrak {F}^{4}}\neq f_{\mathfrak {F}^{4}}$. By Lemma 7, $(uu^{\prime })^{\emptyset }\in \text {fix}(\mathfrak {S}^{4},w)$, so $f_{\mathfrak {F}^{4}}\notin D^{\langle \langle \rangle ,\langle \rangle \rangle }_{w}$. □

Using world-propositions, it is easy to show that there is higher-order contingency in $\oplus \mathfrak {S}^{4}$:

Lemma 9

For all w,v∈W, if w≠v then $v_{\mathfrak {F}^{4}}\notin D^{\langle \rangle }_{w}$.

Proof

Let w≠v, and consider any g∈(S _W ) _w such that g(v)≠v. Thus $g(v)_{\mathfrak {F}^{4}}\neq v_{\mathfrak {F}^{4}}$. By Lemma 5 (ii), $g^{\emptyset }.v_{\mathfrak {F}^{4}}=g(v)_{\mathfrak {F}^{4}}$, so $g^{\emptyset }.v_{\mathfrak {F}^{4}}\neq v_{\mathfrak {F}^{4}}$. By Lemma 7, $g^{\emptyset }\in \text {fix}(\mathfrak {S}^{4},w)$, so $v_{\mathfrak {F}^{4}}\notin D^{\langle \rangle }_{w}$. □

It follows straightforwardly with the last two lemmas and Lemma 5 that +Comp _{F S} is not true in any model based on $\oplus \mathfrak {S}^{4}$, and therefore not valid on C+. Since all + closed structures are world-selective, this establishes the central claim of this section.

Theorem 1

$\nvDash _{C+}+\text {Comp}_{\mathit {FS}}$.

Proof

Let $\mathfrak {M}$ be a model based on $\oplus \mathfrak {S}^{4}$. Consider any w, v∈W such that w≠v. For all $\xi \in \text {fix}(\mathfrak {S}^{4},v)$, ξ.v = v, so by Lemma 5 (ii), $\xi .v_{\mathfrak {F}^{4}}=v_{\mathfrak {F}^{4}}$. Trivially, $D\boxplus v_{\mathfrak {F}^{4}}$, so $v_{\mathfrak {F}^{4}}\in D^{\langle \rangle }_{v}$. Consider any assignment a mapping p ^〈〉 to $v_{\mathfrak {F}^{4}}$. By Lemma 8, the only f∈S _W such that $f_{\mathfrak {F}^{4}}\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$ is id, so by Lemma 6, $\mathfrak {M}$ only verifies +Comp _{F S} if $v_{\mathfrak {F}^{4}}\in D^{\langle \rangle }_{w}$. As shown in Lemma 9, this is not the case, so $\mathfrak {M}\nvDash +\text {Comp}_{\mathit {FS}}$. □

6 Internal Closure and Internal Generation

Given that +Comp _{F S} is not valid on world-selective + closed models, a defender of the higher-order closure variant of the Fine-Stalnaker view faces a choice: They can either modify the model theory so as to validate the comprehension principle +Comp _{F S} or come up with an alternative object-language statement of their view. In this section, we consider the first option, and develop a more restrictive class of models, which we call internally +closed, on which +Comp _{F S} is valid. The second option is considered in Part 3.

6.1 Internal Closure

The definition of internal closure is basically dictated by Lemma 6: we want to express the condition expressed by +Comp _{F S} , and generalize it in the natural way to remove the language-dependence. Modifying the definition of closure, we have to restrict the quantification over permutations to those whose representation is in the domain of some world of the model. We start by introducing some terminology, defining variants of aut and fix, restricted to pairs of permutations existing at some world. These definitions will be phrased slightly more generally than required here, so that we will be able to use them again when we investigate analogous adaptations of the notion of qualitative generation in Section 6.5.

Definition 25

Let $\mathfrak {S}=\langle W,I,B\rangle$ and $\mathfrak {S}^{\prime }=\langle W,I,D\rangle$ be structures, $\mathfrak {F}=\langle W,I\rangle$ and $\langle f,g\rangle \in \text {aut}(\mathfrak {F})$.

• f is possible in $\mathfrak {S}^{\prime }$ iff $f_{\mathfrak {F}}\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$.

• g is possible in $\mathfrak {S}^{\prime }$ iff $g_{\mathfrak {F}}\in D^{\langle e,e\rangle }_{W}$.

• 〈f, g〉 is possible in $\mathfrak {S}^{\prime }$ iff f and g are possible in $\mathfrak {S}^{\prime }$.

For any w∈W, define $\text {aut}(\mathfrak {S})|\mathfrak {S}^{\prime }$ to be the set of elements of $\text {aut}(\mathfrak {S})$ which are possible in $\mathfrak {S}^{\prime }$, and $\text {fix}(\mathfrak {S},w)|\mathfrak {S}^{\prime }$ to be the set of elements of $\text {fix}(\mathfrak {S},w)$ which are possible in $\mathfrak {S}^{\prime }$.

We can now state the condition of being internally closed by replacing $\text {fix}(\mathfrak {S},w)$ in the definition of closure by $\text {fix}(\mathfrak {S},w)|\mathfrak {S}$:

Definition 26

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure. $\mathfrak {S}$ is internally +closed if for all w∈W, types t≠e and $o\in \iota _{\langle W,I\rangle }^{t}$,

$$o\in {D^{t}_{w}}\; \text{iff}\; D\boxplus o\; \text{and} \;\xi.o=o\; \text{for all} \;\xi\in\text{fix}(\mathfrak{S},w)|\mathfrak{S}. $$

A model is internally + closed just in case it is based on an internally + closed structure.

6.2 Comprehension and Comparison to Closure

It is straightforward to prove that the restriction to internally + closed models solves the problem described in the last section:

Proposition 12

+Comp _FS is valid on the class of world-selective internally +closed models.

Proof

With Lemma 6, this is immediate by definition. □

It is also straightforward to show that internal + closure implies + closure, but not vice versa.

Proposition 13

Any internally +closed model is +closed.

Proof

Consider any model based on an internally + closed structure $\mathfrak {S}=\langle W,I,D\rangle$, w∈W, type t≠e and $o\in \iota ^{T}_{\langle W,I\rangle }$. If $o\in {D^{T}_{W}}$, then since $\mathfrak {S}$ is internally + closed, $D\boxplus o$. Also, since $o\in {D^{T}_{W}}$, ξ.o = o for all $\xi \in \text {fix}(\mathfrak {S},w)$. If $D\boxplus o$ and ξ.o = o for all $\xi \in \text {fix}(\mathfrak {S},w)$, then since $\text {fix}(\mathfrak {S},w)|\mathfrak {S}\subseteq \text {fix}(\mathfrak {S},w)$, ξ.o = o for all $\xi \in \text {fix}(\mathfrak {S},w)|\mathfrak {S}$. Since $\mathfrak {S}$ is internally + closed, $o\in {D^{T}_{W}}$. So $\mathfrak {S}$ is + closed, and so the model with which we started is + closed as well. □

Proposition 14

There is a +closed model which is not internally +closed.

Proof

We established in Theorem 1 that there is a + closed model which does not verify +Comp _{F S} ; the claim follows with Proposition 12. □

As a corollary to Proposition 13, we immediately obtain that Comp⁻ and +Comp _C are valid on internally + closed structures. We can also extend the result of Proposition 10 to internally + closed structures and prove that they do not validate unrestricted comprehension:

Proposition 15

+Comp is not valid on the class of internally +closed models.

Proof

We show that for $\mathfrak {S}=\langle W,I,B\rangle$ used in the proof of Proposition 10, $\oplus \mathfrak {S}=\langle W,I,D\rangle$ is internally + closed. To do so, we show that for all w∈W, $\text {fix}(\oplus \mathfrak {S},w)|{\oplus }\mathfrak {S}=\text {fix}(\oplus \mathfrak {S},w)$. Note that by Lemma 3, $\text {fix}(\oplus \mathfrak {S},w)=\{\langle f,\emptyset \rangle :f\in (S_{W})_{w}\}$, so it suffices to prove that $f_{\langle W,I\rangle }\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$ for all f∈(S _W ) _w . Letting W = {w, v, u}, note that (S _W ) _w = {id,(v u)}. The claim is straightforward for id. We show that $(vu)_{\langle W,I\rangle }\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{w}$. To do so, it suffices to show that g.(v u) = (v u) for all g∈(S _W ) _w . The claim is trivial for g = id, so it only remains to show that (v u).(v u) = (v u), which is straightforward. □

6.3 Cumulative Representations of Permutations

When we defined +Comp _{F S} , we chose to regiment talk of permutations of worlds and individuals as talk of binary relations among world-propositions and individuals which have the same extension at every world. This choice wasn’t forced on us; we could also have chosen to allow relations which vary in extension across worlds, but in some other way uniquely specify a way of permuting worlds or individuals. One might wonder whether this choice influenced the resulting theory; in particular, one might wonder whether there is some other way of formalizing in $\mathcal {L}$ quantification over permutations of modal space which gives rise to a different notion of internal closure. One might even hope for such a revision to establish the equivalence with closure. Exemplarily, we consider one natural such revision and show that it determines the same class of structures.

From a model-theoretic perspective, what gives rise to the the mismatch between closure and internal closure is that in some structures, some permutations of worlds and individuals are not represented in the domain of any world. The most natural thought is therefore to look for weaker notions of representation, and the most straightforward way of implementing this is to require a representation of a permutation of individuals to possibly relate one individual to another if and only if the first is mapped to the second by the permutation, and weaken the requirement for world permutations analogously. On this proposal, we no longer have a unique representative for a given permutation, but this is of course part of the desired generality.

Definition 27

Let $\mathfrak {F}=\langle W,I\rangle$ be a frame.

• For any R ⊆ I ² and $o\in \iota _{\mathfrak {F}}^{\langle e,e\rangle }$, o cumulatively represents R in $\mathfrak {F}$ if $\bigcup _{w\in W}o(w)=R$.

• For any Z ⊆ W ² and $o\in \iota _{\mathfrak {F}}^{\langle \langle \rangle ,\langle \rangle \rangle }$, o cumulatively represents Z in $\mathfrak {F}$ if $\bigcup _{w\in W}o(w)=\{\langle w_{\mathfrak {F}},v_{\mathfrak {F}}\rangle :\langle w,v\rangle \in Z\}$.

We can now define a condition analogous to internal closure using cumulative representations of permutations, and then show that this change makes no difference – the notions coincide. Since this condition will be less important in what follows, the definitions are somewhat condensed.

Definition 28

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure and w∈W. Define $\text {fix}(\mathfrak {S},w)|_{c}\mathfrak {S}$ to be the set of $\langle f,g\rangle \in \text {fix}(\mathfrak {S},w)$ such that there is an $f_{c}\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$ which cumulatively represents f and a $g_{c}\in D^{\langle e,e\rangle }_{W}$ which cumulatively represents g.

Since every representation of a permutation cumulatively represents it, it is immediate that in general $\text {fix}(\mathfrak {S},w)|\mathfrak {S}\subseteq \text {fix}(\mathfrak {S},w)|_{c}\mathfrak {S}$.

Definition 29

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure. $\mathfrak {S}$ is cumulatively internally +closed if for all w∈W, types t≠e and $o\in \iota _{\langle W,I\rangle }^{t}$,

$$o\in {D^{t}_{w}}\; \text{iff}\; D\boxplus o\; \text{and}\; \xi.o=o\; \text{for all}\; \xi\in\text{fix}(\mathfrak{S},w)|_{c}\mathfrak{S}. $$

Lemma 10

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure, $\mathfrak {F}=\langle W,I\rangle$ , f∈S _W , g∈S _I , f _c a cumulative representation of f, g _c a cumulative representation of f, and $\xi \in \text {aut}(\mathfrak {S})$ . Then

$$\begin{array}{@{}rcl@{}} If\; \xi.f_{c}=f_{c}\; then\; \xi.f_{\mathfrak{F}}=f_{\mathfrak{F}},\\ If \;\xi.g_{c}=g_{c}\; then \;\xi.g_{\mathfrak{F}}=g_{\mathfrak{F}}. \end{array} $$

Proof

We present only the case for f; the case for g can be proven in exactly the same way. Let ξ = 〈h, i〉. Assume $\xi .f_{\mathfrak {F}}\neq f_{\mathfrak {F}}$. Then by Lemma 5 (iv), $(\xi .f)_{\mathfrak {F}}\neq f_{\mathfrak {F}}$, so by the injectivity of the function mapping every permutation to its representation, h.f≠f. So there is a w∈W such that h f h ⁻¹(w)≠f(w), and therefore v = h ⁻¹(w) is such that h f(v)≠f h(v). Since f _c cumulatively represents f, there is a u∈W such that $\langle v_{\mathfrak {F}},f(v)\rangle \in f_{c}(u)$. So $\langle \xi .v_{\mathfrak {F}},\xi .(f(v)_{\mathfrak {F}})\rangle \in \xi .f_{c}(\xi .u)$. By Lemma 5 (ii), it follows that $\langle h(v)_{\mathfrak {F}},(hf(v))_{\mathfrak {F}})\rangle \in \xi .f_{c}(\xi .u)$. Since f h(v)≠h f(v) and f _c cumulatively represents f, $\langle h(v)_{\mathfrak {F}},(hf(v))_{\mathfrak {F}})\rangle \in f_{c}(\xi .u)$. So ξ.f _c ≠f _c . □

Proposition 16

A structure is internally +closed if and only if it is cumulatively internally +closed.

Proof

That every internally + closed structure is cumulatively internally + closed can be proven analogously to Proposition 13. So consider any cumulatively internally + closed structure $\mathfrak {S}=\langle W,I,D\rangle$, w∈W, type t≠e and $o\in \iota ^{T}_{\langle W,I\rangle }$. Let $\mathfrak {F}=\langle W,I\rangle$. Since $\text {fix}(\mathfrak {S},w)|\mathfrak {S}\subseteq \text {fix}(\mathfrak {S},w)|_{c}\mathfrak {S}$, it is immediate that if $o\in {D^{T}_{W}}$ then $D\boxplus o$ and ξ.o = o for all $\xi \in \text {fix}(\mathfrak {S},w)|\mathfrak {S}$. For the converse direction, assume $o\notin {D^{t}_{w}}$ and $D\boxplus o$. Then there is a $\langle f,g\rangle \in \text {fix}(\mathfrak {S},w)|_{c}\mathfrak {S}$ such that 〈f, g〉.o≠o. So there are $f_{c}\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$ and $g_{c}\in D^{\langle e,e\rangle }_{W}$ such that f _c cumulatively represents f and g _c cumulatively represents g. As $\mathfrak {S}$ is cumulatively internally + closed, (i) $v_{\mathfrak {F}}\in D^{\langle \rangle }_{v}$ for all v∈W, and (ii) ξ.f _c = f _c and ξ.g _c = g _c for all $\xi \in \text {fix}(\mathfrak {S},w)|_{c}\mathfrak {S}$. By (i), $D\boxplus f_{\mathfrak {F}}$ and $D\boxplus g_{\mathfrak {F}}$. With Lemma 10, it follows from (ii) that $\xi .f_{\mathfrak {F}}=f_{\mathfrak {F}}$ and $\xi .g_{\mathfrak {F}}=g_{\mathfrak {F}}$ for all $\xi \in \text {fix}(\mathfrak {S},w)|_{c}\mathfrak {S}$. Hence $\langle f,g\rangle \in \text {fix}(\mathfrak {S},w)|\mathfrak {S}$. □

This result shows that in defining internal closure, it makes no difference whether we quantify only over representations of permutations, or include intensions which merely cumulatively represent permutations. Similar results can be obtained for other ways of understanding quantification over permutations in our type-theoretic setting. E.g., we could understand permutations to be individuals, which can be applied to worlds or individuals using an application relation. We can show that every structure internally closed on such an understanding is internally closed as defined above.

6.4 Internal Closure in Negative Semantics

So far, we have worked in a positive semantics. Were we instead to assume the being constraint, we could formulate a comprehension principle analogous to +Comp _{F S} , prove that it is invalid on −closed models, and conclude that −closed models are an inadequate semantics for the higher-order closure view. Since doing so is straightforward, let us move straight to defining the model-theoretic condition of internal −closure.

In the setting of negative semantics, the choice of requiring the representation of a permutation to have a constant intension immediately creates problems: whenever there is any variation in the first-order domain function, no permutation of individuals counts as possible in the relevant structure. Quantification over automorphisms in the closure constraint is then vacuous, and thus forces the domains of all worlds to contain all intensions which are supported by the domain function, which entails, among other things, propositional necessitism (□∀p ^〈〉□∃q ^〈〉□(p↔q)). It is therefore natural to instead formulate internal −closure using cumulatively representing intensions. Of course, there is no reason to think that the analog to Proposition 16 in a negative setting holds. We therefore define:

Definition 30

A structure $\mathfrak {S}=\langle W,I,D\rangle$ is internally −closed if for all w∈W, types t≠e and $o\in \iota _{\langle W,I\rangle }^{t}$,

$$o\in {D^{t}_{w}}\; \text{iff}\; D\boxminus o\; \text{and}\; \xi.o=o\; \text{for all} \;\xi\in\text{fix}(\mathfrak{S},w)|_{c}\mathfrak{S} $$

This definition does not make being internally −closed incompatible with contingency in what individuals there are. However, it is not hard to see that we get similar problems in cases in which there are incompossible individuals which are indistinguishable from some world. The being constraint ensures that we cannot map any individual to one incompossible with it using an automorphism which has a possible cumulative representation, but the definition of internal −closure may require there to be such intensions in order for the individuals to be possibly indistinguishable. The following proposition illustrates this problem using a very simple example.

Proposition 17

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure such that W={1,2,3}, I={a,b} (for some distinct a and b) and D such that ${D^{e}_{1}}=\emptyset$ , ${D^{e}_{2}}=\{a\}$ , ${D^{e}_{3}}=\{b\}$ , and $o\notin D^{\langle e\rangle }_{1}$ , where o is the element of $\iota ^{\langle e\rangle }_{\langle W,I\rangle }$ such that o(1)=o(3)=∅ and o(2)={a}. $\mathfrak {S}$ is not internally −closed.

Proof

We distinguish two cases.

Case 1: :

There is a g∈S _I which has a cumulative representation g _c in $D^{\langle e,e\rangle }_{W}$ such that g(a) = b or g(b) = a. Then there are w, v∈W such that $o\in D^{\langle e,e\rangle }_{w}$, and 〈a, b〉∈o(v) or 〈b, a〉∈o(v). Thus not $D\boxminus o$, and so $\mathfrak {S}$ is not internally −closed.

Case 2: :

There is no g∈S _I such that g(a) = b or g(b) = a which has a cumulative representation in $D^{\langle e,e\rangle }_{W}$. Consider any $\langle f,g\rangle \in \text {fix}(\mathfrak {S},1)|_{c}\mathfrak {S}$. Then g has a cumulative representation in $D^{\langle e,e\rangle }_{W}$, so g = id _I . Since $\langle f,g\rangle \in \text {aut}(\mathfrak {S})$, it follows that f = id _W . So 〈f, g〉.o = o. As $D\boxminus o$ and $o\notin D^{\langle e\rangle }_{1}$, $\mathfrak {S}$ is not internally −closed.

□

The constraints on the structure described in this proposition fit the higher-order closure view perfectly: at world 1, we might have no materials to distinguish individual a at world 2 from individual b at world 3, so the property which only applies to individual a at 2 should not exist at world 1.

There is no obvious way of weakening the notion of cumulative representation even further to allow this structure. Thus if there are incompossible indistinguishable possible individuals, the higher-order closure view is incompatible with the being constraint, destabilizing Stalnaker’s overall position. And from a contingentist perspective, it is plausible that there are incompossible indistinguishable possible individuals: consider the knives that could have been made from a merely possible handle and two qualitatively indistinguishable merely possible blades.

There is a way of modifying the being constraint imposed by negative semantics to solve the problem. Both Stalnaker and Williamson only discuss the being constraint as applied to relations among individuals. If we weaken the being constraint to only apply to such relations, then we can solve the problem pointed out in this section by representing permutations of possible individuals not using relations among individuals but using relations among haecceities of individuals (properties necessarily equivalent to being identical to those individuals). We won’t explore this option further. Instead, we now turn to adapting the notion of internal closure to the case of generation in a positive setting. The issues raised will not essentially depend on the choice of positive semantics.

6.5 Internal Generation

Like the definition of closure, we can revise the definition of generation by restricting our quantification over automorphisms to those which are possible in the structure, in the sense defined above. We could also formulate this proposal in the form of a comprehension principle, although this would require extending the syntax to include a connective which expresses the condition of being a ‘generating’ relation. We omit a formal discussion of these issues and move straight to the model-theoretic condition of internal generation.

In the definition of generation, we are dealing with two structures, the generated one and the generating one. We restrict the quantification over permutations to permutations which are possible in the generated structure, as there is no reason why we should only be able to appeal to generating permutations in stating the view. Imposing this restriction fundamentally changes the nature of generation. The qualitative generation view is intended as a reductive account of the existence of relations (whereas the higher-order closure view is simply a constraint on what relations there are). Adding a restriction to possibly existing permutations creates trouble for generation understood in this way, because the existence condition for higher-order entities becomes dependent on the generated higher-order domains. Thus we can no longer assume that for a given distribution of individuals and intensions, there is a unique structure generated by it. Consequently, we define internal + generation as a relation rather than a function. The natural way to do so is as follows:

Definition 31

Let $\mathfrak {S}=\langle W,I,B\rangle$ and $\mathfrak {S}^{\prime }=\langle W,I,D\rangle$ be structures. $\mathfrak {S}^{\prime }$ is internally +generated by $\mathfrak {S}$ if for all w∈W, ${D^{e}_{w}}={B^{e}_{w}}$ and for all types t≠e and $o\in \iota ^{T}_{\langle W,I\rangle }$,

$$o\in {D^{t}_{w}}\; \text{iff}\; D\boxplus o\; \text{and}\;\xi.o=o\; \text{for all} \;\xi\in\text{fix}(\mathfrak{S},w)|\mathfrak{S}^{\prime}. $$

A model is internally + generated just in case it is based on an internally + generated structure.

We show that this relation of internal + generation is not functional: one structure can internally + generate two distinct structures. To specify these structures, we make use of the cycle notation for permutations introduced above, as well as writing, for any element g of a group G, 〈g〉 for the subgroup of G generated by g, which consists of the combinations of g with itself using composition and inverses.

Proposition 18

There are structures $\mathfrak {S}$ , $\mathfrak {S}^{\prime }$ and $\mathfrak {S}^{\prime \prime }$ such that $\mathfrak {S}^{\prime }$ and $\mathfrak {S}^{\prime \prime }$ are distinct and both are internally +generated by $\mathfrak {S}$.

Proof

Let $\mathfrak {S}=\langle W,I,D\rangle$ be the structure given by W = {0,1,2,3,4} and $I={D^{T}_{W}}=\emptyset$. Using addition modulo 5, let for each w∈W

$$\begin{array}{@{}rcl@{}} g^{w}&=&(w+1\;w+2\;w+3\;w+4)\; \text{and} \;G^{w}=\langle g^{w}\rangle,\\ h^{w}&=&(w+1\;w+2\;w+4\;w+3)\; \text{and} \;H^{w}=\langle h^{w}\rangle. \end{array} $$

Let $\mathfrak {F}=\langle W,I\rangle$. As in Section 5.4, we abbreviate 〈f, ∅〉, for any f∈S _W , as f ^∅. Let $\mathfrak {S}^{\prime }=\langle W,I,D^{\prime }\rangle$ and $\mathfrak {S}^{\prime \prime }=\langle W,I,D^{\prime \prime }\rangle$ be the structures such that for all w∈W, types t≠e and $o\in \iota ^{t}_{\mathfrak {F}}$,

$$\begin{array}{@{}rcl@{}} o&\in&{D}^{\prime t}_{w}\; \text{iff} \;D^{\prime}\boxplus o\; \text{and}\; f^{\emptyset}.o=o\; \text{for all}\; f\in G^{w},\\ o&\in&{D}^{\prime\prime t}_{w}\; \text{iff} \;D^{\prime\prime}\boxplus o\; \text{and}\; f^{\emptyset}.o=o\; \text{for all} \;f\in H^{w}. \end{array} $$

$\mathfrak {S}^{\prime }$ and $\mathfrak {S}^{\prime \prime }$ are distinct since $(1234)_{\mathfrak {F}}\in D^{\prime \langle \langle \rangle ,\langle \rangle \rangle }_{0}$ and $(1234)_{\mathfrak {F}}\notin D^{\prime \prime \langle \langle \rangle ,\langle \rangle \rangle }_{0}$.

To show that both $\mathfrak {S}^{\prime }$ and $\mathfrak {S}^{\prime \prime }$ are internally + generated by $\mathfrak {S}$, it suffices to show that for all w∈W and f∈S _W , $f^{\emptyset }\in \text {fix}(\mathfrak {S},w)|\mathfrak {S}^{\prime }$ iff f∈G ^w, and $f^{\emptyset }\in \text {fix}(\mathfrak {S},w)|\mathfrak {S}^{\prime \prime }$ iff f∈H ^w. We will now establish this for G; the case of H is parallel.

First, note that f is possible in $\mathfrak {S}^{\prime }$ iff there is a v∈W such that $f_{\mathfrak {F}}\in D^{\prime \langle \langle \rangle ,\langle \rangle \rangle }_{v}$, which in turn is the case iff $D^{\prime }\boxplus f_{\mathfrak {F}}$ and $g^{\emptyset }.f_{\mathfrak {F}}=f_{\mathfrak {F}}$ for all g∈G ^v. The former is the case for any f∈S _W , and the latter is the case iff g.f = f for all g∈G ^v; it is routine to show that this is the case iff f∈G ^v.

Since all domains of $\mathfrak {S}$ are empty, f ^∅ is trivially an automorphism of $\mathfrak {S}$ which maps all elements of ${D^{t}_{w}}$ to themselves. So $f^{\emptyset }\in \text {fix}(\mathfrak {S},w)|\mathfrak {S}^{\prime }$ iff f(w) = w and both f and id _∅ are possible in $\mathfrak {S}^{\prime }$. id _∅ is possible in $\mathfrak {S}^{\prime }$, and as we have shown, f is possible in $\mathfrak {S}^{\prime }$ iff there is a v∈W such that f∈G ^v. If f(w) = w, this is the case iff f∈G ^w. So $f^{\emptyset }\in \text {fix}(\mathfrak {S},w)|\mathfrak {S}^{\prime }$ iff f∈G ^w. □

We take it that the main attraction of the qualitative generation view over the higher-order closure view is the reductive account of what relations there are that it supposedly affords. As we just saw, taking higher-order contingency seriously shows that this supposed difference is chimerical. Qualitative generation still offers an explanation of the source of higher-order contingency, since some structures internally + generate only structures with variable higher-order domains (and, moreover, generate at least one such structure). However, there is a further, more serious, problem for the qualitative generation view as formalized by the class of internally + generated models: it fails to validate +Comp _C . The basic observation which drives the proof is that the automorphisms of $\mathfrak {F}$ determined by the members of G ^w and H ^w are only required to be automorphisms of the generating structure, but not automorphisms of the respective generated structures. Consequently, the domains of these generated structures fail to include some intensions which are definable in terms of existing entities.

Proposition 19

+Comp _C is not valid on the class of internally +generated models.

Proof

Let $\mathfrak {F}=\langle W,I\rangle$, $\mathfrak {S}^{\prime }=\langle W,I,D^{\prime }\rangle$ and the functions g and G on W be defined as in the proof of Proposition 18, and let $\mathfrak {M}$ be a model based on $\mathfrak {S}^{\prime }$. Define

$$\varphi:=\exists Y^{\langle\langle\rangle,\langle\rangle\rangle}{\Sigma}^{\text{\textsc{world}}} wv(\text{\textsc{wperm}}(Y)\wedge\neg(w{{\begin{array}{c}\text{\textsc{hi}}\\[-4pt]{\sim}\end{array}}} v)\wedge Xwv\wedge Xvw\wedge Ywv\wedge Yvw) $$

Let a be an assignment such that $a(X)=(g^{0}g^{0})_{\mathfrak {F}}=(13)(24)_{\mathfrak {F}}$. $\mathfrak {M}$ is world-selective, so wperm expresses the intended condition on it. So $\varphi ^{+}_{\mathfrak {M},a}$, the propositional intension expressed by φ relative to $\mathfrak {M}$ and a, is true in the worlds in which there is a representation of a world permutation f such that f(1)=3 and f(3)=1, or f(2)=4 and f(4)=2. This is of course the case for 0, where (13)(24) is represented, and otherwise only for 1, where g ¹ g ¹ = (03)(24) is represented, and 4, where g ⁴ g ⁴ = (02)(13) is represented. Since $a(X)=(13)(24)_{\mathfrak {F}}$ exists in 0, the truth of +Comp _C in $\mathfrak {M}$ would entail that $\varphi ^{+}_{\mathfrak {M},a}=\{0,1,4\}_{\mathfrak {F}}$ exists in 0, but this is not the case since $(1234)^{\emptyset }.\{0,1,4\}_{\mathfrak {F}}=\{0,1,2\}_{\mathfrak {F}}\neq \{0,1,4\}_{\mathfrak {F}}$. So +Comp _C is not true in $\mathfrak {M}$. □

In response to these problems, one might propose to adapt as one’s model theory the class of internally + generated models which are also internally + closed. Since every internally + closed model is internally + generated (since it internally + generates itself), this is the class of internally + closed models. +Comp _C is valid on the class of internally + closed models, so this proposal solves the problem posed by Proposition 19, albeit in a rather ad hoc fashion. The proposal would gain some appeal if we could prove that when restricting the generated structures to internally + closed ones, internal + generation is a total function. Whether this holds is an open question given what we have established so far. On the one hand, it might well be possible to strengthen Proposition 18 to show that there are distinct internally + closed structures which are internally + generated by the same structure. On the other hand, it might well be that some structures do not internally + generate any internally + closed structure; in fact, we have not even established that every structure internally + generates some structure (whether internally + closed or not). We leave these questions open.

6.6 Existing Representations of Permutations

We now return to the option of formulating a version of higher-order closure which quantifies over all permutations instead of all possible permutations. A corresponding variant of +Comp _{F S} is defined by replacing the outer quantifier binding X and Y by ∀. It is easily seen that this variant entails +Comp _{F S} as defined above: over world-selective models, πX Y φ entails ∀X Y φ, so ∀X Y φ→ψ entails πX Y φ→ψ. This strengthening of +Comp _{F S} corresponds to the following strengthening of internal closure:

Definition 32

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure. For any w∈W, define $\text {fix}(\mathfrak {S},w)|\mathfrak {S},w$ to be the set of $\langle f,g\rangle \in \text {fix}(\mathfrak {S},w)$ such that $f_{\langle W,I\rangle }\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$ and $g_{\langle W,I\rangle }\in D^{\langle e,e\rangle }_{w}$.

$\mathfrak {S}$ is strongly internally +closed if for all w∈W, types t≠e and $o\in \iota _{\langle W,I\rangle }^{t}$,

$$o\in {D^{t}_{w}}\; \text{iff}\; D\boxplus o\; \text{and}\; \xi.o=o\; \text{for all}\; \xi\in\text{fix}(\mathfrak{S},w)|\mathfrak{S},w. $$

A model is strongly internally + closed just in case it is based on a strongly internally + closed structure.

It turns out that strong internal + closure is implausibly restrictive: it rules out patterns of indistinguishability which naturally fit the intuitive motivations for the higher-order closure view, and which are plausibly instantiated if it is true. As an example, consider three electrons. Each of them could have existed without the others, in qualitatively identical circumstances. Further, it could have been that none of them exist, and that consequently, no distinctions can be drawn among them. This is ruled out by strong internal + closure, as we now show more precisely.

To do so, we first have to clarify the relevant kind of indistinguishability. It is not enough that no two of the three worlds can be distinguished from the fourth, which we might call pairwise indistinguishability. Rather, any way of permuting them must be allowed, which we might call collective indistinguishability. To make this idea precise, we let, for any permutation g of a set X, the support of g, written supp(g), be the set of elements moved by g, i.e., supp(g) = {x∈X:g(x)≠x}.

Definition 33

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure, X ⊆ W and w∈W. We define the members of X to be collectively indistinguishable from w if for all f∈S _W such that supp(f)⊆X, there is a g∈S _I such that $\langle f,g\rangle \in \text {fix}(\mathfrak {S},w)$.

The difference between pairwise and collective indistinguishability is also relevant for the two kinds of models for the contingent existence of propositions proposed in Stalnaker [18, Appendix A]; see Fritz [7] and Part 2.

To be able to appeal to it again below, we first prove part of the result on strong internal + closure as a lemma:

Lemma 11

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure, X⊆W and w∈W such that |X|≥3. If the members of X are collectively indistinguishable from w, then for every v∈X and f∈S _W such that $f_{\langle W,I\rangle }\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$ , f(v)=v.

Proof

Assume for contradiction that there are v∈X and f∈S _W such that $f_{\langle W,I\rangle }\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$ and f(v)≠v. Let u∈X∖{v, f(v)}. Since {v, u}⊆X, it follows from the fact that the members of X are collectively indistinguishable from w that there is an h∈S _I such that $\langle (vu),h\rangle \in \text {fix}(\mathfrak {S},w)$. So 〈(v u), h〉.f _{〈W, I〉} = f _{〈W, I〉}, and thus by Lemma 5 (iv), (v u).f = f. But (v u).f(u) = f(v) which is distinct from f(u) as v≠u. . □

Proposition 20

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure, X⊆W and w∈W such that |X|≥3 and the members of X are collectively indistinguishable from w. $\mathfrak {S}$ is not strongly internally +closed.

Proof

Consider any v∈X. By Lemma 11, for every f∈S _W such that $f_{\langle W,I\rangle }\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{W}$, f(v) = v. So for every $\xi \in \text {fix}(\mathfrak {S},w)|\mathfrak {S},w$, ξ.v _{〈W, I〉} = v _{〈W, I〉}. If $\mathfrak {S}$ is strongly internally + closed, then $v_{\langle W,I\rangle }\in D^{\langle \rangle }_{w}$, contradicting the assumption that the members of X are collectively indistinguishable from w. So $\mathfrak {S}$ is not strongly internally + closed. □

6.7 Constraints of Internal Closure

Proposition 20 shows that strong internal + closure is implausibly restrictive. Can a similar argument be given against internal + closure? It is easy to see a structure $\mathfrak {S}$ satisfying the condition of Proposition 20 may be internally + closed. To adapt this proposition to internal + closure, the condition on $\mathfrak {S}$ has to be strengthened; the following is a natural way of doing so:

Proposition 21

Let $\mathfrak {S}=\langle W,I,D\rangle$ be a structure and X⊆W such that |X|≥4 and for all w∈W, the members of X∖{w} are collectively indistinguishable from w and $X_{\langle W,I\rangle }\in D^{\langle \rangle }_{w}$. $\mathfrak {S}$ is not internally +closed.

Proof

Assume for contradiction that $\mathfrak {S}$ is internally + closed, and consider any w∈W and v∈X∖{w}. Let $\xi =\langle f,g\rangle \in \text {fix}(\mathfrak {S},w)|\mathfrak {S}$; then there is a u∈W such that $f_{\langle W,I\rangle }\in D^{\langle \langle \rangle ,\langle \rangle \rangle }_{u}$. So by Lemma 11, f(x) = x for all x∈X∖{u}. Since $\xi \in \text {fix}(\mathfrak {S},w)$ and $X_{\langle W,I\rangle }\in D^{\langle \rangle }_{w}$, ξ.X _{〈W, I〉} = X _{〈W, I〉}, and so ξ.x = x for all x∈X. So in particular ξ.v _{〈W, I〉} = v _{〈W, I〉}. Thus with the assumption that $\mathfrak {S}$ is internally + closed, $v_{\langle W,I\rangle }\in D^{\langle \rangle }_{w}$, which contradicts the assumption that the members of X∖{w} are collectively indistinguishable from w. □

The structure $\mathfrak {S}^{4}$ used in the proof of Theorem 1 is a simple instance of this more general result. $\mathfrak {S}^{4}$ is a paradigmatic instance of the kind of structures with which higher-order contingentists motivate their views. One might therefore take these results to be signs of trouble for the Fine-Stalnaker view. But it is not obvious how to make this worry more concrete. In particular, it is not obvious how to adapt the concrete example used in Section 6.6 to the present case: plausibly, any three possible electrons are compossible, so the indistinguishability of possible electrons does not lead to the patterns of indistinguishability ruled out by Proposition 21. It is a interesting question whether there are any metaphysical arguments against the restrictions on patterns of indistinguishability imposed by internal + closure.

6.8 Impossible Representations of Permutations

The results of the previous two sections show that the difficulties with internal generation only get worse when we reformulate Comp _{F S} using quantification over (existing) permutations. Conversely, this suggests that we might solve some of these difficulties by replacing quantification over possible permutations by quantificational expressions which range in some sense also over certain impossible permutations.

One might think that in the formal language used here, it is impossible to express any impossible relations. In the relevant sense, this is mistaken: consider the formula □∀p ^〈〉□∀q ^〈〉◇∃r ^〈〉□((p∧q)↔r), which says that for any two possible propositions, it is possible for there to be a proposition necessarily equivalent to their conjunction. It is easily seen that this can fail in some models. Analogously, we might try to include impossible permutations in a reformulation of Comp _{F S} by piecing together incompossible relations. We don’t think that this option is promising: First, the natural way of trying to formalize quantification over different ways of piecing together various possible relations would be to use some kind of infinitary conjunction, where a way of piecing together relations is given by an open formula. The problem it that, no matter how big we allow such a conjunction to be, it must still fall within the scope of only finitely many modal operators, since formulas are well-founded – a point we discuss in detail in Part 3. Consequently, any impossible permutation we can talk about using modalized quantifiers would have to be pieced together from relations from finitely many worlds, which is probably not sufficient to validate Comp _{F S} . In effect, analogous difficulties to those brought out in Proposition 21 will still arise for models based on infinite sets X.

These considerations lend further support to the suspicion that the informal motivations behind the Fine-Stalnaker view can only be understood by adopting the viewpoint of the higher-order necessitist. One option is to conclude that these motivations must therefore be confused. But alternatively, one might also claim that this is simply how the view should be formulated. E.g., Fine [6] sketches a ‘suppositional calculus’ in which we can quantify over what there is on a given supposition. Such a calculus would allow us to quantify over the needed permutations by quantifying over permutations on the supposition of necessitism. We are skeptical about the intelligibility of the suppositional devices employed by Fine, but do think that if we can make sense of them, they allow us to formulate a version of the Fine-Stalnaker view which is adequately modeled by closed models.

7 Conclusion

We developed a general possible worlds model theory for higher-order contingentism and isolated several classes of models as candidates to model the Fine-Stalnaker view of higher-order contingentism. The class of closed models emerged as a natural variant of Fine’s development, and was supposed to model both the higher-order closure and qualitative generation versions of the view. It was rejected since it did not validate the formal statement of higher-order closure in the form of the object-language automorphism-theoretic comprehension principle Comp _{F S} .

The invalidity of Comp _{F S} motivated the move to internally closed and internally generated models. These were found to be incompatible with negative semantics, in which only existing entities can stand in relations. Even on a positive semantics, where this is not required, internal generation was found not to validate Comp _C . This left only internal closure on a positive semantics. Although this imposes strong constraints on higher-order contingency, it was not found to conflict with any uncontentious metaphysical assumptions.

Higher-order closure as modeled by internally closed models on a positive semantics stands up well to Williamson’s challenge of providing a unified explanation for Comp⁻ and Comp _C without validating Comp; it validates the first two principles without validating the third. Williamson [19, p. 287] does claim that any adequate higher-order modal logic must also validate a certain modalization of the claim that, for any complete order on a domain, any definable condition that has an upper bound in the domain has a least upper bound in the domain. While it is likely that the model construction Williamson presents in his Appendix 6.7 carries over to prove that this claim is invalid on internally closed models on a positive semantics, we simply see no reason for the higher-order contingentist to agree with Williamson’s judgement that such a principle ought to be validated in the first place.

This concludes Part 1, which was concerned with developing the most plausible versions of the Fine-Stalnaker view of higher-order contingency. Part 2 considers Stalnaker’s models of contingency in what propositions there are, as presented in Fritz [7], and compares them formally to the model theories explored here. Part 3 discusses the issue of expressive power on the Fine-Stalnaker view of higher-order contingentism. There, certain expressive limitations are established, which are used in an expressive power challenge for contingentism in Fritz and Goodman [9].