I am trying to understand the following Passage from a DL tutorial in terms of First Order Logic (FOL).

Passage

To represent the set of individuals all of whose children are female, we use the universal restriction

∀parentOf.Female (16)

It is a common error to forget that (16) also includes those individuals that have no children at all.

I take (16) to mean "if an individual has children, then those children are all female". My FOL representation of (16) is:

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

My rational for this translation is that the implicit variable x represents the set of individuals being defined by the role parentOf. I assume x is universally quantified. The variable y represents female children, which I believe is called the successor of x in DL terminology, it is explicitly universally quantified in DL.

My FOL representation of "individuals that have no children at all" in FOL is:

∀x∀y ¬(parentOf(x,y)) (2)

My interpretation of the Passage, in FOL terms, is that if (2) holds then (1) holds. This is because the antecedent of (1) is false in this case.

Is my interpretation of the Passage correct?

Are my translations correct?

TL;DR

What's wrong in your interpretation is that, while (1) correctly represent an axiom (i.e. something that you assume or impose to be true), (2) does it incorrectly. Indeed "individuals that have no children at all" is not an axiom, is just a set of individuals.

Using the DL syntax, you can express it as follows:

∀parentOf.⊥

Under every possible interpretation, ∀parentOf.⊥ is always included in ∀parentOf.Female (because, under every possible interpretation, ⊥ is always included in Female).

Long explanation

About your formula (1)

If you say

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

or, equivalently

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

you mean that every x can only have female children. But for stating this in DL you need concept inclusion, that is:

⊤ ⊑ ∀parentOf.Female

that means "the range of role parentOf is included in concept Female" (see below the reason why).

Concept and role inclusions are intensional assertions, i.e., axioms specifying general properties of DL constructs.

Instead, DL's restrictions are not assertions, but constructs like concepts. So they are not used to state properties that are valid for every individual of the ontology. Like, when you say C⊓D, you are not stating that all the individuals of your ontology are instances of C and D, but you are simply "collecting" only the individuals that are instances of C and D at the same time.

Therefore, the formula ∀parentOf.Female just "collects" all the x such that, if x is a parent of y, then y is Female. More formally, every interpretation I of your ontology must be such that the interpretation function ⋅ᴵ satisfies the equation:

(∀parentOf.Female)ᴵ = {x|for every y, if (x,y) ∈ parentOfᴵ then y ∈ Femaleᴵ}

Now, if the ontology contains the axiom ⊤ ⊑ ∀parentOf.Female, then every interpretation I, in order to be a model of the ontology, must be such that the interpretation function ⋅ᴵ satisfies the equation:

⊤ᴵ ⊆ (∀parentOf.Female)ᴵ

from which it follows that:

Δᴵ ⊆ {x|for every y, if (x,y) ∈ parentOfᴵ then y ∈ Femaleᴵ}

(where Δᴵ is the whole interpretation domain), which holds iff your FO implication (1) is entailed by the ontology.

But this is not what you want! You just need to select the "individuals all of whose children are female", which, as we said, can be done by ∀parentOf.Female.

About your formula (2)

Likewise, the "individuals that have no children at all" cannot be captured by ∀x∀y ¬(parentOf(x,y)). This formula is imposing that every individual has no children, while you just want to refer to all such individuals.

The correct DL construct

Using the DL syntax, you can express "individuals that have no children at all" as follows:

∀parentOf.⊥

or equivalently:

¬∃parentOf

For the sake of brevity, let us focus on the first one. Intuitively, you are selecting all the individuals x that, if they have a relation parentOf with some y, then y must be instance of ⊥. Since the consequent is impossible, then all the individuals you are referring to have no relation parentOf (i.e. they have no children at all).

Formally, similarly to what we saw above, every interpretation I of your ontology must be such that the interpretation function ⋅ᴵ satisfies the equation:

(∀parentOf.⊥)ᴵ = {x|for every y, if (x,y) ∈ parentOfᴵ then y ∈ ⊥ᴵ}

It is easy to see that, for every interpretation I, we have that (∀parentOf.⊥)ᴵ ⊆ (∀parentOf.Female)ᴵ, since ⊥ᴵ (i.e. the empty set) is trivially included in Femaleᴵ.

Conclusion

You say right: "if (2) holds then (1) holds". The point is that neither (2) nor (1) necessarily hold, because you are not required to claim any axiom.

Since you are working with sets, you should not reason in terms of logical inference but of set inclusion.

Then, the correct interpretation of the Passage is not

if ∀x∀y ¬(parentOf(x,y)) then ∀x∀y(parentOf(x,y) → Female(y))

but

{x|∀y ¬parentOf(x,y)} is a subset of {x|∀y (parentOf(x,y) → Female(y))}