description-logic

Translate "there exists one" from English sentence to ALCQO description logic


I have the following English question

There exists one school student.

And I would like to translate it to ALCQO or First order logic.

I have written the following:

∃SchoolStudent

or in First Order Logic:

∃x(SchoolStudent(x))

However, I know from mathematics and the theory that is translated as "at least one" or "some". Thus, I am wondering if the following two options are correct:

approach 1

¬∃x(SchoolStudent(x))

approach 2

(≥1student.SchoolStudent)⊓(≤1student.SchoolStudent)

Solution

  • ∃SchoolStudent is meaningless in ALCQO. The only constructor available in ALCQO using existential restrictions are of the form

    ∃r.C

    which is interpreted as

    {d ∈ ΔI | there is an e ∈ ΔI with (d, e) ∈ rI and e ∈ CI}

    In first order logic ∃r.C translates to πx(∃r.C) = ∃y.r(x, y) ∧ πy(C).

    To define a school with only 1 student you will have to have the concepts School and Student and a role which can be used to associate a student with a school, say hasStudent.

    School ≡ ∃hasStudent.Student ⊓ ≤1hasStudent.Student

    This means School here is the set of schools that have only a single student.

    But we can also define School as anything that has more than 1 student and then define a specific individual of the school as a school with only 1 student.

    School ≡ ∃hasStudent.Student

    School(x)

    ≤1hasStudent.Student(x)