3

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?

2

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.

  • 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. – Adam Oct 26 '18 at 13:44
  • @Adam, I didn't keep looking for too long, but I never found anything. : ( – Canyon Oct 28 '18 at 22:14

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.