#
# Huntington axioms of the logic of Boolean algebra
#
a&b == b&a		# commutative (Huntington axiom)
a|b == b|a		# commutative (Huntington axiom)
(a&b)|c == (a|c)&(b|c)	# distributive (Huntington axiom)
(a|b)&c == (a&c)|(b&c)	# distributive (Huntington axiom)
a&true == a		# neutral element (Huntington axiom)
a|false == a		# neutral element (Huntington axiom)
a&~a == false		# complement (Huntington axiom) induces Principium contradictionis
a|~a == true		# complement (Huntington axiom) induces Tertium non datur, law of excluded middle (Russel/Whitehead. Principia Mathematica. 1910, 101 *2.11)
#
# alternative form of Huntington axioms (from Huntington[33b] and [33a])
# for the logic basis (~,|)
#
a|b == b|a		# commutative (Huntington axiom)
(a|b)|c == a|(b|c)	# associative
~(~a|b) | ~(~a|~b) == a	# Hungtington3
#
# Robbins algebra (after 1990 proven to be equivalent to alternative Huntington axioms)
# for the logic basis (~,|)
#
a|b == b|a		# commutative (Huntington axiom)
(a|b)|c == a|(b|c)	# associative
~(~(a|b) | ~(a|~b)) == a	# Robbins Algebra axiom3
#
# laws derived from Huntington axioms
#
(a&b)&c == a&(b&c)	# associative
(a|b)|c == a|(b|c)	# associative
a&a == a		# idempotent
a|a == a		# idempotent
a&(a|b) == a		# absorbtion
a|(a&b) == a		# absorbtion <=(a),(c),(idem)
~(~a) == a		# involution "duplex negatio est affirmatio". (induces duality forall a exists b: b = ~a. dualities: a ~a, & |)
~(a&b) == ~a|~b		# deMorgan
~(a|b) == ~a&~b		# deMorgan
a&false == false	# (dual to neutral element)
a|true == true		# (dual to neutral element)
#
# additional equivalences
#
a->b == ~b->~a		# contra positition [Lex contrapositionis]
a->b == ~a|b		# material implication
~(a->b) == a&~b		# negated implication
a->b == ~(a&~b)
|= a<->a		# reflexive
a<->b == b<->a		# commutative
(a<->b)<->c == a<->(b<->c)	# associative
a<->b == (a->b)&(b->a)	# coimplication (alias '<->' introduction or elimination)
a<->b == (a&b) | (~a&~b)	# equivalence in DNF
a<->b == (a|~b) & (~a|b)	# equivalence in CNF
~a<->b == a<->~b	# "~ behaves like scalar-multiplication in scalar-product"
~a<->b == ~(a<->b)	# "~ behaves like scalar-multiplication in scalar-product"
a^b == ~(a<->b)		# "duality" of equivalence and antivalence
a^b == ~a<->b		#
a^b == b^a		# commutative
a^b == (a&~b) | (~a&b)	# antivalence in DNF
a^b == (a|b) & (~a|~b)	# antivalence in CNF
a^a == false
(a^b)^c == a^(b^c)	# associative
(a^b)^c == a<->b<->c	#
(a->b)->c == a->b && b->c
a&b->c == a->(b->c)	# exportation / importation [Lex exportationis, Lex importationis]
~a == a->false		# not in INF
~a == a<->false		# not with equivalence
#
# some important tautologies from axioms
#
|= ~(a&~a)		# Principium contradictionis
|= a | ~a		# tertium non datur, law of excluded middle (Russel/Whitehead. Principia Mathematica. 1910, 101 *2.11)
|= a -> a		# self implication (c reflexive)
#
# implicative properties of |= and thus inference rules
#
p->q, p |= q		# Modus (ponendo) ponens	 (resp. assuming p->q, p is sufficient for q. repeated application is forward chaining)
p->q, ~q |= ~p		# Modus (tollendo) tollens (resp. assuming p->q, q is necessary for p. repeated application is backward chaining)
p->q, q->r |= p->r	# hypothetical "syllogism" Principle of Syllogism (due to affinity to mode Barbara)
p|q, ~p |= q		# disjunctive "syllogism"
p, q |= p&q		# conjunction
p |= p|q		# weakening addition (alias '|' introduction)
p&q |= p		# weakening subtraction (alias '&' elimination)
a |= b->a		# weakening conditional
a->b, b->c |= a->c	# transitivity
#
# tautological properties of == aka |=| (thus inference rules, as well)
#
p->~p == ~p
(p->q), (p->r) == p->(q&r)
p->(q->r) == (p&q)->r	# chain rule
p->(q->r) == (p&q)->r	# distribute
p->(q->r) == (p->q)->(p->r)	# distributive
# Rules for quantifiers
# some rules
p->(p->q) |= p->q	# rule of reduction
p->(q->r) |= q->(p->r)	# Law of Permutation, the 'commutative principle' (Russel/Whitehead. Principia Mathematica. 1910, 99 *2.04)
~p->p |= p		# consequentia mirabilis
(p->r), (q->s) |= (p&q)->(r&s)	# Praeclarum Theorema
|= p->(q->p)		# principle of simplification (Russel/Whitehead. Principia Mathematica. 1910, 100 *2.03)
|= p->p			# principle of identity (Russel/Whitehead. Principia Mathematica. 1910, 101 *2.08)
|= p->~~p		# Affirmatio est duplex negatio, principle of double negation (Russel/Whitehead. Principia Mathematica. 1910, 101 f)
|= ~~p->p		# Duplex negatio est affirmatio, principle of double negation (Russel/Whitehead. Principia Mathematica. 1910, 101 f)
false |= a		# 'ex falso quodlibet'
#
# some less important
#
# diverse
p|q == ~p->q		# | as ~,->
p&q == ~(p->~q)		# & as ~,->
~p->p == p		# self proof
p->~p |= ~p		# self contradiction
p->q, ~p->q |= q	# reasoning by cases
~(p->q) == p&~q		# negative implication
~(p<->q) == (p|q)&(~p|~q) # negative equivalence
~(p<->q) == p<->~q
p<->~q == ~p<->q
p->q |= (p|r)->(q|r)
p->r, q->r |= (p|q)->r
|= (f->g) | (g->f)	# material implication has strange causal relations
#
# definitions
#
#X!=Y == ~(X=Y)
# a nor b == ~(a|b)		# Peirce function
# a nand b == ~(a&b)	