 Providing a sound and complete semantics for NL is an open problem in connexive logic. Angell’s (1962) axiomatic proof system PA1 can also be seen as belonging to the proof-theoretical tradition because it is incomplete with respect the truth tables presented by Angell. However, Angell proved PA1 to be sound with respect to these truth tables, thereby for the first time presenting a non-triviality proof for a formal system of connexive logic. Providing an intuitive sound and complete semantics for PA1 is another open problem in connexive logic. (Routley [1978, p. 409] admits that his characterization is “not intuitively very satisfying: as it stands the modelling is rather complex, with the modelling conditions exceeding in number the postulates they model, and basic connexive postulates like Boethius, instead of being validated in a natural way, have fairly intractable conditions.”)