Modal Operator Comprehension, what Logic would suit?

[Jan Burse]

Dear All

I just did a little tour de force of Prawitz on Minimal 2nd
Order Logic. What I like about it, is its cut elimination
theorem and that we can derive comprehension:

|- exists X forall y ((X y) <-> C)

When we cast this in kinds, then we would have:

X : i -> o

y : i

Whereby i stands for Individuals, and o for Propositions.
The nice thing is that comprehension can be derived from
abstraction and second order existential quantifier.
Abstraction reads:

G |- C[y/t]
------------------- (Right lambda)
G |- (lambda y.C)t

And second order existential quantifier reads:

G |- D[X/F]
--------------- (Right exists)
G |- exists X D

The involved kinds are:

t : i

F : i -> o

D, C : o

What if I want to do comprehension for a modal operator?
To be precise I want to arrive at comprehension as
follows:

|- exists M forall D ((M D) <-> C)

M : o -> o

Can I just modify the above rules (Right lambda) and
(Right exists)? The thing will not be second order logic
anymore, right? Would cut elimination still go through?
What kind of logic is it?

Bye