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
In
`{NAME_S}
,NAME_S
must have been declared as a symbol.The first argument of the
$
operator must be a Concept.The number and types of the arguments applied to
$(x)
must be consistent with the signature of Conceptx
.The type of
$(x)(y1, .. yn)
is the range in the signature of Conceptx
.
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].