Issue 673: missing inverse labels P81, P82, P171, P172
Post by Eleni Tsouloucha (8 February 2024)
Dear all,
Since we made E61 isA E59 AND E41, it means that there can be inverse properties for *P81 ongoing throughout* & *P82 at some time within*. Which
is implicit in the FOL for P170 defines time (time is defined by) --see v7.1.2 (Official (Base for initial ISO Submission) and v7.2.3(draft, community version).
In first-order logic:
P170(x,y) ⇒ E61(x)
P170(x,y) ⇒ E52(y)
*P170(x, y) ⇒ P81i(x, y) ∧ P82i(x, y)*
* Incidentally, we have documented that P170(x,y) ⇒ P81(y,x) & P82(y,x) (see
issue 508, Martin's post on 23 July 2020 specifically), which got translated into listing the inverse forms of P81/P82 in v7.1.2, without bothering to revisit the lack of inverse forms for respective properties.
The same situation holds for P171 at some place within and P172 contains, (whose ranges are set to E94 Space Primitive). Now that E94 isA E59 AND E41, we should define inverse properties for them (and these should have labels).
Best,
Eleni
Post by Martin Doerr (8 February 2024)
Dear Eleni,
I'd suggest not to assign inverse labels, nevertheless. These primitive values do not constitute particular objects of discourse, albeit that there is a naming aspect.
P170, P168, P169 are different, they are epistemic constructs. Anyway, to be discussed!
Best,
Martin