# Proof of $p\rightarrow (\Box (\Box p \wedge p) \rightarrow (\Box p \wedge p))$

I need to prove:

$$p\rightarrow (\Box (\Box p \wedge p) \rightarrow (\Box p \wedge p))$$

The system contains all propostional tautologies and the axiom scheme $\mathbf K$:$\Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q)$.

Rules are modus ponens, substitution and necessitation.

Thanks for help!

• What does $\Box$ stand for? Negation? – layman Nov 26 '14 at 12:58
• @MathIsHardNoItsNot Necessity. – Git Gud Nov 26 '14 at 13:00
• @Charles Do you mind listing $\bf K$? – Git Gud Nov 26 '14 at 13:00
• @GitGud Sure, no problem! – Charles Bronson Nov 26 '14 at 13:02
• Do you have the reflexivity axiom $\square p\to p$? – user21467 Nov 26 '14 at 13:14

$\square p\land p\to p$ is a theorem; therefore $\square(\square p\land p\to p)$ by necessitation, and so $$\square(\square p\land p)\to \square p$$ by $\mathbf K$ (and modus ponens). Now apply $p\land\cdot$ to both sides and use the equivalence of $a\land b\to c$ and $a\to(b\to c)$.