Понимание универсального ограничения концепции в логике описания (DL)

О вашей формуле (1)

Если вы скажете

∀x∀y(parentOf(x,y) → Female(y))

или, что то же самое

∀y((∃x parentOf(x,y)) → Female(y))

вы имеете в виду, что каждый x может иметь только девочек. Но для того, чтобы указать это в DL, вам нужно включить понятие, то есть:

⊤ ⊑ ∀parentOf.Female

это означает, что диапазон роли parentOf включен в понятие Female.

Включение понятий и ролей — это интенсиональные утверждения, т. е. аксиомы, определяющие общие свойства конструкций DL.

Вместо этого ограничения DL являются не утверждениями, а конструкциями, подобными концепциям. Таким образом, они не используются для определения свойств, действительных для каждого индивидуума онтологии. Например, когда вы говорите C⊓D, вы не утверждаете, что все индивидуумы вашей онтологии являются экземплярами C и D, а просто собираете только индивидуумы, которые одновременно являются экземплярами C и D.

Следовательно, формула ∀parentOf.Female просто хочет поймать все x таким образом, что если x является родителем y, то y будет Female. Более формально его семантика такова:

{x|∀y (parentOf(x,y) → Female(y))}

О вашей формуле (2)

Точно так же семантика индивидуумов, у которых вообще нет детей, также является набором индивидуумов:

{x|∀y ¬parentOf(x,y)}

или эквивалентно

{x|¬∃y parentOf(x,y)}

Ведь вы собираете всех особей, у которых нет детей, а не констатируете, что у всех особей нет детей.

Вывод

Вы правильно сказали: если выполняется (2), то выполняется (1). Дело в том, что ни (2), ни (1) (обязательно) не выполняются.

Поскольку вы работаете с множествами, вам следует рассуждать не с точки зрения логического вывода, а с точки зрения включения множества.

Следовательно, правильная интерпретация отрывка не

если ∀x∀y ¬(parentOf(x,y)) то ∀x∀y(parentOf(x,y) → Female(y))

но

{x|∀y ¬parentOf(x,y)} является подмножеством {x|∀y (parentOf(x,y) → Female(y))}