K = λxy.x

S = λxyz.((xz)(yz))

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

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.

what is the type of S = λx.(λy.(λz.((xz)(yz)))) ?

To see that it is (A → (B → C)) → ((A → B) → (A → C))

We presume that the type of x is (A → (B → C)) in (λy.(λz.((xz)(yz))))

We then presume that the type of y is (A → B) in (λz.((xz)(yz)))

and then that the type of z is A in ((xz)(yz))

We note then, using first presumption, that the type of (xz) is (B → C)

Likewise we see that the type of (yz) is B.

We see thus that the type of ((xz)(yz)) is C.

Q.E.D.