[ontoiop-forum] DOL finalisation

[Till Mossakowski]

Rick,

Am 05.01.2018 um 01:18 schrieb rick:
> Thanks Till for taking the time to answer my questions.
>
> I remain unconvinced that an institution that's not in the proposal is
> in scope.
>
> More important though is whether an institution of "second order logic"
> exists. 
yes, it does. See p.415 bottom of my paper
T. Mossakowski.  Relating CASL with Other Specification Languages: the
Institution Level.
Theoretical Computer Science, 286:367-475, 2002.


> And whether the required mapping from the abstract syntax of OMS
> to the signatures and sentences of "second order logic" exists. right?
Hets provides an abstract syntax for second-order logic (as part of the
CASL logic). The mapping to the institution is easy.
>
> Just to be sure, when you say "second order logic" you mean Henkin
> Semantics, right?
no, in my paper, I used standard semantics, which I need for translating
first-order logic with induction to second-order logic (see p.429 of my
paper). With Henkin semantics, it is not possible to specify inductive
datatypes (like natural numbers, lists, trees etc.) in a monomorphic
(i.e. unique up to isomorphism) way.
>
> I will enjoy reading the reference on type class polymorphism.
>
> Do you claim the paper contains the institution and the mapping? It
> seems not as the paper predates (2004) DOL.
>
> If not, could you please provide a pointer?
>
> I briefly scanned the paper. Looks like a great paper.
This paper (cited in my previous email) contains an institution for
polymorphic higher-order logic, but not for system F. It does not
contain any logic translations, except from a technical one linking two
variants of the same logic.

Best, Till