DRAFT The Information Management Framework Core Constructional Ontology The Foundation for the Top-Level Ontology of the Information Management Framework Version 1.91 DRAFT April 6, 2022 -- 1 of 91 -- DRAFT Contents Executive summary 4 Introduction 4 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Purpose . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Target Audience . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1 Context 5 2 Report overview 6 3 Project background 7 4 Constructional ontology 9 5 Core Constructional Ontology 10 6 Developing the Core Constructional Theory 11 7 Technical background 13 8 Core Constructional Theory: the formal language 14 8.1 Logical framework . . . . . . . . . . . . . . . . . . . . . . . . . . 14 8.2 Non-logical vocabulary . . . . . . . . . . . . . . . . . . . . . . . . 16 8.3 Conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 9 Core Constructional Theory: the axioms 19 9.1 Plural logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 9.2 Stages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 9.3 Initial stage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 9.4 What exists at stages . . . . . . . . . . . . . . . . . . . . . . . . . 24 9.5 What is and is not constructible . . . . . . . . . . . . . . . . . . 26 9.6 Generic constructor . . . . . . . . . . . . . . . . . . . . . . . . . . 27 9.7 Specialised constructors . . . . . . . . . . . . . . . . . . . . . . . 27 9.8 Classification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 9.9 Set constructor . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 9.10 Sum constructor . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 9.11 Left and right constructors . . . . . . . . . . . . . . . . . . . . . 34 9.12 Pair constructor . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 9.13 Union constructor . . . . . . . . . . . . . . . . . . . . . . . . . . 38 9.14 Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 9.15 Maximal extension of a stage . . . . . . . . . . . . . . . . . . . . 42 9.16 Induction on the construction of objects . . . . . . . . . . . . . . 43 2 -- 2 of 91 -- DRAFT 10 Derivation of set theory and mereology 43 10.1 Axioms of set theory . . . . . . . . . . . . . . . . . . . . . . . . . 43 10.2 Derivation of the axioms of set theory . . . . . . . . . . . . . . . 46 10.3 Axioms of mereology . . . . . . . . . . . . . . . . . . . . . . . . . 48 10.4 Derivation of the axioms of mereology . . . . . . . . . . . . . . . 49 11 Consistency of the Core Constructional Theory 50 12 Conclusion 51 A Notions 53 A.1 List of key types and identity criteria . . . . . . . . . . . . . . . . 53 A.2 Constraints on inputs . . . . . . . . . . . . . . . . . . . . . . . . 54 B Design choices 54 C Supporting the IMF’s selected TLOs 56 D CLAP background 58 E Constructing via CLAP profiles 61 E.1 Induction on the construction of Ks . . . . . . . . . . . . . . . . 62 E.2 From sufficient to necessary conditions for identity . . . . . . . . 63 E.3 An intended model of our construction . . . . . . . . . . . . . . . 66 E.4 Equivalent formulations of the extremal clause . . . . . . . . . . 67 E.5 Further investigations . . . . . . . . . . . . . . . . . . . . . . . . 71 F Proof of consistency of the Core Constructional Theory 71 G Axioms 77 G.1 Primary axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 G.2 Optional axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 H Future work 84 H.1 Short term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 H.2 Long term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 I Literature sources 85 I.1 Current situation with foundations . . . . . . . . . . . . . . . . . 85 I.2 History of constructional ontology . . . . . . . . . . . . . . . . . 86 I.3 Current work on constructional ontology . . . . . . . . . . . . . . 87 I.4 Other background work . . . . . . . . . . . . . . . . . . . . . . . 87 References 88 Acknowledgments 91 3 -- 3 of 91 -- DRAFT Executive summary West forthcoming describes the seven-circles approach that is being used to organise the development of the Information Management Framework. The focus of this report is on the seventh circle: the Core Constructional Ontology. An investigation (West 2020) recommended that the top-level ontology of the Information Management Framework be underpinned by rigorously established foundations. This report develops a constructional approach to ontology, the Core Constructional Ontology, that provides these foundations. The report describes the ontology and its motivation, and it provides its first formalisation, thereby giving the Core Constructional Ontology a rigorous foundation. The formalisation is proved to be consistent. With these in place, we have established the feasibility of formalising the foundation of the Information Management Framework’s top-level ontology and provided a base for the building of the top-level ontology. Future work will refine this formalisation. Introduction Background In 2017, the National Infrastructure Commission published “Data for the Pub- lic Good” (NIC 2017) which sets out a number of recommendations including the development of a UK National Digital Twin supported by an Information Management Framework of standards for sharing infrastructure data, under the guidance of a Digital Framework Task Group set up by the Centre for Digital Built Britain. Much work has been done following this, but in particular: • A vision of how society can benefit from a UK National Digital Twin is set out in “Flourishing Systems - Re-envisioning infrastructure as a platform for human flourishing” (Burgess et al. 2020). • The direction for the technical standards, guidance and common resources needed as part of the Information Management Framework is set out in “The pathway towards an Information Management Framework - A ‘Com- mons’ for Digital Built Britain” (Hetherington and West 2020). In particular the latter identified the need for: • A Foundation Data Model: a data model that provides the struc- ture and meaning of data incorporating a top-level ontology based on science and engineering principles, enabling it to be extended to support the broadest possible scope consistently. • A Reference Data Library: the classes and properties needed to enable different organizations and sectors to describe things consistently. 4 -- 4 of 91 -- DRAFT • An Integration Architecture: the technical means, including open source software, for sharing data securely with authorised users. It also set out an outline approach and plan to develop the Information Man- agement Framework. Purpose The purpose of this report is to give an understanding of the technicalities of the foundation and formalisation underpinning the Information Management Framework’s ontology. Target Audience This report is directed at a technical audience interested in understanding what the foundation of the Information Management Framework’s ontology is and how it is formalised. In particular, we expect the report to be of interest to logicians and formal ontologists. 1 Context The National Infrastructure Commission’s report “Data for the Public Good” (NIC 2017) recommended the creation of a National Digital Twin (NDT) con- necting digital twins across different sectors to give a system of systems view of national infrastructure. As emphasised in reports such as Burgess et al. 2020, this harnessing of the power of information and data will deliver better decisions which lead to better outcomes for people and society. The NDT is supported by an Information Management Framework (IMF) that includes a Foundation Data Model (FDM) as a key component (Hether- ington and West 2020). An investigation (West 2020) recommended that the FDM seed be founded on a top-level ontology based on the four 4-dimensionalist top-level ontologies (TLOs) that it had been determined best met the technical requirements of the FDM, underpinned by rigorously established foundations. Existing TLOs, including those selected as a starting point for the FDM, are typically assembled from disconnected core components. In the case of the selected TLOs, such components correspond to sets, parts (mereological sums), and relations, which were not built and formalised in a single, unified way. Previous work (De Cesare and Partridge 2016; Partridge, Cesare, et al. 2017; Partridge, Mitchell, Loneragan, et al. 2019; Partridge, Mitchell, Loneragan, et al. manuscript) has investigated how the selected TLOs could be unified based on a constructional framework developed by the philosopher and logician Kit Fine. Here we develop this novel approach, formally refactoring the disconnected core components into a unified theory. Using this unified theory to underpin the IMF’s TLO will significantly simplify and strengthen it, as well as providing a firmer foundation for future development. 5 -- 5 of 91 -- DRAFT The National Digital Twin programme (NDTp) set up a project to build this unified ontology, called the Core Constructional Ontology (CCO). This stage of the project has developed a transitional framework that establishes the feasibility of building the CCO. The framework is formalised by means of a theory we call the Core Constructional Theory (CCT). Here we describes the CCT and its associated CCO. Later stages of the project will further develop and enhance this framework. Appendix E.5 gives some indication of what these enhancements could be. This novel theory develops the idea that all the objects in the CCO emerge during construction. We start from an initial collection of objects—often called givens—and a small number of constructors, and the entire ontology unfolds from repeated constructions. So from the givens and constructors one knows, in principle, all the objects in the ontology. Using the technical resources of plural logic, the CCT formalises the arrangement of constructions in stages, where the intended ontology arises after exhausting all the stages. This report documents the CCT and provides a proof of its consistency. 2 Report overview The report broadly divides into two parts. The first part is introductory and is accessible to non-specialist readers. The second part is more technical, as it describes the details of the formalisation. There are also various appendices. The first, introductory part comprises five sections. • Section 3 (Project background) provides the context for our project, its connection to the IMF, and its relation to TLOs. • Section 4 (Constructional ontology) introduces the idea of constructional ontology. • Section 5 (Core Constructional Ontology) describes the main features and benefits of the CCO, our own constructional approach. • Section 6 (Developing the Core Constructional Theory) develops the basic framework for our formalisation of the CCO. • Section 7 (Technical background) explains the level of specialist knowledge presupposed by different sections of the report. It also provides references for readers interested in acquiring the appropriate background for the relevant sections. The second, more technical part also comprises four sections. • Section 8 (Core Constructional Theory: the formal language) introduces the formal language in which the axioms of our theory will be formulated. • Section 9 (Core Constructional Theory: the axioms) presents and explains the axioms of the CCT. 6 -- 6 of 91 -- DRAFT • Section 10 (Derivation of set theory and mereology) shows how set theory and mereology can be recovered from the CCT. • Section 11 (Consistency of the Core Constructional Theory) provides the context for our proof of consistency of the CCT. The main body of the report refers to appendices that contain a variety of supporting material. The key ones are: • an explanation of the design choices we have made and their motivations (Appendix B, Design choices); • a mathematical investigation of the inductive features of construction (Ap- pendix E, Constructing via CLAP profiles); • a proof of consistency for the CCT (Appendix F, Proof of consistency of the Core Constructional Theory); • a description of future work (Appendix H, Future work). In this report, we aim to use consistently technical terminology that either follows standard mathematical and philosophical usage or reflects usage in the survey Partridge, Mitchell, Cook, et al. 2020 and in relevant TLOs. For example, we will consistently write about ‘elements’ of sets and ‘members’ of pluralities, though these are used interchangeably in the literature. 3 Project background The UK has initiated a programme to build a National Digital Twin: the Na- tional Digital Twin programme (NIC 2017 and Bolton et al. 2018). Hethering- ton and West 2020 recommends the adoption of an Information Management Framework that includes a Foundation Data Model (FDM) as a key compo- nent. West forthcoming describes the seven-circles approach that is being used to organise the development of the Information Management Framework (see Figure 1). The present report is part of the output of the Information Manage- ment Framework. Its focus is on the last, seventh circle: the Core Constructional Ontology. It was proposed that the FDM be built on a TLO (Hetherington and West 2020). West 2020 determined that four selected 4-dimensionalist TLOs—the tar- get TLOs—best met the technical requirements of the FDM. It recommended that these target TLOs should be underpinned by rigorously established foun- dations. The formalisation in this report provides the rigorous foundations for these target TLOs. The NDTp has carried out a comprehensive survey of available TLOs (Par- tridge, Mitchell, Cook, et al. 2020), which also develops a framework for as- sessing ontologies, including TLOs. One dimension of this assessment, called “the vertical aspect”, concerns the formal structure of the “core of basic on- tological hierarchical relations that are typically found in top-level ontologies; 7 -- 7 of 91 -- DRAFT Information Operations Process Model based information Requirements Integration Architecture Industry Data Models & Reference Data Foundation Data Model Top Level Ontology Core Constructional Ontology Figure 1: Information Management Framework: seven-circles approach whole-part, type-instance and super-sub-type [...]. [I]n practice these hierar- chies are a key part of the backbone of the ontological architecture” (Section 4.2.1). In the target TLOs, these are: whole-part, type-instance, tuple-place, and super-sub-type. As noted in this survey, TLOs tend to use a number of well-known formali- sations for the core hierarchical relations in the vertical aspect. The whole-part hierarchy is usually formalised using General Extensional Mereology (GEM), also known as Classical Extensional Mereology (see Varzi 2019 and Partridge, Mitchell, Cook, et al. 2020, Section 4.3.2). The target TLOs follow this ap- proach. Some TLOs, including the target TLOs, adopt an extensional criterion of identity for types, that is, sets (described in Partridge, Mitchell, Cook, et al. 2020, Section 4.3.6). In these TLOs, the type-instance hierarchy is often for- malised using a version of set theory that includes urelements and is also used to formalise the super-sub-type hierarchy. However, these TLOs adopt mereology and set theory as separate formal theories, without an integrated development of the two. As Section 4.2.1 of the survey notes, the basic ontological hierarchical rela- tions may be viewed as belonging to a single family and so should have similar formalisations. We remarked above on previous work that included initial in- vestigations of this suggestion for the target TLOs. These investigations started to develop, but not yet formalise, the unified constructional approach sketched by Fine (most prominently in Fine 1991 and Fine 1999). The investigations 8 -- 8 of 91 -- DRAFT also noted that, for the unified approach, three basic forms of construction are required: one for sets, one for sums, and another for tuples, with an additional, derived constructor for subsets. Our project was tasked with building upon this initial investigation to pro- duce a unified formalisation of the core hierarchies required for the target TLOs. In particular, it was tasked with proving the consistency of the resulting for- malisation. 4 Constructional ontology In this section, we provide more context about the conception of ontology un- derlying our project, namely, constructional ontology. On this conception of ontology, one starts with some constructors and some givens. Then new ob- jects emerge by construction, that is, from the application of constructors to objects. So the resulting ontology can be characterised by three parameters: the givens with which one starts, the constructors one employs, and the objects that emerge from applications of the constructors. Among the latter, we allow both constructed objects—the direct outputs of the construction—and traces of the construction process itself. (More details are given in later sections) Two features of constructional ontology are worth highlighting here. First, it gives us a very clear picture of the overall contents of the ontology, including a comprehensive view of the categories of objects. For example, if the ontology includes only a set constructor, then all the objects in the ontology fall under one of these three kinds: givens, sets, and traces of the construction process. We start with the givens. Then sets and associated traces arise from repeated appli- cations of the set constructor. In short, a constructor determines the category of the objects it generates. Second, identity criteria emerge from the constructional process: the iden- tity of constructed objects is dictated by their constructors and the inputs of the constructions. For examples, two sets (i.e. objects obtained from the set constructor) are identical if and only if they are constructed from the same ob- jects. In short, a constructor determines the identity of the objects it generates as well as their category. Constructional ontology has a long and venerable history (see Appendix I.2 for basic references). Of special importance for our project is Kurt G¨odel’s articulation of “the concept of set [...] according to which a set is anything obtainable from the integers (or some other well-defined objects) by iterated application of the operation ‘set of’ [...]” (G¨odel 1964, p. 180). Here G¨odel is referring to a broadly constructional concept of set: sets are generated by applications of the set constructor. More recent work on constructional ontology includes that of Kit Fine, who has significant influence on this project. We build on a number of his ideas for developing a unified constructional ontology. 9 -- 9 of 91 -- DRAFT 5 Core Constructional Ontology As we have mentioned, a constructional ontology can be characterised by three parameters: the givens with which one starts, the constructors one employs, and the constructed objects that emerge from applications of the constructors. We begin to develop our approach, the CCO, by specifying these parameters. The CCO assumes that the givens are the spatiotemporal atomic elements of all possible worlds—sometimes called the pluriverse. In other words, these atoms “cover” the pluriverse. The theory developed in this report, the CCT, has a more flexible structure: the choices of givens is left open. More specifically, the CCT only requires a minimal collection of givens: those that are necessary to characterise the construction process (see Section 9.3). This simplifies the task of formalisation, where such a minimal collection is used. But the theory is consistent with stronger assumptions about the givens in the CCO and can be adapted straightforwardly to other settings. Our approach involves a single, generic pattern for constructors, which we specialise into three key constructors: set, sum, and ordered pair. This speciali- sation involves characterising the conditions under which these constructors can be applied. From these emerge the key categories of constructed objects: sets, sums, and ordered pairs. (Hereafter we refer to ordered pairs simply as pairs, since unordered pairs do not play any important role in this context.) Note that, as new objects emerge, more possibilities for construction become available. For example, once two sets a and b have been constructed, we can construct their singletons or the set that has just these two objects as elements. We generate the target ontology after we exhaust all possible constructions based on the generic constructor. In the remainder of this section, we focus on three features of our approach and explain their benefits for our project: the approach is foundational, it has a high degree of unification, and it is constructional in the sense introduced above. Our ontology has three characteristics that enable it to play a foundational role. The first is its categorical completeness. That is, the ontology provides the three basic categories of objects for the target TLOs: sets, sums, and tuples, together with their associated hierarchical relations (type-instance, super-sub- type, whole-part, and tuple-place). The second characteristic is object com- pleteness. That is, the ontology generates all the objects needed by the target TLOs. One might think of it as an “object factory” which supplies the objects that might be needed in any domain. The third characteristic is that the ba- sic categories provide objects in the ontology with appropriate identity criteria. These are broadly extensional, based on the type of constructor and its input. For example, two sets are identical if and only if they are constructed from the same objects. Similarly, two sums are identical if and only if they have the same parts. Our approach is unified in the following ways. First, it gives a common development of three key domains: sets, sums, and tuples. Ontologies that in- 10 -- 10 of 91 -- DRAFT volve sets and sum usually adopt set theory and mereology as separate theories, without an integrated development. Here we provide a unified treatment of sets, sums and pairs (hence tuples) as sui generis objects. So the three target domains—sets, sums, and tuples—arise in similar ways through construction. Second, there is a common basis for identity criteria, which are crucial for the foundational role discussed above. Identity criteria for the objects of the ba- sic types are extensional, with differences arising from the way the objects are constructed. Third, the approach offers uniform ways of capturing key com- monalities and differences among objects of the basic types. Such commonalities and differences are captured by features of the underlying constructors. In the previous section, we outlined the basic structure of a constructional ontology. We now want to highlight four of its main benefits. • Categorical differences are constructional differences: in constructional approaches, different kinds of objects can be distinguished from one an- other by the manner in which they are constructed. So categorical differ- ences are explained by constructional differences. • Dependency: some objects are built from others and hence “depend on” them. This provides an explanation of ontological dependence and the associated notion of grounding. • Reduction: the ontology is built out of a relatively small set of initial objects and thus achieves fundamental ontological parsimony in the sense of Schaffer 2015. • Consistency: construction can be a basis for consistency, avoiding para- doxes such as those of Russell and Burali-Forti, although we need to take care with the construction process. In our case, this is achieved by requir- ing that the construction be “bottom-up” in the sense that the properties of the constructed objects are determined by the properties of the inputs to the construction. G¨odel stresses this last benefit in the article cited above. Speaking of the constructional view of sets, he says: [It] has never led to any antinomy whatsoever; that is, the perfectly ‘na¨ıve’ and uncritical working with this concept of set has so far proved completely self-consistent. (G¨odel 1964, p. 180) In this report, we show that our approach can be developed consistently. We do so by providing a mathematical proof of consistency for the associated for- malisation. 6 Developing the Core Constructional Theory The project was tasked with developing the CCT, a formalisation of the CCO. The first decision concerned what kind of constructional framework to adopt. It 11 -- 11 of 91 -- DRAFT was essential to demonstrate that this innovative approach would work, so we decided to go with the established, and thus safe, option of adopting a stage- theoretic framework (described below). This framework is well-developed for set theory but needed to be extended to sums and tuples. We also recognised that plurals have a natural role in representing the multiplicity of the input to our constructors. (For example, it is far more natural to describe the set {a, b} as constructed from the elements a and b than from any single entity representing both a and b.) These things together provided us with the overall framework for our formalisation. Our formalisation takes its inspiration from the influential iterative concep- tion of sets, which goes back to G¨odel’s article cited earlier: “What is Cantor’s Continuum Problem?” (1964). According to this conception, the sets are formed in stages. We start, at stage 0, with some urelements. At stage 1, we form all sets of urelements, which results in a larger domain. At stage 2, we form all sets of objects from this larger domain. We continue into the infinite. At limit stages, such as the first infinite stage ω, we collect the previously formed sets, which are then used to form new sets at the next stage ω + 1. The most famous development of the iterative conception of sets is due to George Boolos (Boolos 1971), who develops a stage theory—an axiomatic theory that describes how sets are successively formed at stages. We generalise and extend Boolos’s stage theory in three different ways. First, instead of considering just the construction (or “formation”) of sets, we adopt Fine’s framework and offer a unified account of three different kinds of con- struction that are central to the target TLOs: sets, mereological sums, and pairs. This enables us to capture the core hierarchical relations of the target TLOs mentioned earlier, namely, type-instance, super-sub-type, whole-part, and tuple-place. We do not rely on a set-theoretic representation of pairs. Rather, we treat pairs as a category of constructed objects, distinct from that of sets. Our generic pattern for constructors relies on plural logic, which does not allow for order. So we reconstruct paired objects by means of special constructed ob- jects marked by positions—we call them “position objects”. For pairs, we need two positions, so we introduce two categories of position objects. To emphasize that there is no assumed order, we call these “left objects” and “right objects” (we could have used a different naming convention, such as “red objects” and “blue objects”). These objects are built by the corresponding constructors: the left constructor and the right constructor. For example, suppose that we want to construct the pair of a and b. We first construct from a and b two position objects a′ and b′, obtained respectively by applying the left constructor to a and the right constructor to b. Then we apply the pair constructor to a′ and b′, which yields the desired pair. Second, we do not require that all objects that can be constructed at a stage are constructed at that stage. This enables us to realise separately construc- tional possibilities that are independent of each other. Third, the target ontologies involve traces, special objects that “log” the structure of the construction process. These characterise how the objects are constructed. For example, suppose a set is constructed at a certain stage. Then 12 -- 12 of 91 -- DRAFT this stage also includes a trace for each element of the set constructed. These traces log the element’s view of the construction: the element itself, the type of construction (set), and the output (the set constructed). For example, if the set constructed is {a, b}, there will be two related traces, one recording that a has been used as input in the construction of a set with output {a, b}, the other recording that b has been similarly used. More details are provided in Section 9.14. We describe the process of construction in stage-theoretic terms. The process consists of stages ordered by E, which may be seen as an accessibility relation in the sense of relational semantics. We think of s E t quasi-temporally and therefore often pronounce it “s precedes t” or “t is after s”. The accessibility relation is reflexive. So the intended sense of “s precedes t” is “s precedes t or s is equal to t”. Every object in the target TLOs is introduced at some stage. We write x@s for “x exists at s”. Some objects exist at an initial stage—these are the givens. Once an object exists, it continues to exist at all later stages. However, as we move from earlier to later stages, new objects might be constructed and thus might begin to exist. In the investigation of the target TLOs, this process is called ontogenesis as, intuitively, after all the stages all the objects in the ontology exist. In describing the CCT, we tend to use a dynamic language. This makes the structure of construction easier to visualise, and it exposes relations of ontolog- ical dependence among objects (see Section 5). However, the resulting domain is not literally dynamic. It encompasses the objects that exist as a result of the entire process. The same is true of Boolos’s stage theory for the iterative conception of set. While his theory describes a seemingly dynamic process of generation, the domain of the theory is not dynamic. It encompasses all sets and results from the entire process. All construction is effected by means of constructors. A constructor is ap- plied to appropriate objects that exist at some stage so as to construct another object, which may exist only at a later stage. In Appendix B, we provide details about the design choices that inform our approach. 7 Technical background We aim to make this report, as far as possible, accessible to non-specialist readers, without additional readings. For readers interested in deepening their understanding, appropriate references have been given in the preceding sections. However, the development of the formalisation and the proof of consistency of CCT in the succeeding sections have to rely on specialist and sometimes highly technical notions from logic and mathematics. So these sections of the report are more demanding and require a degree of specialist knowledge. Section 8 presupposes a basic knowledge of first-order logic. The appropriate background information can be found in logic textbooks such as Enderton 2001 and Hodges 1977. Building on this knowledge, readers should be able to follow 13 -- 13 of 91 -- DRAFT reasonably well the presentation of plural logic in this report. The presentation is self-contained, though interested readers can find a more detailed discussion of plural logic in Florio and Linnebo 2018 and Florio and Linnebo 2021. The formulation of the CCT in Section 9 is based on, and hence presupposes, the logical framework introduced in Section 8. While no additional knowledge is strictly required to appreciate the formalisation, the context of some parts of the theory (e.g. the axioms of Infinity and Replacement) will be clearer to readers with basic knowledge of set theory (see, for example, Enderton 1977). The most technical sections of the report—Section 11, Appendix E, and Appendix F—use advanced notions from set theory and model theory. Expla- nations of the required notions can be found in Kunen 1980 and Chang and Keisler 1990. To accommodate non-specialist readers, we add informal glosses to the for- mal statements of the axioms. Moreover, where we make comments, we divide these into more accessible notes and technical remarks. To further help non- specialist readers, we supply in Appendix I an organised list of background literature. 8 Core Constructional Theory: the formal lan- guage In this section, we introduce the formal language in which the axioms of the CCT will be formulated (for the axioms, see Section 9). The language is given by the logical framework (plural logic) and some non-logical vocabulary. The non- logical vocabulary includes expressions for the key constructional operations and for auxiliary vocabulary needed to express the way in which the constructional operations are deployed through the stages. 8.1 Logical framework As a logical framework for the CCT, we use plural logic, specifically what is known in the philosophical literature as PFO+, which is short for plural first- order logic plus plural predicates. This is the standard language for the for- malisation of plural logic, though there are some differences in notation among authors that use this system. Our exposition of the system relies on Florio and Linnebo 2021. The language of PFO+ extends the language of first-order logic with the following classes of expressions: A. Plural terms: plural variables (vv, xx, yy, . . ., and variously indexed vari- ants thereof) and plural constants (aa, bb, . . ., and variants thereof), roughly corresponding to the natural language pronoun ‘they’ and to plu- ral proper names (e.g. ‘The Hebrides’), respectively. 14 -- 14 of 91 -- DRAFT B. Universal and existential quantifiers that bind plural variables (e.g. ∀xx, ∃yy, . . . ). We may read ‘∀xx’ as ‘whenever there are some things xx, then . . . ’, and we may read ‘∃yy’ as ‘there are some things yy such that. . . ’. C. The binary predicate ≺ for plural membership, corresponding to the nat- ural language ‘is one of’ or ‘is among’. Its first argument place is singular, while the second is plural (e.g. ‘x ≺ xx’). So the predicate expresses a relation between an object and some objects. The intended reading of ‘x ≺ xx’ is ‘x is one of xx’, which may be pronounced “x is one of the xs”. For example, ‘s ≺ hh’ may be used to represent ‘Skye is one of the Hebrides’. D. Plural predicates, defined as predicates with one or more argument places reserved for plural terms. An example is Construct(z, xx, y), which represents that z is constructed from xx using the constructor type y. The predicate’s arity can be represented by numerical superscripts, which may be omitted for economy, as in the preceding example. The full predicate is Construct3(z, xx, y). The non-logical vocabulary of the language, which includes first-order and plural predicates (class D above), is discussed in the next section. We define a well-formed formula in the language of PFO+ starting with atomic formulas. These are formed by combining predicates with the appropri- ate number of terms. As noted earlier, we need to ensure that argument places reserved for terms of a certain kind (singular or plural) are occupied by terms of that kind. More complex formulas are obtained by means of sentential con- nectives and variable binding using singular or plural quantifiers. (See Florio and Linnebo 2021 for details.) We should emphasize that plural predicates in this language are read collec- tively. Collective readings of plural predicates contrast with distributive read- ings. To appreciate the distinction, consider a natural language predicate such as ‘lifted a box’. The sentence ‘Annie and Bonnie lifted a box’ can mean that Annie and Bonnie lifted a box together (collective reading), or it can mean that Annie and Bonnie lifted a box individually (distributive reading). So a predicate in our formal language such as Construct(z, xx, y) has a collective reading: it means that z is constructed collectively from xx using the constructor type y. This choice of interpretation for the plural predicates does not make PFO+ any less expressive, since the effect of distributive predication can be obtained by paraphrase. For example, suppose we want to say that xx are sets, which has only a distributive reading, i.e. each of xx is a set. Then, using the singular predicate IsSet(x), we can express that xx are sets by saying that everything that is one of xx is a set: ∀x(x ≺ xx → IsSet(x)) To illustrate the use of PFO+, it might be helpful to provide some examples of formulas together with informal glosses. For intuitiveness and simplicity, our 15 -- 15 of 91 -- DRAFT informal glosses will often render plural expressions in terms of “pluralities” and their members. • v ≺ vv (v is one of vv, i.e. it is one of them.) • AreSeven(aa) (aa are seven.) • IsBox(b) ∧ ∃xx(∀x(x ≺ xx ↔ IsTile(x) ∧ IsIn(x, b)) ∧ Weigh8kg(xx)) (The tiles in box b weigh 8 kg together. Literally, b is a box and there are some things such that anything is one of them if and only if it is a tile in b and, together, they weigh 8 kg.) • ∃z∃xx∃yConstruct(z, xx, y) (Some object is constructed from some things using some type of constructor.) • ∃zz∀z(z ≺ zz ↔ (z = a ∨ z = b)) (Consider two objects a and b, possibly identical. There is a plurality that has a and b, and only a and b, as its members. If a = b, then this is a “singleton” plurality.) • ∀z∀xx∀y(Construct(z, xx, y) → ∀ww(∀w(w ≺ xx ↔ w ≺ ww) → Construct(z, ww, y))) (If an object of some type is constructed from a plurality xx, then it is also constructed by any plurality ww that has exactly the same members as xx.) 8.2 Non-logical vocabulary We have designed the language of the CCT so that its basic non-logical vo- cabulary can express the constructional operations in scope, the structure of the stages, and the way in which operations and stages interact to produce the target ontology. This vocabulary is given by constants, first-order predicates, and plural predicates of kind D mentioned above. The present version of the CCT includes a single, generic constructor, which we express here as a three-place predicate rather than an operator. Given our requirements for formalisation, this is the simpler choice: it makes working in classical logic unproblematic, as we avoid the need to handle empty terms and partial functions. Different types of constructed object can be obtained by switching one of its parameters. The switch is effected using special constants, one for each type of constructed objects. 16 -- 16 of 91 -- DRAFT Generic constructor predicate intended reading Construct(z, xx, y) z is an/the object constructed from xx using the type y The predicate has three argument places. The first is associated to the object constructed, while the other two are associated to the inputs of the construction (a plurality of objects) and an object representing the type of construction effected. To indicate the types of construction, we use six special constants. Types constant intended reading cset set construction type csum sum construction type cleft left position construction type cright right position construction type cpair pair construction type cunion union construction type For example, we describe the construction of a set by filling the third argu- ment place of Construct(z : xx, y) with the constant for the desired type of construction: Construct(z : xx, cset). Next, we have some predicates pertaining to stages and their structure. Stages predicate intended reading Stage(x) x is a stage E(s, t) s is before, or equal to, t @(x, s) x exists at (stage) s The process of construction involves the application of the generic construc- tor to some objects and the specification of the type of construction to be ef- fected. Since we require pluralities to be non-empty (see Section 9), we thereby 17 -- 17 of 91 -- DRAFT disallow empty inputs to any constructor. Moreover, one can refine this pro- cess by placing constraints—in accordance with the target TLOs—upon what objects can serve as inputs relative to particular types. In the case of the set constructor, for example, all objects other than position objects can serve as inputs and thus are (informally) “settable”. In the case of mereological sums, the CCT restricts the process of construction to individuals, namely, objects that are either givens or sums. Only individuals are “summable”. The notion of “individual” is expressed by a primitive predicate. Individuals predicate intended reading Individual(x) x is either a given or a sum As mentioned above, the target ontology involves traces, namely, objects that log the structure of the construction process. The components of this structure are accessed by three predicates listed below. More details about these predi- cates and their role is provided in Section 9.14. Traces predicate intended reading HasOutput(w, z) w records a construction with output z HasInput(w, x) w records a construction with x as one of the inputs HasType(w, y) w records a construction of type y This completes our basic stock of primitive non-logical vocabulary. We will make frequent use of definitions to introduce new notions. To facilitate the automated translation of the formalisation into computer-readable format, we treat these definitions as axioms rather than abbreviations. As a result, these definitions introduce new primitive non-logical expressions relying on non-logical expressions from the basic stock as well as prior definitions. 8.3 Conventions To simplify the exposition of the CCT, we rely on a number of familiar conven- tions. Let us highlight some key examples. First, we adopt the following formatting conventions. • When parentheses are omitted, ambiguities should be resolved by applying the standard rules of precedence among logical connectives. 18 -- 18 of 91 -- DRAFT • Different styles of parentheses are used to make groupings of formulas easier to recognize. • A leading block of universal quantifiers is frequently omitted. So axioms with free variables, i.e. variables not bound by a quantifier, are short for their universal closure. • To improve readability, we use infix notation for some predicates. For example, we write ‘s E t’ rather than ‘E(s, t)’, and ‘x@t’ rather than ‘@(x, t). Secondly, we adopt a convention related to restricted quantification. • Quantification restricted to certain kinds of entities may be marked by the use of particular variables. We use s, s′, s0, t, etc. to range over stages. So ∀sϕ(s) is short for ∀s(Stage(s) → ϕ(s)). Similarly, we use ss, ss′, tt for plural quantification over stages. So ∀ssϕ(ss) is short for ∀ss(∀x(x ≺ ss → Stage(x)) → ϕ(ss)). Finally, we use the following, less common formatting convention in order to emphasize constructional links among argument places of relevant predicates. • We use a colon rather than a comma to separate the argument place for the constructed object from the rest of the arguments. For example, we write Construct(z : xx, y) rather than Construct(z, xx, y) to indicate that z is constructed from xx and y. 9 Core Constructional Theory: the axioms Our theory has several parts, with different concerns. The axiomatisation aims to be perspicuous, user-friendly, and modular rather than minimal. It is based on the language introduced in the preceding section. 9.1 Plural logic The formal system PFO+, which we introduced in Section 8.1, comes equipped with logical axioms and rules of inference. The axioms and rules associated with the logical vocabulary of ordinary first-order logic are the standard ones. For example, one could rely on introduction and elimination rules for each logical expression. The plural quantifiers are governed by axioms or rules analogous to those governing the first-order quantifiers. In addition, we have the following axioms or axiom schemes. First, every plurality is non-empty: (A1) ∀xx∃y y ≺ xx (Every plurality has at least one member.) Then, there is an axiom scheme of indiscernibility: 19 -- 19 of 91 -- DRAFT (A2) ∀xx∀yy(∀z(z ≺ xx ↔ z ≺ yy) → (ϕ(xx) ↔ ϕ(yy))) (Coextensive pluralities satisfy the same formulas.) Some remarks are in order. First, the formula ϕ may contain parameters. So we have the universal closure of each instance of the displayed axiom scheme. Second, as is customary, we write ϕ(xx) for the result of replacing all free occurrences of some designated plural variable vv with ‘xx’ whenever ‘xx’ is substitutable for vv in ϕ (see, for example, Enderton 1977, p. 113). Third, (A2) is a plural analogue of Leibniz’s law of the indiscernibility of identicals, and as such, the scheme needs to be restricted to formulas ϕ(xx) that don’t set up intensional contexts. Since there is no requirement for intensional contexts in the CCO, no such context will be introduced in the CCT. Thus, the axiom scheme may be used unrestrictedly in the present setting. Finally, there is the unrestricted axiom scheme of plural comprehension, an intuitive principle that provides information about what pluralities there are. For any formula ϕ(x) in which x is free but xx is not, we have an axiom stating that if ϕ(x) is satisfied by at least one thing, then there are the things each of which satisfies ϕ(x): (A3) ∃xϕ(x) → ∃xx∀x(x ≺ xx ↔ ϕ(x)) (If something is ϕ, then there are some things that are all and only the ϕs. That is, if something is ϕ, then the ϕs exist.) We refer to an axiomatization of plural logic based on the principles just de- scribed as full plural logic. The fullness of the logic has to do with the fact that plural comprehension applies to any formula ϕ(x)—provided, as stated, that x but not xx occur free. Two important relations in plural logic are introduced as definitions. One is the many-many relation of plural inclusion (‘are among’), which is symbolized as ‘4’: (D1) xx 4 yy ↔ ∀z(z ≺ xx → z ≺ yy) (Some things xx are among yy when everything that is one of xx is one of yy.) Another important relation is plural identity, symbolized as ‘≈’. The relation can be defined using ‘4’, the symbol introduced by the preceding definition: (D2) xx ≈ yy ↔ (xx 4 yy ∧ yy 4 xx) (Two pluralities xx and yy are identical if and only if xx are among yy and yy are among xx, i.e. xx and yy have the same members.) When showing how to derive the axioms of set theory from the CCT (Sec- tion 10.2), we will mention another principle of plural logic, one that corresponds to the Axiom of Choice in set theory. Informally, the plural principle states that 20 -- 20 of 91 -- DRAFT for every plurality pp representing a family of pairwise disjoint pluralities of ob- jects, there is a choice plurality for pp. This is a plurality containing a unique member for any plurality in the family represented by pp. (See Section 10.2 for more details.) We do not adopt this plural principle as an official axiom of CCT. Rather, we leave it as an option available in contexts where the set-theoretic Axiom of Choice is needed. 9.2 Stages The stages are linearly ordered by the accessibility relation E: (A4) ∀s s E s (E is reflexive.) (A5) ∀s∀t(s E t ∧ t E s → s = t) (E is antisymmetric.) (A6) ∀s0∀s1∀s2(s0 E s1 ∧ s1 E s2 → s0 E s2) (E is transitive.) (A7) ∀s∀t(s E t ∨ t E s) (E is connected.) In addition, stages are well-founded by E. Let us define s C t (“s is strictly before t”) as follows: (D3) s C t ↔ (s E t ∧ s 6 = t) Then, we have: (A8) ∀ss∃s(s ≺ ss ∧ ¬∃t(t ≺ ss ∧ t C s)) (The stages are well-founded by E. That is, for any plurality ss of stages, there is a member s that is first among ss with respect to the order E.) Notice that the last axiom makes essential use of plural logic, asserting some- thing of every plurality of stages. Moreover, this axiom enables us to do well- founded induction on E. (Assume that a property holds at the initial stage and that, whenever the property holds at every s such that s C t, then it also holds at t. Then the property holds at every stage.) Using this form of induction, we will be able to show, for example, that something exists at every stage. The accessibility relation is also serial: (A9) ∀s∃t s C t (For every stage, there is a strictly later stage.) We say that t is a successor stage of s if and only if s precedes t and there is no stage strictly in between s and t, that is: 21 -- 21 of 91 -- DRAFT (D4) Succ(s, t) ↔ s C t ∧ ¬∃u (s C u ∧ u C t) Later we will introduce a related abbreviation, a predicate ‘Max(s, t)’ repre- senting that t is a maximal extension of s, that is, that t contains the result of carrying out every construction that is possible at s (Section 9.15). Remark. Axiom (A9) and the well-foundedness of E entail that every stage has a successor stage. Remark. We will eventually see that the seriality of E can be proved from the other axioms of our theory (see Section 9.9). We keep the axiom of seriality, however, as we will sometimes be interested in working with less than the full theory. There is an infinite stage: (A10) ∃t(∃s s C t ∧ ∀s(s C t → ∃u(s C u ∧ u C t))) (There is a stage that is after some stage and is not immediately after any other stage.) Note. To see how this axiom secures an infinite stage, consider the finite stages 0, 1, 2, ... and the first infinite stage ω, which comes after all the finite stages. To say that a stage t is not immediately after any other stage means that, if there is a stage s before t, then there is a stage between s and t. Both 0 and ω are not immediately after any other stage. (In the case of 0, this condition is vacuously satisfied). However, unlike 0, ω is after some stage. So we can characterise ω as the first stage that is after some stage but is not immediately after any other stage. Remark. We can now prove that there is an initial stage. Axiom (A10) entails that there is a stage. Thus the plurality of stages exists and, given (A8), is well-founded. So there is a first stage. Let us say that some things exist at a stage if and only if each of them exists at that stage. So we define ‘xx@@s’ (“xx exist at s”) as follows: (D5) xx@@s ↔ ∀x(x ≺ xx → x@s) We also assume a stage-theoretic version of the axiom scheme of Replace- ment. This is a powerful principle, which provides information about how many stages there are. Specifically, the principle says there are so many stages that the objects available at any one of them do not suffice to reach arbitrarily high in the hierarchy of stages. That is, for any stage s, any objects xx at s, and any formula ψ(x, y) that represents a function from xx to objects throughout the hierarchy, there is a stage at which we find all the values that this function takes for arguments among xx. 22 -- 22 of 91 -- DRAFT (A11) xx@@s ∧ ∀x(x ≺ xx → ∃y(¬Stage(y) ∧ ∀z(ψ(x, z) ↔ y = z))) → ∃t∀x(x ≺ xx → ∀y(ψ(x, y) → y@t)) (Suppose that xx exist at s and that ψ(x, y) represents a function mapping objects among xx to objects other than stages. Then there is a stage t such that what exists at t includes the image under ψ of every member of xx.) This axiom is included primarily for the sake of re-construing set theory; it is not essential to our approach. Notice, though, that our Replacement axiom is not about sets but about stages and the many objects that exist at various stages. Indeed, Replacement is the first of our axioms that ties the existence of stages to the existence of objects that exist at stages, i.e. it is the first “interactive” axiom. 9.3 Initial stage An initial stage is one that is not preceded by any other stage. Let us define ‘Init(s)’ to mean that s is initial: (D6) Init(s) ↔ ¬∃t t C s Remark. It follows from the connectedness of E that s is initial if and only if it is before every other stage, i.e. ∀t s E t. This also means that there is at most one initial stage. In a different context, the current definition of initial stage would permit several alternative initial stages. We define an object to be a given if and only if it exists at some initial stage: (D7) Given(x) ↔ ∃s(Init(s) ∧ x@s) Then we assume the existence of some given: (A12) ∃x Given(x) (There is some given.) In our setting, we need objects that code information about types of con- struction. So we assume the existence of such objects. For example, we intro- duce an object cset that stands for the type set. We do the same for each type of construction in scope: sum, left object, right object, pair, and union. We make the pragmatic choice to treat these objects as givens and, in fact, as the only givens. In the future, we might want to separate these objects from those that more properly represent the intended constructional ontology. For this specific implementation of the CCT, and to allow modularity, we have the following strengthening of (A12): 23 -- 23 of 91 -- DRAFT (A13) Given(cset) ∧ Given(csum) ∧ Given(cleft) ∧ Given(cright) ∧ Given(cpair) ∧ Given(cunion) (The givens include: cset, csum, cleft cright, cpair, cunion.) These are six distinct givens: (A14) cset 6 = csum ∧ cset 6 = cleft ∧ cset 6 = cright ∧ cset 6 = cpair ∧ cset 6 = cunion ∧ csum 6 = cleft ∧ csum 6 = cright ∧ csum 6 = cpair ∧ csum 6 = cunion ∧ cleft 6 = cright ∧ cleft 6 = cpair ∧ cleft 6 = cunion ∧ cright 6 = cpair ∧ cright 6 = cunion ∧ cpair 6 = cunion It is convenient to have a separate predicate applying to these objects qua rep- resentations of types of construction: (D8) Type(y) ↔ (y = cset ∨ y = csum ∨ y = cleft ∨ y = cright ∨ y = cpair ∨ y = cunion) In section 9.13, we will see that the type union has a derived status, while the remaining types are basic. Remark. Our approach can be extended to other constructors one may wish to add. If new constructors are adopted, then the definition of Type(y) will have to be modified accordingly. However, as we will see, other axioms that utilise this predicate can remain unchanged, thus allowing a pleasing modularity. 9.4 What exists at stages Some of the previous axioms already provide information about what exists at stages. For example, stipulating the existence of some givens implies that they exist at the initial stage. Moreover, the axiom scheme of Replacement informs us that if some objects exist at a stage, their images under a functional relation also exist at some stage—provided only that no image is a stage. It is worth emphasising that while stages are part of the CCT, they are not part of the CCO. We use the term ‘object’ in two corresponding ways. In a wide sense, it stands for all entities in the domain of the CCT. In a narrow sense, it stands for relevant entities in the CCO and thus excludes stages. (So far we have used the term primarily in the narrow sense.) We now continue to explore principles that connect stages and what exists. First, we have an axiom that ties the objects in our ontology to stages, with the exception of the stages themselves, which are not part of the intended ontology and thus have a purely auxiliary role. (In future work, we will explore formalisations that do rely on stages as primitive.) (A15) ∀x(¬Stage(x) → ∃s x@s) (Everything that isn’t a stage exists at some stage.) 24 -- 24 of 91 -- DRAFT Note. We will be able to prove the other direction of the conditional in (A15) relying also on axioms introduced in later sections. So, in the CCT, something is not a stage if and only if it exists at some stage. We identify stages extensionally. That is, stages with identical domains are identical: (A16) ∀x(x@s ↔ x@t) → s = t (Stages with identical domains are identical.) Moreover, stages are “cumulative”: (A10) s E t ∧ x@s → x@t (When one stage precedes another, then everything that exists at the former also exists at the latter.) Define a stage t to be the least upper bound (LUB) of some stages ss in the usual way: (D9) LUB(t, ss) ↔ ∀s(s ≺ ss → s E t) ∧ ∀t′(∀s(s ≺ ss → s E t′) → t E t′) (According to the definition, t is the least upper bound of ss if and only if two conditions are met: (i) t is an upper bound of ss, i.e. t is after, or equal to, any stage in ss; (ii) t is the least among the upper bounds of ss, i.e. t is before, or equal to, any upper bound of ss.) Next, we have an axiom characterising “collection” stages. No new object is in- troduced at these stages; they merely collect objects existing at previous stages. Collection stages are useful when, as in our case, the construction process is extended into the transfinite and hence requires infinite stages. To see why, consider the first infinite stage ω, which comes after all finite stages. We cannot think of ω as introducing new objects constructed from those available at the preceding stage. This is because there is no stage that immediately precedes ω: any stage n prior to ω has a successor stage n + 1 that is also prior to ω. So what happens at stage ω? We adopt the option of simply letting ω collect the objects that exist at prior stages. The same applies to other infinite stages that are limit, namely, neither an initial stage nor a successor one. The following entails that limit stages are collection stages (and it provides trivial information about successor stages): (A17) LUB(t, ss) → ∀x(x@t → ∃s(s ≺ ss ∧ x@s)) (Suppose t is the least upper bound of some stages ss. Then everything that exists at t exists at some of ss.) Remark. The cumulativity of the stages entails the other direction, which means this conditional can be strengthened to a biconditional. We now want to define a predicate ConstrFrom(x, s) whose intuitive mean- ing is that x is constructed from some objects that exist at stage s. The precise definition is as follows: 25 -- 25 of 91 -- DRAFT (D10) ConstrFrom(x, s) ↔ ∃xx∃y(xx@@s∧Type(y)∧Construct(x : xx, y)) Finally, we restrict what can exist at a successor stage. This axiom also uses the notion of trace, which is characterised in Section 9.14. (A18) Succ(s, t) ∧ x@t → x@s ∨ ConstrFrom(x, s) ∨ Trace(x) (Everything that exists at a successor stage either existed at the predecessor stage, or is constructed from something at that stage, or is a trace.) Subsequent axioms will ensure the existence of appropriate traces at each suc- cessor stage. In particular, they will ensure that new traces emerging at a successor stage correspond to constructions effected at that stage. 9.5 What is and is not constructible We impose various constraints on which objects can serve as inputs to different types of construction. These constraints do not appear in the framework of Fine 2010. They are added here to reflect the constraints in the target TLOs and could easily be lifted in connection with the pursuit of other goals. In this section, we provide an informal characterisation of the constraints. Formal renderings of them will be developed in the later sections, where each type of construction is axiomatised. Let us recapitulate the overall structure of our ontology. We have five basic types of objects that can be constructed: set, sum, two types of position objects (left object and right object), and pair. One additional type of objects is derived: union. The construction process proceeds in stages, beginning with some givens. It yields objects of basic and derived types as well as traces storing information about the constructions effected. The construction of sets is the least constrained operation. Sets, sums, pairs, givens, and traces can all serve as inputs to constructions of sets or, as we may put it, are “settable”. Moreover, any plurality mixing objects of settable types is itself settable. By contrast, the construction of sums is the most constrained operation. Only individuals can serve as inputs, where an individual is defined as follows: (D11) Individual(x) ↔ (Given(x) ∨ ∃xx Construct(x : xx, csum)) (Any object is an individual if and only if it is either a given or a sum. ) Remark. The axioms of the CCT entail that sets, position objects, and pairs are