Core Constructional Ontology (CCO): a Constructional Theory of Parts, Sets, and Relations 4-Dimensionalism in Large Scale Data Sharing and Integration Newton Gateway to Mathematics -- 1 of 46 -- Top Level Ontology Foundation Data Model Industry Data Models - Reference Data Integration Architecture Process Model based Information Requirements Information Quality Management Core Constructional Ontology The Seven Circles of Information Management 2 -- 2 of 46 -- Main Authors Salvatore Florio Øystein Linnebo Martin Pleitz Information Quality Management Team effort Author Chris Partridge Contributors Kit Fine Paweł Garbacz Steven Kraines Liam McGee Andrew Mitchell Jan Sullivan Matthew West Integration 3 -- 3 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 1. Constructional ontology: background 2. Our approach 2.1 Key features of the approach 2.2 Overview of the formalisation Core Constructional Ontology Plan 4 -- 4 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Core Constructional Ontology Disclaimer § Reporting on the current state of our work § First attempt o MVP approach o We expect to improve and extend our approach in future work. § Feedback welcome! 5 -- 5 of 46 -- Constructional ontology: background 6 -- 6 of 46 -- Foundation Data Model Process Model based Information Requirements Constructional ontology: the basic idea 1. Start with some objects (“givens”) or even an empty domain. 2. Construct the rest of the ontology by applying selected constructors. 7 givens constructors constructed objects The ontology is characterized by: -- 7 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Core Constructional Ontology Constructional ontology: the basic idea (cont.) § Generally, the types of objects are determined by the constructors that generated the objects. § The identity of constructed objects is dictated by their constructors and the inputs of the constructions. 8 -- 8 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Gödel on a concept of set “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ödel, What is Cantor's continuum problem?) 9 -- 9 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Core Constructional Ontology Recent work The SWXd\ Rf OQWRORg\ KIT FINE U.C.L.A. A cRQVWUXcWiRQaO RQWRORg\ iV RQe Zhich VeUYeV WR cRQVWUXcW cRPSOe[eV fURP ViPSOe. The SUeVeQW SaSeU iV cRQceUQed ZiWh Whe QaWXUe aQd ZiWh Whe VWXd\ Rf VXch RQWRORgieV. IW aWWePSWV WR Va\, iQ Whe fiUVW SOace, hRZ Whe\ aUe cRQVWiWXWed aQd b\ ZhaW SUiQciSOeV Whe\ aUe gRYeUQed. BXW iW aOVR aWWePSWV WR Va\ hRZ WheiU VWXd\ Pa\ Oead RQe WR adRSW ceUWaiQ SRViWiRQV aQd WR PaNe ceUWaiQ defiQiWiRQV. The UePaUNV RQ Whe VWXd\ Rf RQWRORg\ aUe PeaQW WR UeOaWe WR Whe VWXd\ Rf diVciSOiQeV iQ geQeUaO. I aP iQWeUeVWed iQ hRZ Whe VWXd\ Rf a diVciSOiQe geWV VhaSed b\ Whe SRViWiRQV Zhich aUe adRSWed aQd Whe VWUaWegieV Zhich aUe SXUVXed. TheVe iQWeUacW; fRU Whe SXUVXiW Rf ceUWaiQ NiQdV Rf VWUaWeg\ ZiOO Oead WR Whe adRSWiRQ Rf ceUWaiQ NiQdV Rf SRViWiRQ, aQd Whe adRSWiRQ Rf ceUWaiQ NiQdV Rf SRViWiRQ ZiOO be UeTXiUed b\ Whe SXUVXiW Rf ceUWaiQ NiQdV Rf VWUaWeg\. OQe WheUefRUe QeedV WR XQdeUVWaQd hRZ Whe\ iQWeUacW. CeUWaiQ VXbVidiaU\ WhePeV UXQ WhURXgh Whe SaSeU, aOO iQWeUUeOaWed iQ RQe Za\ RU aQRWheU. OQe cRQceUQV a diaOecWicaO cRQceSWiRQ Rf PRdaOiW\, RQe WhaW iV deWeUPiQed b\ ZhaW iV OefW RSeQ aW a giYeQ VWage Rf eQTXiU\. AQRWheU iQYROYeV a SaUWicXOaU Za\ Rf e[SUeVViQg PRdaO cOaiPV, iQ WeUPV Rf ceUWaiQ RbMecWV UeTXiUiQg RWheUV. YeW a WhiUd iV aQ iQWeUeVW iQ a UeOaWiYiVW cRQceSWiRQ Rf RQWRORg\, accRUdiQg WR Zhich QR RQWRORg\ VWaQdV RXW aV beiQg cRUUecW. The SaSeU cRQcOXdeV ZiWh a fRUPaO aSSeQdi[, Zhich aWWePSWV WR PaNe SUeciVe PXch Rf ZhaW caQ be Pade SUeciVe iQ Whe eaUOieU iQfRUPaO SaUW Rf Whe SaSeU. Each SaUW haV beeQ deVigQed WR be Uead iQdeSeQdeQWO\ Rf Whe RWheU, aOWhRXgh a SURSeU XQdeUVWaQdiQg Rf eiWheU SaUW deSeQdV XSRQ UeadiQg WheP bRWh. NOUS 25 (1991) 263-294 ? 1991 b\ NRUV PXbOicaWiRQV 263 This content downloaded from 147.188.128.74 on Tue, 21 Aug 2018 16:51:52 UTC All use subject to https://about.jstor.org/terms c . c THE JOURNAL OF PHILOSOPHY volume cvii, no. 11, november 2010 c . c TOWARDS A THEORY OF PART* My aim in this paper is to outline a general framework for dealing with questions of part-whole. Familiar as this topic may be, my treatment of it is very different from more con- ventional approaches. For instead of dealing with the single notion of mereological part or sum, I have attempted to provide a comprehen- sive and unified account of the different ways in which one object can be a part of another. Thus mereology, as it is usually conceived, becomes a small branch of a much larger subject. My discussion has been intentionally restricted in a number of ways. In the first place, my principal concern has been with the notion of absolute rather than relative part. We may talk of one object being a part of another relative to a time or circumstances (as when we say that the tire was once a part of the car or that the execution of Marie Antoinette was as a matter of contingent fact a part of the French Revolution) or in a way that is not relative to a time or the circumstances (as when we say that this pint of milk is a part of the quart or that the letter ‘c’ is part of the word ‘cat’). Many philoso- phers have supposed that the two notions are broadly analogous and that what goes for one will tend to go for the other.1 I believe this view to be mistaken and a source of endless error. But it is not my aim to discuss either the notion of relative part or its connection with the absolute notion.2 * The material outlined in this paper has been developed over a period of thirty years. It was most recently presented in a seminar at Princeton in 2000; and I am grate- ful to Cian Dorr, Michael Fara, Gail Harman, Mark Johnston, David Lewis, and Gideon Rosen for their comments. I am also grateful for some comments I received from Ted Sider and two anonymous referees for this journal; and I owe a special debt of thanks to Achille Varzi for his encouragement. 1 As in Ted Sider, Four Dimensionalism (New York: Oxford, 2001), for example. 2 The matter is briefly discussed in Kit Fine, “Things and Their Parts,” Midwest Studies in Philosophy, xxiii (1999): 61–74. 0022-362X/10/0711/559–589 ã 2010 The Journal of Philosophy, Inc. 559 This framework has been recently advocated by Kit Fine. We build on his ideas. 10 -- 10 of 46 -- Our approach 11 -- 11 of 46 -- Foundation Data Model Process Model based Information Requirements Core Constructional Ontology (CCO): our current approach 12 givens the mereological atoms constructors set constructor sum constructor pair constructor We assume that the pluriverse has an atomistic mereological structure. constructed objects -- 12 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements § Foundational § Unifying § Constructional Core Constructional Ontology Key features and benefits of the approach 13 -- 13 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements § Object completeness o The construction process (“object factory”) supplies all the objects needed (resulting in an “object store”). § Categorical completeness o The approach also supplies the three basic types of objects (sets, parts, and tuples) together with their associated hierarchical relations. § Identity criteria o The construction determines the conditions for the identity of constructed objects (extensional based on the type of constructor and its input). Foundational 14 -- 14 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Core Constructional Ontology Unifying § Common development of three domains (sets, parts, and tuples) o Three “domains” (sets, parts, tuples) arising in similar ways, i.e. through construction. § Common basis for identity criteria o Identity criteria for objects of the basic types are extensional, with differences arising from the way they are constructed. § Uniform way of capturing key commonalities and differences o Commonalities and differences between objects of the basic types can be captured by features of the underlying constructors. 15 -- 15 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Core Constructional Ontology Constructional § Categorical differences are constructional differences o The ways of construction are the basis for differences in kinds of objects. § Dependency o Some objects are built from other objects and hence “depend on” them. § Reduction o The ontology is built out of a relatively small set of fundamental objects. § Consistency o Construction can be a basis for consistency. 16 -- 16 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Core Constructional Ontology Consistency “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’, […] 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ödel, What is Cantor's continuum problem?) 17 -- 17 of 46 -- Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Core Constructional Ontology supplies the required types: o sets o sums o tuples with the required extensional criteria of identity. Core Constructional Ontology and 4-dimensionalism 18 -- 18 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements § A number of options are available. § For this early phase, we chose a stage theory, inspired by o Gödel’s remark; o George Boolos’s development of the iterative conception of set based on a stage theory. Core Constructional Theory (CCT) Formalising the Core Constructional Ontology 7+( -2851$/ 2) 3+,/2623+< 92/80( /;9,,, 12 $35,/ , , B a a a aaaaa 7+( ,7(5$7,9( &21&(37,21 2) 6(7 $ 6(7 DFFRUGLQJ WR &DQWRU LV DQ\ FROOHFWLRQ LQWR D ZKROH RI GHILQLWH ZHOO GLVWLQJXLVKHG REMHFWV RI RXU LQWXLWLRQ RU WKRXJKW &DQWRU DOR VGHILQHG D VHW DV D PDQ\ ZKLFK FDQ EH WKRXJKW RI DV RQH L H D WRWDOLW\ RI GHILQLWH HOHPHQWV WKDW FDQ EH FRPELQHG LQWR D ZKROH E\ D ODZ 2QH PLJKW REMHFW WR WKH ILUVW GHIL QLWLRQ RQ WKH JURXQGV WKDW LW XVHV WKH FRQFHSWV RI FROOHFWLRQ DQG ZKROH ZKLFK DUH QRWLRQV QR EHWWHU XQGHUVWRRG WKDQ WKDW RI VHW WKDW WKHUH RXJKW WR EH VHWV RI REMHFWV WKDW DUH QRW REMHFWV RI RXU WKRXJKW WKDW LQWXLWLRQ LV D WHUP ODGHQ ZLWK D WKHRU\ RI NQRZOHGJH WKDW QR RQH VKRXOG EHOLHYH WKDW DQ\ REMHFW LV GHILQLWH WKDW WKHUH VKRXOG EH VHWV RI LOO GLVWLQJXLVKHG REMHFWV VXFK DV ZDYHV DQG WUDLQV HWF HWF $QG RQH PLJKW REMHFW WR WKH VHFRQG RQ WKH JURXQGV WKDW D PDQ\ LV XQJUDPPDWLFDO WKDW LI VRPHWKLQJ LV D PDQ\ LW VKRXOG KDUGO\ EH WKRXJKW RI DV RQH WKDW WRWDOLW\ LV DV REVFXUH DV VHW WKDW LW LV IDU IURP FOHDU KRZ ODZV FDQ FRPELQH DQ\WKLQJ LQWR D ZKROH WKDW WKHUH RXJKW WR EH RWKHU FRPELQDWLRQV LQWR D ZKROH WKDQ WKRVH HIIHFWHG E\ ODZV HWF HWF %XW LW FDQQRW EH GHQLHG WKDW &DQWRU V GHILQLWLRQV FRXOG EH XVHG E\ D SHUVRQ WR LGHQWLI\ DQG JDLQ VRPH XQGHUVWDQGLQJ RI WKH VRUW RI REMHFW RI ZKLFK &DQWRU ZLVKHG WR WUHDW 0RUHRYHU WKH\ GR VXJJHVW DOWKRXJK LW PXVW EH FRQFHGHG RQO\ YHU\ IDLQWO\ WZR LP SRUWDQW FKDUDFWHULVWLFV RI VHWV WKDW D VHW LV GHWHUPLQHG E\ LWV HOH PHQWV LQ WKH VHQVH WKDW VHWV ZLWK H[DFWO\ WKH VDPH HOHPHQWV DUH , 8QWHU HLQHU 0HQJH YHUVWHKHQ ZLU MHGH =XVDPPHQIDVVXQJ 0 YRQ EHVWLPUQWHQ ZRKOXQWHUVFKLHGHQHQ 2EMHNWHQ P XQVHUHU $QVFKDXXQJ RGHU XQVHUHV 'HQNHQV ZHOFKH GLH (OHPHQWH YRQ 0 JHQDQQW ZHUGHQ ]X HLQHP *DQ]HQ *HRUJ &DQWRU *HVDPPHOWH $EKDQGOXQJHQ (UQVW =HUPHOR HG %HUOLQ S MHGHV 9LHOH ZHOFKHV VLFK DOV (LQHV GHQNHQ O,VVW G K MHGHQ ,QEHJULII EHVWLPPWHU (OHPHQWH ZHOFKHU GXUFK HLQ *HVHW] ]X HLQHP *DQ]HQ YHUEXQGHQ ZHUGHQ NDQQ LELG S This content downloaded on Tue, 29 Jan 2013 18:51:48 PM All use subject to JSTOR Terms and Conditions 19 -- 19 of 46 -- Stage theory (Boolos) 20 stages Æ {Æ} Æ Æ {Æ} {{Æ}} {Æ, {Æ}} … § Stages are well ordered. § The domain associated with each stage includes sets formed at that stage. § At each stage all possible sets of objects existing at previous stages are formed. Æ {Æ} {{Æ}} … {Æ, {Æ}, {{Æ}}, {{{Æ}}}, …} … Suppose there are no givens: 0 1 2 w w + 1 -- 20 of 46 -- Stage theory (Boolos) 21 starting with some givens -- 21 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Our work generalizes and extends Boolos’s stage theory in three main ways: 1) we provide a unified account of parts, sets, and tuples; 2) we allow a more flexibile construction process; 3) in keeping with the target TLOs, CCT includes reified constructions, special objects that “log” the structure of the construction process. Core Constructional Ontology Core Constructional Theory: novelty 22 -- 22 of 46 -- Core Constructional Theory: mereological constructions 23 Stage 0 Stage 1 Stage 2 -- 23 of 46 -- Core Constructional Theory: mereological constructions 24 Stage 0 Stage 1 Stage 2 Example of a construction relation and a corresponding reified construction added to stage 1 a a a -- 24 of 46 -- Core Constructional Theory: mereological constructions 25 Stage 0 Stage 1 Stage 2 Example of a construction relation and a corresponding reified construction added to stage 1 a a a h Example of a construction relation and a corresponding reified construction added to stage 2 h -- 25 of 46 -- e g f Core Constructional Theory: mereological constructions 26 Stage 0 Stage 1 All mereological construction relations and corresponding reified constructions added to stage 1 a a b c d e f g b c d -- 26 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements CCT builds upon a logical framework known as plural logic, an extension of standard first-order logic. This is a classical two-sorted system, with singular and plural quantification. Core Constructional Ontology Logical framework quantification reading notation singular there is something such that… $x plural there are some things such that… there is a plurality such that… $xx 27 -- 27 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Plural quantification § gives strength to the theory by allowing to quantify over “collections” of objects in the range of the singular quantifiers. o Analogy with classes and monadic second-order quantification § serves to describe naturally inputs to constructors. Core Constructional Ontology Logical framework (cont.) 28 -- 28 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements § Logic o Plural logic § Constructors o Set, Sum, Pair § Construction process o Special predicates and constants for types of constructions § Stages o Stage-theoretic notions (is a stage, exists at a stage, follows as a stage) Primitive notions 29 -- 29 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 1) Plural logic 2) Stages 3) Initial stages 4) What exists at stages 5) Constructors 6) Reified constructions (“logs” of the construction process) 7) Maximal extension of a stage 8) Classification Axiomatisation 30 -- 30 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Core Constructional Ontology Axiomatisation (current draft) 31 G.1 Primary axioms To be deleted: the following list of axioms should be supplemented with axioms stating that  forms an atomistic general extensional mereology (AGEM) whose atoms are precisely the givens. xx 4 yy $ 8z(z xx ! z yy) xx ⇡ yy $ (xx 4 yy ^ yy 4 xx) xx@s $ 8x(x xx ! x@s) s C t $ s E t ^ s 6 = t t D s $ s E t t B s $ s C t Succ(s, t) $ s C t ^ ¬9u (s C u ^ u C t) 8xx9y y xx 8xx8yy[xx ⇡ yy ! ('(xx) $ '(yy))] 9x'(x) ! 9xx8x(x xx $ '(x)) 8s s E s 8s8t(s E t ^ t E s ! s = t) 8s08s18s2(s0 E s1 ^ s1 E s2 ! s0 E s2) s0 E s1 ^ s0 E s2 ! 9t(s1 E t ^ s2 E t) x C y $ x E y ^ x 6 = y 8ss9s(s ss ^ ¬9t(t ss ^ t C s)) 8s9t s C t 9t(9s s C t ^ 8s(s C t ! 9u(s C u ^ u C t))) xx@s^8x(x xx ! 9y(¬Stage(y)^8z( (x, z) $ y = z))) ! 9t(sEt^8x(x xx ! 8y( (x, y) ! y@t))) Init(s) $ 8t s E t Given(x) $ 9s(Init(s) ^ x@s) 38 9x Given(x) Given(cset) ^ Given(csum) ^ Given(cop) ^ Given(cunion) ^ Given(cSetElements) ^ Given(cWholeParts) ^ Given(cTuplePlaces) ^ Given(cSuperSubSets) 8x(¬Stage(x) ! 9s x@s) s E t ^ x@s ! x@t LUB(t, ss) $ 8s(s ss ! s E t) ^ 8t0(8s(s ss ! s E t0) ! t E t0) LUB(t, ss) ! 8x(x@t ! 9s(s ss ^ x@s)) ConstrFrom(x, s) $ 9xx(xx@s ^ Set(x : xx) _ Sum(x : xx)) _ 9u9v(u@s ^ v@s ^ Pair(x : u, v)) 8x(x@s $ x@t) ! s = t Succ(s, t) ^ x@t ! x@s _ ConstrFrom(x, s) _ ReifiedConstr(x) Individual(x) $ (Given(x) _ 9xx Sum(x : xx)) 8xx8s(xx@s ! 9t9x(s E t ^ Set(x : xx) ^ x@t)) 8x(x@t ^ Set(x : xx) ! 9s(s C t ^ xx@s)) Set(x : xx) ^ Set(y : yy) ! (xx ⇡ yy $ x = y) 8x(x xx ! Individual(x) ^ x@s) ! 9t9x(s E t ^ Sum(x : xx) ^ x@t) Sum(x : xx) ^ Sum(y : yy) ^ xx ⇡ yy ! x = y Sum(x : xx) ^ 8u(u xx $ u = y) ! x = y Sum(x : xx) ^ Sum(y : yy) ^ 9u 9uu 9vv (Sum(u : uu) ^ 8z(z xx $ z = u _ z vv) ^ 8z(z yy $ z uu _ z vv)) ! x = y x  y $ 9xx 9yy (Sum(x : xx) ^ Sum(y : yy) ^ xx 4 yy) x@s ^ y@s ! 9t9z(s E t ^ z@t ^ Pair(z : x, y)) Pair(z : x, y) ^ z@t ! 9s(s C t ^ x@s ^ y@s) Pair(x : u, v) ^ Pair(y : u0, v0) ! (u = u0 ^ v = v0 $ x = y) (ConstrProj1(w, y)^ConstrProj1(w, y0) ! y = y0) ^(ConstrProj2(w, y)^ ConstrProj2(w, y0) ! y = y0) ^(ConstrProj3(w, y)^ConstrProj3(w, y0) ! y = y0) ^ (ConstrProj4a(w, yy) ^ ConstrProj4a(w, yy0) ! yy ⇡ yy0) ^ (ConstrProj4b(w, y1, y2) ^ ConstrProj4b(w, z1, z2) ! y1 = z1 ^ y2 = z2) (Set(x : xx) ^ x@t ^ 9s(ConstrFrom(x, s) ^ s C t)) ! 9w(w@t ^ ConstrProj1(w, cset) ^ConstrProj2(w, cSetElements) ^ConstrProj3(w, x) ^ ConstrProj4a(w, xx)) set constructor -- 31 of 46 -- Axiomatisation (current draft) 32 (Sum(x : xx) ^ x@t ^ 9s(ConstrFrom(x, s) ^ s C t)) ! 9w(w@t ^ ConstrProj1(w, csum) ^ConstrProj2(w, cWholeParts) ^ConstrProj3(w, x) ^ ConstrProj4a(w, xx)) (Pair(x : u, v) ^ x@t ^ 9s(ConstrFrom(x, s) ^ s C t)) ! 9w(w@t ^ ConstrProj1(w, cop) ^ConstrProj2(w, cTuplePlaces) ^ConstrProj3(w, x) ^ ConstrProj4b(w, u, v)) Union(x : yy) $ 9xx (Set(x : xx) ^ 8y(y yy ! 9zz Set(y : zz)) ^ 8z(z xx $ 9y9zz(y yy ^ Set(y : zz) ^ z zz))) (Union(x : yy) ^ x@t ^9s(yy@s^ sCt)) ! 9w(w@t ^ ConstrProj1(w, cunion) ^ ConstrProj2(w, cSuperSubSets) ^ConstrProj3(w, x) ^ConstrProj4a(w, yy)) ReifiedConstr(w) $ 9x ConstrProj1(w, x) ReifiedConstr(w) ^ w@t ! 9x9xx9s(Set(x : xx) ^ x@t ^ xx@s ^ s C t ^ ConstrProj1(w, cset)^ConstrProj2(w, cSetElements) ^ConstrProj3(w, x)^ ConstrProj4a(w, xx)) _9x9xx9s(Sum(x : xx)^x@t^xx@s^sCt^ConstrProj1(w, csum)^ ConstrProj2(w, cWholeParts)^ConstrProj3(w, x)^ConstrProj4a(w, xx)) _ 9x9y19y29s(Pair(x : y1, y2)^x@t^y1@s^y2@s^sCt^ConstrProj1(w, cpair)^ ConstrProj2(w, cTuplePlaces) ^ConstrProj3(w, x)^ConstrProj4b(w, y1, y2)) _ 9x9xx9s(Union(x : xx) ^ x@t ^ xx@s ^ s C t ^ ConstrProj1(w, cunion) ^ ConstrProj2(w, cSuperSubsets) ^ConstrProj3(w, x)^ConstrProj4a(w, xx)) Max(s, t) $ sEt^8x(ConstrFrom(x, s) ! x@t) ^8x(x@t ! ConstrFrom(x, s) _ (ReifiedConstr(x) ^(9y(ConstrProj3(x, y)^ConstrFrom(y, s)) _(ConstrProj1(x, cunion)^ 9yy(yy@s ^ ConstrProjc4a(y, yy)))))) 8s9t Max(s, t) Succ(s, t) ! Max(s, t) IsSet(x) $ 9xx Set(x : xx) IsPair(x) $ 9y19y2 Pair(x : y1, y2) (IsSet(x) ! ¬Individual(x)^¬IsPair(x)^¬ReifiedConstr(x)^¬Stage(x))^ (Individual(x) ! ¬IsSet(x)^¬IsPair(x)^¬ReifiedConstr(x)^¬Stage(x))^ (IsPair(x) ! ¬IsSet(x)^¬Individual(x)^¬ReifiedConstr(x)^¬Stage(x))^ (ReifiedConstr(x) ! ¬IsSet(x)^¬Individual(x)^¬IsPair(x)^¬Stage(x))^ (Stage(x) ! ¬IsSet(x)^¬Individual(x)^¬IsPair(x)^¬ReifiedConstr(x)) The list should be supplemented with axioms stating that ≤ forms an Atomistic General Extensional Mereology (AGEM) whose atoms are precisely the givens. -- 32 of 46 -- Foundation Data Model Integration Architecture Process Model based Information Requirements Axiomatisation: set constructor 33 7.6 Constructors We need axioms that characterize the behavior of the three basic constructors and fix the identity criteria of the outputs of the constructions. This is done in the next three sections covering sets, sums, and pairs, in this order. 7.7 Set constructor (15) 8xx8s(xx@s ! 9t9x(s E t ^ Set(x : xx) ^ x@t)) (For every plurality xx of objects existing at s, there is a later stage t at which the set of xx exists.) (16) 8x(x@t ^ Set(x : xx) ! 9s(s C t ^ xx@s)) (The elements of a set exist at an earlier stage than the set itself.) (17) Set(x : xx) ^ Set(y : yy) ! (xx ⇡ yy $ x = y) (Extensionality: two sets are identical if and only if their elements are the same.) Note. Since pluralities are not empty, the axioms for the set constructor rule out the empty set. Remark. We can now derive the correct CLAP profile for sets, namely C◆ LAP. (See Appendix D for a definition of CLAP profile and for more context.) Remark. Given the set constructor and the axioms governing it, it follows logically that the stages are serial, that is, that for every stage, there is a strictly Key axioms for the set constructor -- 33 of 46 -- Axiomatisation: set constructor (cont.) 34 … a b … … {a, b} … t § Suppose the plurality of a and b exists at stage s and not before s. § Then the set of a and b, {a, b}, exists at a stage t after s. s -- 34 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements Using a natural definition of membership, we can deduce the axioms of Zermelo-Fraenkel (ZF) set theory, minus Empty Set, in CCT. Currently, the axioms of Atomistic General Extensional Mereology (AGEM) are incorporated after defining parthood. At the next stage, we will drop the axioms and deduce them from CCT. Core Constructional Ontology Set theory and mereology in CCT 35 -- 35 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements We provide a mathematical proof of consistency of CCT. This is done by constructing a model within some chosen metatheory. CCT is then shown to be consistent relative to this metatheory. § Morse-Kelley class theory (MK): it adds to ZFC a single layer of classes on top of the sets § ZFC + an extra axiom stating that there exists an inaccessible cardinal § ZFC for weakenings of CCT (e.g. plural comprehension restricted to stages or dropping the analogue of Replacement) Core Constructional Ontology Consistency 36 -- 36 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements § To help ensure logical data quality, Paweł Garbacz is working on translating automatically the human-readable axioms of CCT into CLIF. § This will avoid manual translation errors. § Owing to the axiom schemas in CCT, the translation is lossy. § We anticipate further lossy translations to OWL. CLIF 37 -- 37 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Core Constructional Ontology Questions and feedback 38 F -- 38 of 46 -- Core Constructional Ontology (CCO): a Constructional Theory of Parts, Sets, and Relations 4-Dimensionalism in Large Scale Data Sharing and Integration Newton Gateway to Mathematics -- 39 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 1) Plural logic o Pluralities are non-empty. o Pluralities with the same members satisfy the same formulas. o There is a plurality corresponding to every formula satisfied by one thing (“If there is an F , then there are the Fs.”). 2) Stages o Stages form a convergent, serial partial order. o Stages are well founded. o There are infinitely many stages and a limit stage. o A version of the axiom of Replacement holds for stages Appendix: informal overview of the axiomatisation 40 -- 40 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 3) Initial stages o The initial stage is non-empty (there are “givens” at this stage). o We assume the existence of specific givens serving to represent constructors and other relevant relations (set-elements, whole-parts, tuple-places, super- subsets). Appendix: informal overview of the axiomatisation 41 -- 41 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 4) What exists at stages o Everything that isn’t a stage exists at some stage. o Stages are “cumulative” (everything that exists at earlier stages also exists at later stages). o Limit stages are “collection” stages. o Stages with identical domains are identical. o What exists at a successor stages existed before or resulted from some construction. Appendix: informal overview of the axiomatisation 42 -- 42 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 5) Constructors 5.1) Set constructor o Every plurality of objects at a stage is used to construct a set. o The elements of a set exist before the set. o Extensionality (two sets are identical iff they have the same elements) Appendix: informal overview of the axiomatisation 43 -- 43 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 5.2) Sum constructor o Every plurality of individuals at a stage is used to construct a sum. o Sums constructed from the same pluralities are the same. o The sum constructed from the singleton plurality of x is x. o Two pluralities, one obtained from the other by replacing some objects with their sum, yield the same sum. o Parthood satisfies the axioms of AGEM. Appendix: informal overview of the axiomatisation 44 -- 44 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 5.3) Pair constructor o For any two objects existing at a stage, there is a later stage when they are used to construct a pair. o The coordinates of a pair exist before the pair. o Extensionality (two pairs are identical iff their first coordinates are the same and their second coordinates are the same) Appendix: informal overview of the axiomatisation 45 -- 45 of 46 -- Top Level Ontology Foundation Data Model Industry Data ModelsReference Data Integration Architecture Process Model based Information Requirements 6) Reified constructions (“logs” of construction process) o These axioms ensure that, whenever certain constructions are effected, there are objects that encode this information. 7) Maximal extension of a stage o These axioms sanction that every stage s has a maximal extension, i.e. a stage obtained by effecting every construction possible at s. 8) Classification o These axioms partition the domain of the theory in five kinds of entities: individuals, sets, pairs, reified constructions, and stages. Core Constructional Ontology Appendix: informal overview of the axiomatisation 46 -- 46 of 46 --