We combine a variety of constructive methods (including forcing, realizability, asymmetric interpretation), to obtain consistency results concerning combinatory logic with extensionality and (forms of) the axiom of choice.