FO[Concept]

Goal

The goal of FO[Concept] is to allow quantification and aggregates over the concept of an ontology.

Syntax

FO[Concept] adds these production rules:

    Type ← 'Concept' '[' Signature ']';
    Identifier ← '`{NAME_S}';
    Symbol ← '$' '(' Expression ')';

Well-formedness

  1. In `{NAME_S}, NAME_S must have been declared as a symbol.

  2. The first argument of the $ operator must be a Concept.

  3. The number and types of the arguments applied to $(x) must be consistent with the signature of Concept x.

  4. The type of $(x)(y1, .. yn) is the range in the signature of Concept x.

Semantic

FO[Concept] extends the domain of discourse with the “intension” of the symbols in the ontology. The intension of a symbol is the concepts it represents.

Concept[T1 ⨯ ... ⨯ Tn → T] is the type whose elements are the intensions of the symbol with signature T1 ⨯ ... ⨯ Tn → T. These elements are denoted by prepending the symbol with a back-tick: `, e.g., `fever is the concept of symbol fever.

Example

The number of symptoms that a person p has can be defined as

    #{s in Concept[Person → 𝔹]: symptom(s) ∧ $(s)(p)}

Or, using a binary quantification of FO[Sugar]:

    #{s in symtom: $(s)(p)}

FO(Concept) abstract language

The formal semantics of FO(Concept) is described in [CdHD22].