我试图从一阶逻辑(FOL)的角度理解DL教程中的以下段落。
通道
为了代表所有孩子都是女性的一组人，我们使用普遍限制
∀parentOf.Female(16)忘记(16)也包括那些根本没有孩子的人是一个常见的错误。
我认为(16)的意思是">如果一个人有孩子，那么这些孩子都是女性"。 我对 (16) 的 FOL 表示形式是：
∀x∀y(parentOf(x,y) → Female(y))(1)
我对这种翻译的理由是，隐式变量x表示由角色parentOf定义的一组个人。我认为x是普遍量化的。变量y代表女童，我认为在DL术语中被称为x的继承者，它在DL中明确地普遍量化。
我在 FOL 中对">根本没有孩子的个人"的 FOL 表示是：
∀x∀y ¬(parentOf(x,y))(2)
我对这段经文的解释是，如果(2)成立，那么(1)成立。这是因为在这种情况下，(1)的前因是假的。
我对这段经文的解释正确吗？
我的翻译正确吗？
关于您的公式 (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))}的子集