I was reading "Proofs and Types", so there came across that any proposition can be converted to lambda form. So was trying out with Hilbert system's axioms
P1. $A \rightarrow A $
P2. $A \rightarrow (B \rightarrow A)$
P3. $A \rightarrow (B \rightarrow C) \rightarrow (A \rightarrow B) \rightarrow (A \rightarrow C)$
P4. $ (A \rightarrow B ) \rightarrow ((A \rightarrow \lnot B) \rightarrow \lnot A) $
I could get that P1 is $I$ combinator and P2 is $K$ and P3 is $S$. P1 is redundant since $I = SK$. But i couldnt figure out how to turn P4 into $\lambda$ form. Even though i get how $\lnot A = A \rightarrow \bot$ .
Also if there is no equivalent of P4 in Combinatory logic then, basically i cannot express negative stuff in Combinatory logic at all?