# Does the modal system S1 include the rule of necessiation?

I shall first post a couple of screenshots to make it clear what I'm talking about.

I am reading A New Introduction to Modal Logic by Hughes and Cresswell. They answer the question in title very explicitly here, but I want to know why this is the case:

But how come the rule of necessiation isn't derivable? The necessiation rule states that if a is a theorem, then so is □a. I will offer a proof and would greatly appreciate it if anyone could point out my mistake.

``````1.  ⊢ a                    Given
2.  ⊢ (p => p) <=> a        PC
3.  ⊢ □((p & q) => p)       AS1.2
4.  ⊢ □(-(p & q) v p)       PC
5.  ⊢ □(-p v -q v p)        PC
6.  ⊢ (-p v -q v p) <=> ((p => p) v -q)     PC
7.  ⊢ ((p => p) v -q) <=> (p => p)  PC
8.  ⊢ □(p=>p)               eq 5,6,7
9.  ⊢ □a                eq 8,2

``````

So given ⊢ a, we reach ⊢ □a, which is the rule I shouldn't be able to get in S1. What am I doing wrong?

• You have saved me time and time again @Bumble, so I shall tag you in hopes of borrowing your power yet again Jun 27, 2020 at 15:30