 Russell and Whitehead also suggested a system with five propositional axioms.Axioms P1, P2 and P3, with the deduction rule modus ponens (formalising intuitionistic propositional logic), correspond to combinatory logic base combinators I, K and S with the application operator.Proofs in the Hilbert system then correspond to combinator terms in combinatory logic.