Why does modal logic need to use ◻◻p?

In Frederic Fitch's Symbolic Logic he proves (11.8, page 66) that "◻p" coimplicates "◻◻p".

In 11.10 (page 66), he writes,

A system almost the same as the system Lewis calls S2 is obtainable by adding the principle of excluded middle to the present system and making a restriction as follows: When reiterating into a strict subordinate proof, the first square on the left side of the reiterated proposition must be dropped and only the remaining part of the proposition written as an item of the subordinate proof. This restriction would make it impossible to prove [◻p ⊃ ◻◻p] in general, and the second subordinate proof of 11.8 would be invalid.

By "Lewis" he refers to Lewis and Langford's book Symbolic Logic. The system Fitch presents in his book does not allow the use of the law of excluded middle to apply to an arbitrary proposition, but only to propositions with a definite truth value. This is because he also includes propositions that are "indefinite", that is, without a specific truth value.

This makes me wonder why modal logic needs to use "◻◻p" at all?

Modal logic can be used to model a lot of things. One of those things is knowledge (in epistemic logic, which is an application of modal logic in epistemology), which is of particular interest to philosophers. In epistemic logic, ◻p is interpreted to mean that p is known or that A knows that p, relative to some agent A. It's usually written "Kp".

In this context ◻◻p (or: KKp) means that A knows that he knows that p. You can then ask an interesting question: Does Kp entail KKp? That is, if you know something, do you thereby know that you know it? This is called the KK Principle. It's controversial whether it is true (as a thesis about knowledge) and it touches on a lot of interesting issues in epistemology.

• Fitch is able to show, using his system that does not include the law of the excluded middle, that ◻◻p entails ◻p and that ◻p entails ◻◻p. This makes me wonder why model logic needs to use ◻◻p if it has ◻p? In the epistemic logic example you provide, there might be some interest in having KKp provided Kp does not entail KKp. Oct 13 '18 at 23:07
• @FrankHubeny Whether ◻◻p and ◻p are equivalent depends on the specific system of modal logic (that is, which axioms are used). It's not true in all modal logics. It's not simply a matter of definition that ◻◻p ↔ ◻p. And again, in various applications of modal logics they are not equivalent and mean very different things. Oct 13 '18 at 23:25
• @FrankHubeny Maybe I'm misunderstanding your question and you're asking why ◻◻p is needed in Fitch's system where the equivalence holds, but that's a different question than the one in your title and post. Oct 13 '18 at 23:28
• I am asking it more generally. In Fitch's system I don't think ◻◻p is needed. Fitch does mention that there are systems where it is "impossible to prove [◻p ⊃ ◻◻p] in general" as I quoted him. Those are the ones that might have some need for ◻◻p. Oct 14 '18 at 4:00

I may have found an answer to my own question although I thought it would be more complicated than it is.

This question is:

Why does modal logic need to use "◻◻p" at all?

The answer is that such an expression is required by the rule of necessity introduction which Fitch abbreviates to "nec int".

To see this in more detail, first consider the rule of necessity elimination ("nec elim"): (page 64)

1  |  ☐p    hyp
|_
2  |  p      1, nec elim

If I have the hypothesis (hyp) "☐p" I can eliminate the necessity and work only with "p".

Elimination rules are paired with introduction rules. Here is Fitch's description of this rule (page 64-5):

This rule requires the use of a new kind of subordinate proof, one that has no hypothesis and that is such that a proposition q can be reiterated into it only if q is of the general form ☐r, or is of one of certain other forms later to be specified. Such a subordinate proof will be known as a strict subordinate proof and will always have a square attached to the left of its vertical line, near the top, to indicate the special restriction regarding what can be reiterated into it.

Suppose we have something like the following:

1   |  ☐p        hyp
|_
2   | ☐ | ☐p    1, reit
3   |  ☐☐p      2-2, nec int

In order to be able to close the strict subordinate proof which in the example only consists of line 2 I need to be able to add a "☐" in front of whatever I have there even it it is something like "☐p".

Therefore we need to use symbols such as "◻◻p" in order to permit use of the rule of necessity introduction.

As another argument according to Wikipedia, the Necessitation Rule, part of the K system, states the following:

N, Necessitation Rule: If p is a theorem (of any system invoking N), then □p is likewise a theorem.

If □p is a theorem, by the Necessitation Rule, so is □□p.

References

Fitch, F. B. (1952). Symbolic logic.

Wikipedia, "Modal logic" https://en.wikipedia.org/wiki/Modal_logic