[keenerd]

> Two of them are special: NOR and NAND.

No, IMP does this as well. It has mostly been useful for memristor logic.

    A B   IMP
    0 0    1
    0 1    1
    1 0    0
    1 1    1

I have a suspicion there is a more general mathematical law that says any boolean rule with a 1-of-4 split (either exactly one true or exactly one false) can be used for general computation, if you can make a NOT gate out of it. (Since AND/OR obviously is not workable.) So there should be six possible universal logic gates.

[superobserver]

IMP is really NOT( A AND NOT ( B ) )

A → B |- ~(A & ~B)

1) A → B [by assumption] 1

2) A & ~B [by assumption] 2

3) A [conj. elim. 2] 2

4) B [imp by 1,2] 1,2

5) ~B [conj. elim 2] 2

6) B & ~B [conj 4,5] 1,2

7) ~(A & ~B) [reductio ad absurdum 2,6] 1

{Thus by assuming only A → B we prove that we can derive ~(A & ~B).}

From there you can also trivially prove that ~(A & ~B) |- A → B; thus, they are tautologous and so given the primitives ~ and &, implication is not quite as "special" for a Universal Turing machine. This is merely to show, independent of any construction using only IMP, one can trivially reduce it to more primitive components, thus undermining any claim to a "special" status in the context of universal computation.

[kmill]

Rather than deducing it, you can also look at the truth table, see it is 0 exactly where B is not true and A is true, and get not(A and not B). Then, we can conclude there is a proof such as yours from the completeness theorem, I believe.

[superobserver]

Yes, but it's more fun and edifying to prove it. :) It's so rare I get an opportunity to whip out propositional logic and formal proof methods that I hardly balk at the opportunity. (hears groans from non-nerds)

[Breakthrough]

If you use DeMorgan's law on your result, you can simplify it further to ~A | B

[VLM]

The rule relies inductively on proving a nand (or nor or any one of them in the class) is a universal computer, then any other gate where you can hardwire an input to construct an inverter can be treated as that universal gate with some combination of the previously mentioned inverters slapped on inputs and/or output. I don't remember the details either, LOL, but that was the general gist of it, if you can make inverters out of an alternative then you can slap enough inverters on it to make a NAND eventually.

[zamalek]

(Not A) or B, to save others the search.

[jwilk]

IMP alone is not enough to construct a gate that always outputs 0.