One more thing: Often one is not really interested in naming a Physical Thing that creates the shared reference space between two places. Thus, if it hasn't been done yet, I propose a new property:
Pn "shares reference space with", with domain and range E53 Place Pn(x,y) would be a (strong) shortcut for (∃u) [E18(u) ∧ P157(x,u) ∧ P157(y,u)]. P89 "falls within" would be a subproperty of Pn. Probably P121 "overlaps with" and P122 "borders with" as well. (P189 "approximates" would technically be another candidate but I don't understand it well enough to have an opinion.) If we introduce function symbols, one can additionally define: F161a: spatial projection relative to the reference space of z = F161a(x,y) ⇒ E53(z) ∧ E92(x) ∧ E53(y) z = F161a(x,y) ⇔ (∃u) [E18(u) ∧ P157(y,u) ∧ z = F161(x,u)] ⇔ Pn(y,z) ∧ P161(x,z) (the second "⇔" by definition of F161, minimising scope of u and definition of Pn) And yes, the tentative naming scheme for the function symbols is not ideal. Continuation of Example 2: P7 took place at: P7(x,y) ⇒ (∃u,z) [E18(u) ∧ P157(y,u) ∧ E53(z) ∧ P161(x,z) ∧ P157(z,u) ∧ P89(z,y) ] new: P7(x,y) ⇒ (∃z) [E53(z) ∧ Pn(y,z) ∧ P161(x,z) ∧ P89(z,y) ] or even P7(x,y) ⇒ (∃z) [E53(z) ∧ P161(x,z) ∧ P89(z,y) ] P7(x,y) ⇔ (∃u) [E18(u) ∧ P157(y,u) ∧ P89(F161(x,u), y)] new: P7(x,y) ⇔ P89(F161a(x,y), y) And one last thing: I realised that the right-hand side is exactly the same for P7 and P167 "was within": P167(x,y) ⇔ (∃z,u) [E53(z) ∧ E18(u) ∧ P157(y,u) ∧ P161(x,z) ∧ P157(z,u) ∧ P89(z,y)] The only difference is: P7(x,y) ⇒ E4(x) P167(x,y) ⇒ E93(x) (and ⇒ for P7 versus ⇔ for P167, but I guess this can be rectified) F161a(x,y) works for both because x is an E92 Spacetime Volume. Which reminds me of something I had written to Christian-Emil about issue 606: P7 cannot be a superproperty of P161 because of the E4 / E92 domains. Why don't you simply declare it a "quasi subproperty", i.e. the P161(x,y) ∧ E4(x) ⇒ P7(x,y) in your new P161 FOL description, and then stop? Or why don't you extend the domain of P7 (or P167) to E92? I don't see anything in the P7 / P167 scope notes that wouldn't be applicable to any STV. The label "took place at (witnessed)" would be slightly awkward, but that's it. But it is easily possible that I have overlooked something here. > Am 17.10.2022 um 12:21 schrieb Wolfgang Schmidle via Crm-sig > <[email protected]>: > > Dear All, > > Some phenomenal or unique declarative thingies behave like functions and can > be more clearly described as such. This would make many "∃" in the FOL > descriptions superfluous. Therefore I propose to introduce function symbols > in the FOL. Some examples are given below. > > Best, > Wolfgang > > > Example 1: E93 Presence as a function of a Physical Thing or STV and a > Time-Span > > E18 Physical Thing x P46 is composed of E18 Physical Thing y > implies that there is a E52 Time-Span z with: > > x P195i had presence E93 Presence u P164 is temporally specified by z > y P195i had presence E93 Presence w P164 is temporally specified by z > w P10 falls within u > P46(x,y) ⇒ (∃z,u,w) [E52(z) ∧ E93(u) ∧ P195i (x,u) ∧ P164(u,z) ∧ E93(w) ∧ > P195i (y,w) ∧ P164(w,z) ∧ P10(w,u)] > > While the (∃z) is fine, the (∃u,w) is grating. Although not wrong, it doesn't > catch the fact that a Presence is uniquely determined by any Physical Thing > or STV plus any Time-Span. > > To express this, we can introduce an additional function symbol "F93" in the > FOL for E93: > u = F93(x,z) ⇒ E93(u) ∧ [E18(x) ∨ E92(x)] ∧ E52(z) > u = F93(x,z) ⇔ [P195(u,x) ∨ P166(u,x)] ∧ P164(u,z) > > (E93 and F93 are not more repetitive than e.g. P14 and P14.1.) > > And then in the FOL for P46, we can write: > P46(x,y) ⇒ (∃z) [ P10(F93(y,z), F93(x,z)) ] > > > Example 2: P161 has spatial projection, as a function of an STV and a > Physical Thing as reference space > > P7 took place at: > E4 Period x P7 took place at E53 Place y > implies that there is an E18 Physical Thing u with: > > y is at rest relative to u, and the spatial projection z of x relative to u > is contained in y > P7(x,y) ⇒ (∃u,z) [E18(u) ∧ P157(y,u) ∧ E53(z) ∧ P161(x,z) ∧ P157(z,u) ∧ > P89(z,y) ] > > Since the spatial projection of a STV is unique if a reference space is > specified, one can introduce a function symbol F161: > z = F161(x,u) ⇒ E53(z) ∧ E92(x) ∧ E18(u) > z = F161(x,u) ⇔ P161(x,z) ∧ P157(z,u) > > Then the statement above becomes > P7(x,y) ⇔ (∃u) [P157(y,u) ∧ P89(F161(x,u), y)] > > And if one adds a property P7.1 "relative to": > P7.1(x,y,u) ⇔ P7(x,y) ∧ P157(y,u) > then one can write is as > P7.1(x,y,u) ⇔ P89( F161(x,u), y) > > > P167 was within: > E93 Presence x P167 was within E53 Place y > E93 Presence x P161 has spatial projection E53 Place z P89 falls within E53 > Place y > P167(x,y) ⇔ (∃z) [E53(z) ∧ P161(x,z) ∧ P89(z,y)] > > If one includes the reference space: > P167(x,y) ⇔ (∃z,u) [E53(z) ∧ E18(u) ∧ P157(y,u) ∧ P161(x,z) ∧ P157(z,u) ∧ > P89(z,y)] > > This can be written as > P167(x,y) ⇔ (∃u) [P157(y,u) ∧ P89(F161(x,u), y)] > > (However, this might change according to the results of issue 606.) > > > Example 3: P156 occupies, P196 defines > > E18 Physical Thing x P156 occupies E53 Place y > define y = F156(x) > > E18 Physical Thing x P196 defines E92 Spacetime Volume y > define y = F196(x) > > (E4 Period, before it became a subclass of E92 Spacetime Volume, would have > been similar.) > > > From the P156 scope note: > This property implies the fully developed path from E18 Physical Thing > through P196 defines, E92 Spacetime Volume, P161 has spatial projection to > E53 Place. However, in contrast to P156 occupies, the property P161 has > spatial projection does not constrain the reference space of the referred > instance of E53 Place. > P156(x,y) ⇔ (∃z) [E18(x) ∧ E53(y) ∧ P196(x,z) ∧ P161(z,y) ∧ P157(y,x)] > > This can be written as > F156(x) = F161(F196(x), x) > > > P8 took place on or within: > E4 Period x P8 took place on or within E18 Physical Thing y > E4 Period through x P7 took place at E53 Place z P156i is occupied by E18 > Physical Thing y > P8(x,y) ⇐ (∃z) [E53(z) ∧ P7(x,z) ∧ P156(y,z)] > > P8(x,y) ⇐ P7(x, F156(y)) > > > P195 was a presence of: > E93 Presence x P195 was a presence of E18 Physical Thing y > E93 Presence x P166 was presence of E92 Spacetime Volume z P196i is defined > by E18 Physical Thing y > P195(x,y) ⇔ (∃z)[E92(z) ∧ P166(x,z) ∧ P196i(z,y)] > (in the scope note the shortcut is given in the wrong direction, and typo > "P166(z,x)" corrected) > > P195(x,y) ⇔ P166(x, F196(y)) > > > Example 4: P168 place is defined by > > E53 Place z P168 place is defined by E94 Space Primitive y > define z = F168(y) > > P171 at some place within: > E53 Place x P171 at some place within E94 Space Primitive y > E53 Place x P89 falls within E53 Place z P168 place is defined by E94 Space > Primitive y > through a declarative Place z that is not explicitly documented > P171(x,y) ⇔ (∃z) [E53(z) ∧ P89(x,z) ∧ P168(z,y)] > > P171(x,y) ⇔ P89(x, F168(y)) > > P172 contains: > E53 Place P172 contains E94 Space Primitive > P172(x,y) ⇔ (∃z) [E53(z) ∧ P89i(x,z) ∧ P168(z,y)] > > P172(x,y) ⇔ P89(F168(y), x) > > > _______________________________________________ > Crm-sig mailing list > [email protected] > http://lists.ics.forth.gr/mailman/listinfo/crm-sig _______________________________________________ Crm-sig mailing list [email protected] http://lists.ics.forth.gr/mailman/listinfo/crm-sig
