Natural deduction introduction and elimination rules for modal quantifiers

Question

I've read several papers on modal natural deduction but I've only been able to find one clear explanation of []-Introduction ([]A if A can be proved from no assumptions/premises). But there were no separate rules for <>-Introduction. Instead <>A was defined as ~[]~A. And there were no rules for quantifier elimination at all.

For aesthetic reasons I'd prefer to work in a logic where all symbols are defined primitively and their correspondences are results, and where we cannot manipulate terms in the scope of a quantifier.

Is there a formalization of modal logic of this sort? What are its introduction and elimination rules? Are there any papers on it?

Answer 1

From Garson's Modal Logic for Philosophers (link in comments above):

First we introduce a new kind of subproof, a boxed subproof. It contains no assumptions and is marked by [] at its start, as in

| presmises
|---
| stuff
|| []
||---
|| other stuff
| more stuff

You can't reiterate into a boxed subproof, so the following is invalid:

| Q
|---
|| []
||---
|| Q R   (BAD! NO! DON'T!)

That would obviously be fallacious---going from "is the case" to "necessarily the case".

Now for the inference rules. []-Introduction:

| []
|---
| .
| .
| .
| Q
------ []I
[]Q

There's a []-elimination rule, too. It's the exception to the no-reiterating thing and it goes like this:

| []Q
|| []
||---
------ []E
|| Q

Note that this isn't really elimination, not in the normal way we think about it. What you'd really expect is something like []Q -> Q, but this is actually an axiom added to K to make system T.

Now Garson defines <>Q := ~[]~Q, but I want to be able to introduce and eliminate it primitively. Garson provides a derived rule for <>-elimination:

<>P
| []
|---
|| P
|| .
|| .
|| .
|| Q
------ <>E
<>Q

Which can be summed-up as

<>P
[](P -> Q)
------ <>E
<>Q

---

I haven't been able to find an inference rule for <>-introduction. It now seems to me that no such rule is possible, because there is no a priori way of discovering whether or not a formal statement is merely possible. This stands in contrast to necessity---we know a priori that every statement provable in nonmodal logic is necessary.