Appendix A How to read appendices
Each appendix is a class of logic functors. Then each section
describes a different logic functor. The section title gives the name
and arity of the logic functor in the form “Name/arity”. In the case
of a combinator, the name is equated to a logic functor composition,
where the symbol λ introduces each parameter of the
combinator, and the symbol μ defines it as a fixpoint (recursive
structures). In some cases a logic functor is defined as an extension
of a combinator, i.e., some parts of the logics are redefined. In this
case, the symbol ⊇ is used instead of = between the name
and the combinator definition.
The following section shows the structure and contents of each section
describing a functor.
A.1 Name/arity [=/⊇ combinator]
The logic functor is first introduced by a short description of its
formulas, interpretations, and main roles in composing logics. The
following subsections are always present unless the logic functor is
equal to a combinator. Whenever a logic element (e.g., operation,
property) is not given, the default definition is assumed (see
Chapter 2).
A.1.1 Parameters
The parameters of the functor are given a name and a type. Most often
these parameters are sub-logics, but are sometimes non-logical
parameters (e.g., an alphabet for strings).
The syntax of formulas AS is formally defined. TELL-formulas, and ASK-formulas may be defined as subsets
of AS.
The interpretation domain I and the satisfaction relation ⊨
are formally defined. In some cases, the semantics can be defined in
term of M instead of the satisfaction relation ⊨. The
ordering on interpretations ≤ may also be defined.
A.1.4 Operations
Non-default operations are here defined as algorithms. This represents
the executable part of a logic functor.
A.1.5 Properties
The behaviour of properties is given in the form of a theorem relating
a property and the properties of sub-logics. A theorem is always
accompanied by a proof, except when it is trivial given the definition
of the property and definitions of the logic functor. Some properties
can be considered as true, even if no theorem is given, when it is
trivially true: e.g., the conjunction and disjunction are always
consistent and complete when totally undefined; or when a property is
a weakening of another property that is proved: e.g., sg' is
true whenever sg is true.
For the concision of proofs, we assume a good knowledge of the theory
of logics and logic functors in the reading of proofs. What is
emphasized in proofs is the invocation of properties over sub-logics
as these invocations determine the theorems.