3 ms·
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
by superobserver 10y ago
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 10y agoRather 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 10y agoYes, 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 10y agoIf you use DeMorgan's law on your result, you can simplify it further to ~A | B