Question
Given a new proof system S which contains the following axioms:
The regular HPC axioms (https://en.wikipedia.org/wiki/Hilbert_system) P1-P4.
A new axiom is introduced: $(a \lor b) \rightarrow (\lnot a \rightarrow b)$
The deduction rules are: Modus Ponens and the following rules: $\frac a{a \lor b}, \frac b{a \lor b}$
Prove that S is not complete over sentences with the operators $\rightarrow , \lnot, \lor$.
It's given that this system is sound.
Proof idea
I've been told that I need to assume that $\vdash_S p \lor \lnot p$ and somehow get a contradiction from it , but I just can't see the formal way to prove this, I would love some explanation of the formal way to disprove completeness of such systems. Thanks in advance.