Using axioms of K(n+1) as hypothesis in Kn

Question

I am working through Elliott Mendelson's book on mathematical logic, and I don't understand his proof of one of the Lemma.

The lemma reads:

If a closed wf ¬B of a theory K is not provable in K, and if K′ is the theory obtained from K by adding B as a new axiom, then K′ is consistent.

His proof:

Assume K′ inconsistent. Then, for some wf C, ⊢K′ C and ⊢K′ ¬C. Now, ⊢K′ C ⇒ (¬C ⇒ ¬B). So, by two applications of MP, ⊢K′ ¬B. Now, any use of B as an axiom in a proof in K′ can be regarded as a hypothesis in a proof in K.Hence, B⊢K ¬B. (Etc.)

What I don't understand is this: it doesn't seem that B is used as an axiom to prove ¬B in K'. Therefore, I don't see why we can use it as a hypothesis in K to derive B⊢K ¬B.

Am I missing something here?

Thank you in advance for all help!

Answer 1

We can always add un-necessary assumptions: if we have $⊢_{K′} ¬B$, we have also $B ⊢_{K′} ¬B$.

You can review the definition of consequence of a set $Γ$ of formulas (page 28, 6th ed) and the first property:

If $Γ⊆Δ$ and $Γ⊢C$, then $Δ⊢C$.

In the above proof, Mendelson uses the case $Γ= \emptyset$ and $Δ= \{ B \}$.