#
# huntington axioms of boolean algebraic logic
#
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)
#inconsistent 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)
#
# 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|(a&b) == a		# (Verschmelzung...) <=(a),(c),(idem)
a&(a|b) == a		# (Verschmelzung...)
#inconsistent ~(~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
#inconsistent a&false == false	# (dual to neutral element)
# inconsistent 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
a->b == ~(a&~b)
a<->b == b<->a		# commutative
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)
a^b == a&~b | ~a&b	# antivalence in DNF
a^b == (a|b) & (~a|~b)	# antivalence in CNF
#inconsistent a^a == false
# substitutionBug (a^b)^c == a^(b^c)	# associative
(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
#
# some important tautologies from axioms
#
# contradiction query |= ~(a&~a)		# Principium contradictionis
# contradiction query |= a | ~a		# Tertium non datur, law of excluded middle (Russel/Whitehead. Principia Mathematica. 1910, 101 *2.11)
# contradiction query |= 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)
#inconsistent |= p->p			# principle of identity (Russel/Whitehead. Principia Mathematica. 1910, 101 *2.08)
#inconsistent |= p->~~p		# Affirmatio est duplex negatio, principle of double negation (Russel/Whitehead. Principia Mathematica. 1910, 101 f)
#inconsistent |= ~~p->p		# Duplex negatio est affirmatio, principle of double negation (Russel/Whitehead. Principia Mathematica. 1910, 101 f)
#inconsistent false |= a		# 'ex falso quodlibet'
#
# some less important
#
# diverse
p|q == ~p->q		# | as ~,->
p&q == ~(p->~q)		# & as ~,->
#inconsistent? ~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->s) |= (p&q)->(r&s)	# Praeclarum Theorema
p->r, q->r |= (p|q)->r
|= (f->g) | (g->f)	# material implication has strange causal relations
#
# definitions
#
##no e-resolution or paramodulation yet
#=#   x!=y == ~(x=y)

#
# quantifiers
#

$x p(x) |= p(a)
$x p(x) |= $y p(y)
$x p(x) |= $x p(x)

# skolemized form (original form see semantic-pl.txt)

# rules for quantifiers
# @todo denote metavariables correctly.
#
$ x p(x) |= p(a)	#  universal specialization
#@fixme p(a) |= p(s)	# existential generalization  #@fixme doesn't work since when?
~($x p(x)) |= ~p(xp)	# ~all~ conversion (even |=|)
#~some p(x) |= $x ~p(x)	# ~some~ conversion (even |=|)
$x (p(x)->q(x)) |= ($x p(x)) -> ($x q(x))
# some rules
(p(x) & q(x)) |= (p(x)) & (q(x))
