# FO[Concept]¶

Goal

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

Syntax

    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].