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
