# Natural deduction introduction and elimination rules for modal quantifiers

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?

• <> introduction/elimination are described on Cogburn's blog. For quantifiers see ch.12 of Garson's book. Dec 19, 2017 at 0:40
• I can't access the book, but the blog is great! If you post this as an answer, maybe with a small summary, I would accept it in a heartbeat. Dec 19, 2017 at 0:52
• Thanks, but not my cup of tea. Since you seem excited perhaps you could post a self-answer summary. For the book try this link. Dec 19, 2017 at 1:00
• You can see: David Siemens, FITCH-STYLE RULES FOR MANY MODAL LOGICS, NDJFL (1977) Dec 19, 2017 at 8:44
• Maybe also the "original": Frederic Brenton Fitch, Symbolic Logic: An Introduction, Ronald Press (1952) Dec 19, 2017 at 8:46

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.

• What did you find out about a <>-introduction rule? I share your aesthetic tastes and would prefer to have [] and <> primitive too, and am curious if it's possible. Oct 26, 2018 at 13:44
• @Adam, I didn't keep looking for too long, but I never found anything. : ( Oct 28, 2018 at 22:14
• It looks like your <> elimination rule is also a <> introduction rule; and they cannot be seperrated. You are eliminating <>P and introducing <>Q, via deriving Q under a boxed-context assumption of P. Oct 17, 2019 at 2:24