sublogics based on theories?

[till]

Explore the following idea:

It is also possible to define sublogics by requiring signatures to include a certain base theory (like extensionality in HasCASL, or S5 in ModalCASL). (Note that theory inclusions suffice here, arbitrary theory morphisms would add a generality that is not really needed.)

In heterogeneous libraries, the library item "logic lid" would be refined to

logic lid theory thbase

which makes thbase into a base theory for this logic, i.e. a theory that is implicitly included everywhere.

Two options to realize this

• either define "new" logics to be theories in "old" logics, then a "new" theory is an extension of the "old" theory. Although Grothendieck theories would remain essentially the same, this needs a larger refactoring of Logic.Logic, Logic.Grothendieck etc.
• or revise the notion of sublogic (in an institution independent way), such that a "new" sublogic may be a pair of an "old" sublogic and an "old" theory in that sublogic.

[maeder]

#345 depends on this