#
# rules for quantifiers
# @todo denote metavariables correctly.
#
all x p(x) |= p(a)	# universal specialization
p(a) |= some x p(x)	# existential generalization
## some x p(x), ~occured(_a) |= p(_a)	# existential specialization (provided that _a is a new constant and has never occured yet)
~(all x p(x)) |= some x ~p(x)	# ~all~ conversion (even |=|)
~(all x ~p(x)) == some x p(x)	# ~all~ conversion (even |=|)
~(some x p(x)) |= all x ~p(x)	# ~some~ conversion (even |=|)
~(some x ~p(x)) == all x p(x)	# ~some~ conversion (even |=|)
all x (p(x)->q(x)) |= (all x p(x)) -> (all x q(x))
# some rules
some x (p(x) & q(x)) |= (some x p(x)) & (some x q(x))
#=# no e-resolution or paramodulation yet
#=#  (all y ((some x R(x,y)) & (some x all z (R(z,y)->(z=x))))) == (all y (some x (R(x,y) & (all z (R(z,y)->(z=x))))))	# there is at least one and at most one, is equivalent to there is exactly one
#
# axioms of set theory
#
# unique determination of "="
#=#  |= all x (x=x)		# ID1 axiom of identity. "=" reflexive
#=#  |= all x all y ((x=y) -> (p(x) -> p(y))) # ID2 principle of substitution (more general form: P(x) is an arbitrary formula containing the constant x, and P(y) = P(x)[x->y] is the result of a substitution of x by y)
#=#  (a=b), p(a) |= p(b)	# (specialized formulation)
#|= all M all N all x (x&isin;M <=> x&isin;N) -> M=N)	# EXT axiom of extensionality
#|= all M some N N = {x&isin;M | p(x)}	# AUS "Aussonderungsaxiome"
#|= all M some N all L (L&sube;M -> L&isin;N)	# POT axiom of potence set
#|= all M all N some L all x(x&isin;M | x&isin;N -> x&isin;L)	# &cup;-Ax axiom of union
# derived properties
#=#  |= all x all y ((x=y) -> (y=x))	# "=" symmetric
#=#  |= all x all y all z ((x=y) & (y=z) -> (x=z))	# "=" transitive
#=#  |= all x all y all z ((x=z) & (y=z) -> (x=y))	# "=" euclidian
#
# definitions
#
#N&sube;M := all x(x&isin;N -> x&isin;M)
#N&supe;M := M&sube;N
#|= all M all N (M=N <=> M&sube;N & N&sube;M)
#|= all M M&sube;M
#|= all x x&notin;&empty;
#|= all M &empty;&sube;M


#
# some relational implications
# @see Relations.html

# r asymmetric => r irreflexive
all a all b (r(a,b) => ~r(b,a)) |= all a ~r(a,a)
# r transitive and irreflexive => r asymmetric
all a all b all c (r(a,b)&r(b,c)=>r(a,c)) , all a ~r(a,a) |= all a all b (r(a,b)=>~r(b,a))
# r symmetric => (r Euclidean <=> r transitive)
####all a all b (r(a,b)=>r(b,a)) |= (all a all b all c (r(a,c)&r(b,c)->r(a,b))) <-> (all a all b all c (r(a,b)&r(b,c)->r(a,c))) # @fixme
# r reflexive and Euclidean <=> r equivalence
#   "<=" r equivalence => r reflexive and Euclidean
all a r(a,a) , all a all b (r(a,b)=>r(b,a)) , all a all b all c (r(a,b)&r(b,c)=>r(a,c)) |= (all a r(a,a)) & (all a all b all c (r(a,c)&r(b,c)=>r(a,b)))
#   "=>" r reflexive and Euclidean => r equivalence
#   "=>" (1) r reflexive and Euclidean => r reflexive
all a r(a,a) , all a all b all c (r(a,c)&r(b,c)=>r(a,b)) |= all a r(a,a)
#   "=>" (2) r reflexive and Euclidean => r symmetric
all a r(a,a) , all a all b all c (r(a,c)&r(b,c)=>r(a,b)) |= all a all b (r(a,b) => r(b,a))
#   "=>" (3) r reflexive and Euclidean => r transitive
all a r(a,a) , all a all b all c (r(a,c)&r(b,c)=>r(a,b)) |= all a all b all c (r(a,b)&r(b,c)=>r(a,c))
#   "=>" (1+2+3) r reflexive and Euclidean => r equivalence
all a r(a,a) , all a all b all c (r(a,c)&r(b,c)=>r(a,b)) |= (all a r(a,a)) & (all a all b (r(a,b) => r(b,a))) & (all a all b all c (r(a,b)&r(b,c)=>r(a,c))) # @fixme
