InqLog.FO.Signatures

We start by defining the class of Signatures. A signature consists of a set of predicate symbols (captured by the type PSymb) and a set of function symbols (captured by the type FSymb). Each symbol has an finite arity (type), which is assigned by the functions PAri and FAri. The finiteness is captured by enumerations PAri_enum and FAri_enum whose characterization are captured by PAri_enum_charac and FAri_enum_charac. We also want to have decidable (standard) equality for both PSymb and FSymb which is captured by PSymb_EqDec and FSymb_EqDec. In addition, we need a boolean predicate rigid which tells us for every function symbol whether it is rigid or not. A function symbol shall be called rigid if its interpretation is independent from a concrete world. This whole definition is based on Ciardelli's work.