[ontoiop-forum] DOL finalisation

[Till Mossakowski]

Am 03.01.2018 um 08:19 schrieb Pat Hayes:
>> second-order logic is not outside the scope of DOL. DOL is a
>> meta-language that can be used for a variety of logics, provided they
>> can be formalised as an institution. Such logics include propositional
>> logic, OWL, Common Logic, first-order logic, second-order logic, modal
>> logics, hybrid logics, temporal logics, higher-order logics (also
>> variants including type constructors, subtypes and/or polymorphism),
>> intuitionistic logics, program logics, and many more.
> I confess to finding this either (a) hard to believe, or (b) slightly meaningless. This plethora of logics has such a variety of wildly different semantics that I fail to see how anything, or indeed anyone, mechanical or human, can define meaningful - truth-preserving - mappings between them all. But perhaps (?) preservation of meaning is not part of the game? 
First, DOL is about structuring logical theories (in DOL speak: OMS),
declaring theory interpretations, conservative extensions, alignments,
networks, refinement etc. This can be done separately for each logic.
Formalising logics as institutions just provides the technical means to
apply this general theory of structuring. Of course, the conditions on
institutions are rather mild and the notion is rather general, so it is
no surprise that so many logics can be formalised as institutions. But
this is not a bug but a feature, because it means that DOL structuring
can be applied to a wide variety of logics.

Second, DOL is about translation between logics, and related,
specification of heterogeneous logical theories (OMS). This is a
different story. Of course, you cannot expect that all logics can be
mapped into each other, especially because a certain preservation of
meaning is required (otherwise logic mappings are not very useful).
Still, one can define useful graphs of logics and mappings. Hets
supports a particular such graph.
>
> Are there any logics that *cannot* be formalized as an institution? (Nonmonotonic logics. perhaps?) I have no idea what kind of constraint this formalization represents. 
Institution theory and DOL use the model-theoretic definition of logical
consequence: Gamma |= phi iff for all models M, M |= Gamma implies M |=
phi. This is necessarily monotonic. Hence, non-monotonic logics are
outside the scope of DOL. That said, note that DOL provides a construct
"minimize" that captures McCarthy's circumscription and that can be used
to express closed-world assumptions in a fine-grained way (that is, also
restricted to certain symbols).

Best, Till