1. Axioms
This web page defines proofs for predicates about even and odd properties
for natural number addition. Labeled axioms for natural numbers,
their addition, the even/odd property,
and some higher-order forms, are repeated here, with predicate names
abbreviated for conciseness:
Axioms:
n0 (n 0). ! 0 is a natural number
n1 (n (s %))< (num %). ! successor of a nat num is a nat num
p0 (p % 0 %)< (n %). ! n + 0 = n
p1 (p %1 (s %2) (s %3))< (p %1 %2 %3). ! n1 + 1+n2 = 1+n3 if n1+n2=n3
! axiom subset EOA for even and odd natural numbers:
e0 (e 0).
e>o (o (s %e))< (e %e).
o>e (e (s %o))< (o %o).
! equivalent axiom subset EOB for even and odd predicates:
e0 (e 0).
e>e (e (s (s %e)))< (e %e).
o1 (o (s 0)).
o>o (o (s (s %o)))< (o %o).
! at least one expression in list of two is a valid expression:
1v0 (1v %v %)< %v .
1v1 (1v % %v)< %v .
Abbreviations n, p, e, o, 1v, stand for
num, plus, even, odd, one_valid, respectively.
2. Addition Proofs
This section gives proofs of lemmas involving addition.
First we prove valid clauses that state that the arguments and result
of an addition predicate expression are natural numbers:
The result of natural number addition is a natural number:
p>n3 (n %3)< (p %1 %2 %3).
unfold cond p:
0 (n %)< (n %). - tautology, proved
1 (n (s %3'))< (p %1 %2' %3').
= unfold of n1 with ind hyp, proved
p>n1 (n %1)< (p %1 %2 %3).
unfold cond p:
0 (n %)< (n %). - tautology, proved
1 (n %1)< (p %1 %2' %3').
= ind hyp, proved
p>n2 (n %2)< (p %1 %2 %3).
unfold cond p:
0 (n 0)< (n %). - conclu valid, proved
1 (n (s %2'))< (p %1 %2' %3').
= unfold of n1 with ind hyp, proved
Given two addition even/odd-ness properties, we know the third:
pe1e2>e3 (e %3)< (p %1 %2 %3), (e %1), (e %2).
-- addition of two even numbers gives an even number result
unfold p cond:
0 (e %)< (n %), (e %), (e 0). - tautology, proved
1 (e (s %3'))< (p %1 %2' %3'), (e %1), (e (s %2')).
unfold p cond:
0 (e (s %))< (n %), (e %), (e (s 0)).
- unfold cond 3 twice yields no matches, so cond 3 invalid, proved
1 (e (s (s %3")))< (p %1 %2" %3"), (e %1), (e (s (s %2"))).
- unfold cond 3 wrt EOB axioms:
(e (s (s %3")))< (p %1 %2" %3"), (e %1), (e %2").
= unfold of valid clause e>e with ind hyp pe1e2>e3 - proved
po1o2>e3 (e %3)< (p %1 %2 %3), (o %1), (o %2).
-- addition of two odd numbers gives an even number result
unfold p cond:
0 (e %)< (n %), (o %), (o 0).
- unfold cond 3 yields no matches, so invalid - proved
1 (e (s %3'))< (p %1 %2' %3'), (o %1), (o (s %2')).
unfold p cond:
0 (e (s %))< (n %), (o %), (o (s 0)).
= vc o>e with added conds - proved
1 (e (s (s %3")))< (p %1 %2" %3"), (o %1), (o (s (s %2"))).
unfold cond 3 wrt EOB axioms:
(e (s (s %3")))< (p %1 %2" %3"), (o %1), (o %2").
= unfold of vc e>e w ind hyp po1o2>e3 - proved
pe1o2>o3 (o %3)< (p %1 %2 %3), (e %1), (o %2).
-- addition of even and odd numbers yields an odd number result
unfold p cond:
0 (o %)< (n %), (e %), (o 0). - cond 3 invalid - proved
1 (o (s %3'))< (p %1 %2' %3'), (e %1), (o (s %2')).
unfold p cond:
0 (o (s %))< (n %), (e %), (o (s 0)).
= vc e>o plus added conds - proved
1 (o (s (s %3")))< (p %1 %2" %3"), (e %1), (o (s (s %2"))).
- unfold cond 3 wrt EOB
(o (s (s %3")))< (p %1 %2" %3"), (e %1), (o %2").
- unfold of o>o w ind hyp pe1o2>o3 - proved
po1e2>o3 (o %3)< (p %1 %2 %3), (o %1), (e %2).
unfold p cond:
0 (o %)< (n %), (o %), (e 0). - tautology, proved
1 (o (s %3'))< (p %1 %2' %3'), (o %1), (e (s %2')).
unfold p cond:
0 (o (s %))< (n %), (o %), (e (s 0)).
- unfold cond 3 twice gives no matches - invalid - proved
1 (o (s (s %3")))< (p %1 %2" %3"), (o %1), (e (s (s %2"))).
- unfold cond 3 wrt EOB
(o (s (s %3")))< (p %1 %2" %3"), (o %1), (e %2").
= unfold of o>o w ind hyp po1e2>o3 - proved
Given even/odd value of addition result and one argument, we know the
value of the other argument:
pe3e1>e2 (e %2)< (p %1 %2 %3), (e %1), (e %3).
unfold p cond:
0 (e 0)< (n %), (e %), (e %). - conclu valid - proved
1 (e (s %2'))< (p %1 %2' %3'), (e %1), (e (s %3')).
unfold p cond:
0 (e (s 0))< (n %), (e %), (e (s 0)).
- unfold cond 2 twice gives no matches - invalid - proved
1 (e (s (s %2")))< (p %1 %2" %3"), (e %1), (e (s (s %3"))).
- unfold cond 3 w EOB ax:
(e (s (s %2")))< (p %1 %2" %3")< (e %1), (e %3").
= unfold of e>e with ind hyp pe3e1>e2 - proved
pe3e2>e1 (e %1)< (p %1 %2 %3), (e %2), (e %3).
unfold p cond:
0 (e %)< (n %), (e 0), (e %). - tautology - proved
1 (e %1)< (p %1 %2' %3'), (e (s %2')), (e (s %3')).
unfold p cond:
0 (e %)< (n %), (e (s 0)), (e (s %)).
- unfold cond 2 twice shows it invalid - proved
1 (e %1)< (p %1 %2" %3"), (e (s (s %2"))), (e (s (s %3"))).
- unfold cond 2 wrt EOB:
(e %1)< (p %1 %2" %3"), (e %2"), (e (s (s %3"))).
- unfold cond 3 wrt EOB:
(e %1)< (p %1 %2" %3"), (e %2"), (e %3").
= ind hyp pe3e2>e1 - proved
pe3o1>o2 (o %2)< (p %1 %2 %3), (o %1), (e %3).
unfold p cond:
0 (o 0)< (n %), (o %), (e %).
- conds 2,3 and vc eo>nv give added cond:
(o 0)< (n %), (o %), (e %), `nv.
- cond 4 invalid - proved
1 (o (s %2'))< (p %1 %2' %3'), (o %1), (e (s %3')).
unfold p cond:
0 (o (s 0))< (n %), (o %), (e (s %)).
- conclu valid - proved
1 (o (s (s %2")))< (p %1 %2" %3"), (o %1), (e (s (s %3"))).
- unfold cond 3 w EOB ax:
(o (s (s %2")))< (p %1 %2" %3")< (o %1), (e %3").
= unfold of o>o with ind hyp pe3o1>o2 - proved
pe3o2>o1 (o %1)< (p %1 %2 %3), (o %2), (e %3).
unfold p cond:
0 (o %)< (n %), (o 0), (e %). - cond 2 invalid - proved
1 (o %1)< (p %1 %2' %3'), (o (s %2')), (e (s %3')).
unfold p cond:
0 (o %)< (n %), (o (s 0)), (e (s %)).
= vc e1>o plus added conds - proved
1 (o %1)< (p %1 %2" %3"), (o (s (s %2"))), (e (s (s %3"))).
- unfold conds 2 and 3 wrt EOB:
1 (o %1)< (p %1 %2" %3"), (o %2"), (e %3").
= ind hyp pe3o2>o1 - proved
po3e1>o2 (o %2)< (p %1 %2 %3), (e %1), (o %3).
unfold p cond:
0 (o 0)< (n %), (e %), (o %).
- conds 2,3 and vc eo>nv give added cond:
(o 0)< (n %), (e %), (o %), `nv.
- cond 4 is invalid - proved
1 (o (s %2'))< (p %1 %2' %3'), (e %1), (o (s %3')).
unfold p cond:
0 (o (s 0))< (n %), (e %1), (o (s %)).
- conclu is valid - proved
1 (o (s (s %2")))< (p %1 %2" %3"), (e %1), (o (s (s %3"))).
- unfold cond 3 w ax EOB
(o (s (s %2")))< (p %1 %2" %3"), (e %1), (o %3").
= unfold o>o w ind hyp - proved
po3e2>o1 (o %1)< (p %1 %2 %3), (e %2), (o %3).
unfold p cond:
0 (o %)< (n %), (e 0), (o %). - tautology - proved
1 (o %1)< (p %1 %2' %3'), (e (s %2')), (o (s %3')).
unfold p cond:
0 (o %)< (n %), (e (s 0)), (o (s %)).
- cond 2 not valid - proved
1 (o %1)< (p %1 %2" %3"), (e (s (s %2"))), (o (s (s %3"))).
- unfold conds 2 and 3 w ax EOB
(o %1)< (p %1 %2" %3"), (e %2"), (o %3").
= ind hyp po3e2>o1 - proved
po3o1>e2 (e %2)< (p %1 %2 %3), (o %1), (o %3).
unfold p cond:
0 (e 0)< (n %), (o %), (o %). - conclu valid - proved
1 (e (s %2'))< (p %1 %2' %3'), (o %1), (o (s %3')).
unfold p cond:
0 (e (s 0))< (n %), (o %), (o (s %)).
- conds 2,3 and vc oo1>nv give added cond:
(e (s 0))< (n %), (o %), (o (s %)), `nv.
- cond 4 is invalid - proved
1 (e (s (s %2")))< (p %1 %2" %3"), (o %1), (o (s (s %3"))).
- unfold cond 3 w ax EOB
(e (s (s %2")))< (p %1 %2" %3"), (o %1), (o %3").
= unfold of e>e with ind hyp po3o1>e2 - proved
po3o2>e1 (e %1)< (p %1 %2 %3), (o %2), (o %3).
unfold p cond:
0 (e %)< (n %), (o 0), (o %). - cond 2 invalid - proved
1 (e %1)< (p %1 %2' %3'), (o (s %2')), (o (s %3')).
unfold p cond:
0 (e %)< (n %), (o (s 0)), (o (s %)).
- unfold cond 3 w ax EOA
(e %)< (n %), (o (s 0)), (e %).
- tautology - proved
1 (e %1)< (p %1 %2" %3"), (o (s (s %2"))), (o (s (s %3"))).
- unfold cond 2 and 3 wrt ax EOB
(e %1)< (p %1 %2" %3"), (o %2"), (o %3").
= ind hyp po3o2>e1 - proved
-- end of addition proofs --