The paper assumes right associativity of both → and ⊃ but that suppresses the visible symmetries with which I learned these formulae. Reinstating some parens we have:
K = λx.(λy.x)
S = λx.(λy.(λz.((xz)(yz))))
P ⊃ (Q ⊃ P)
(P ⊃ (Q ⊃ R)) ⊃ ((P ⊃ Q) ⊃ (P ⊃ R))
A → (B → A)
(A → (B → C)) → ((A → B) → (A → C))
The 2nd correspondence may not be entirely obvious so we ask OCaml:
# fun x -> (fun y -> (fun z -> ((x z) (y z))));; - : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>OCaml and the authors think that it is obvious. According to them it is rooted in the Curry-Howard isomorphism too.
The paper refers to the two implication formulae as axioms for implication.
I recall that the following tautology can not be deduced from them with modus-ponens:
(((A ⊃ B) ⊃ A) ⊃ A)
That was a theorem but required another axiom such as (¬A ⊃ ¬B) ⊃ (B ⊃ A). Wikipedia says that only the ‘intuitionistic implicational logic’ pare produced thus and I think the above tautology is not a theorem there.