I am looking for secondary literature on a formal propositional calculus which has the NAND connective as its sole connective.
I am coming upon many pages which briefly state that Nicod had shown that propositional logic could be done with 1 axiom using only the NAND connective, and one inference rule. These are given, but then that is it. There are some books which go into it a bit, but kind of only on the surface and not as much as I'm looking for.
None of these pages actually go into this proof at all, or how the axiom and inference rule were found. Nor do they go into any theorems about the system.
I am looking into the history of the NAND/NOR connectives and would like to explore a system which uses only one of those, but I am having trouble finding decent material. Of course, there is the paper written by Nicod himself and the earlier one by Sheffer, but I am wondering if there are any explanatory papers/websites that go into more detail and explanation.
Thanks
Nicod's paper actually didn't prove his axiom complete. Thomas Scharle wrote a paper which provides a proof of completeness with some discussion of the history of this problem. Scharle's paper also has relevance for exploring a system with only a NOR connective, a single rule of inference, and a (relatively short) single axiom. It's all in Polish notation, with D standing for NAND, S for NOR, K for conjunction, N for negation, C for implication, and A for disjunction.