1. Axioms
This web page defines proofs for predicates about even and odd properties
for natural number multiplication. Labeled axioms for natural numbers,
their addition and multiplication, 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
t0 (t % 0 0)< (n %). ! n * 0 = 0
t1 (t %1 (s %2) %4)< (t %1 %2 %3), (p %1 %3 %4).
! n1 * (1+n2) = (n1+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 % $)< % .
1v1 (1v % $)< (1v $).
Abbreviations n, p, t, e, o, 1v, stand for
num, plus, times, even, odd, one_valid, respectively.
2. Multiplication Proofs
This section gives proofs of lemmas involving multiplication.
First we prove valid clauses that state that the
arguments and result of a multiplication predicate expression are
natural numbers:
t>n3 (n %3)< (t %1 %2 %3). - a multiplication result is a natural number
unfold cond t:
0 (n 0)< (n %). - conclu is valid, so proved
1 (n %3)< (t %1 %2' %3'), (p %1 %3' %3).
= valid clause p>n3 with added condition
t>n1 (n %1)< (t %1 %2 %3). - mult argument 1 is a natural num
unfold cond t:
0 (n %)< (n %). - tautology, proved
1 (n %1)< (t %1 %2' %3'), (p %1 %3' %3).
= vc p>n1 with added cond
t>n2 (n %2)< (t %1 %2 %3). - mult arg 2 is a natural num
unfold cond t:
0 (n 0)< (n %). - conclu valid, so proved
1 (n (s %2'))< (t %1 %2' %3'), (p %1 %3' %3).
= unfold of n1 with p>n2, with added cond
If a multiplication argument is even, the result is even:
te1>e3 (e %3)< (t %1 %2 %3), (e %1).
unfold cond t:
0 (e 0)< (n %), (e %). - conclu valid, so proved
1 (e %3)< (t %1 %2' %3'), (p %1 %3' %3), (e %1).
- conds 1, 3 and ind hyp gives added cond:
(e %3)< (t %1 %2' %3'), (p %1 %3' %3), (e %1), (e %3').
- conds 2,3,4 and vc pe1e2>e3 gives added cond:
(e %3)< (t %1 %2' %3'), (p %1 %3' %3), (e %1), (e %3'), (e %3).
- tautology, proved
te2>e3 (e %3)< (t %1 %2 %3), (e %2).
unfold cond t:
0 (e 0)< (n %), (e 0). - conclu valid, so proved
1 (e %3)< (t %1 %2' %3'), (p %1 %3' %3), (e (s %2')).
- unfold cond 3 wrt EOA
(e %3)< (t %1 %2' %3'), (p %1 %3' %3), (o %2').
unfold t
10 (e %3)< (n %), (p % 0 %3), (o 0). - cond 3 invalid, so proved
11 (e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3), (o (s %2")).
- unfold cond 4 wrt EOA
(e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3), (e %2").
- conds 1,4 and ind hyp gives added cond
(e %3)<(t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),(e %2"),(e %3").
- cond 2 and vc p>n1 gives added cond:
(e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %2"), (e %3"), (n %1).
- cond 6 and vc n>1veo gives added cond:
(e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %2"), (e %3"), (n %1), (1v (e %1) (o %1)).
unfold cond 7
0 (e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %2"), (e %3"), (n %1), (e %1).
- conds 2, 7, 5 and vc pe1e2>e3 gives added cond:
(e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %2"), (e %3"), (n %1), (e %1), (e %3').
- conds 3, 7, 8 and vc pe1e2>e3 gives added cond:
(e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %2"), (e %3"), (n %1), (e %1), (e %3'), (e %3).
- tautology, proved
1 (e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %2"), (e %3"), (n %1), (o %1).
- conds 2, 7, 5 and vc po1e2>o3 gives added cond:
(e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %2"), (e %3"), (n %1), (o %1), (o %3').
- conds 3, 7, 8 and vc po1o2>e3 gives added cond:
(e %3)< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %2"), (e %3"), (n %1), (o %1), (o %3'), (e %3).
- tautology, proved
If multiplication result is odd, then both arguments must be odd:
to3>o1 (o %1)< (t %1 %2 %3), (o %3).
unfold cond t:
0 (o %)< (n %), (o 0). - cond 2 not valid, so proved
1 (o %1)< (t %1 %2' %3'), (p %1 %3' %3), (o %3).
- cond 2 and vc p>n2 gives added cond:
(o %1)< (t %1 %2' %3'), (p %1 %3' %3), (n %3'), (o %3).
- cond 3 and vc n>1veo gives added cond:
(o %1)<(t %1 %2' %3'),(p %1 %3' %3),(n %3'),(1v (e %3') (o %3')),(o %3).
unfold cond 4
0 (o %1)<(t %1 %2' %3'),(p %1 %3' %3),(n %3'),(e %3'),(o %3).
- conds 2,4,5 and vc pe2o3>o1 gives added cond
(o %1)<(t %1 %2' %3'),(p %1 %3' %3),(n %3'),(e %3'),(o %3),(o %1).
- tautology, proved
1 (o %1)<(t %1 %2' %3'),(p %1 %3' %3),(n %3'),(o %3'),(o %3).
= ind hyp plus added conds - proved
to3>o2 (o %2)< (t %1 %2 %3), (o %3).
unfold cond t:
0 (o 0)< (n %), (o 0). - cond 2 not valid, so proved
1 (o (s %2'))< (t %1 %2' %3'), (p %1 %3' %3), (o %3).
unfold cond t:
0 (o (s 0))< (n %), (p % 0 %3), (o %3). - conclu valid, so proved
1 (o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),(o %3).
- cond 3 and vc p>n2 gives added cond
(o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),
(n %3'),(o %3).
- cond 4 and vc n>1veo gives added cond
(o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),
(n %3'),(1v (e %3') (o %3')),(o %3).
unfold cond 5:
0 (o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),
(n %3'),(e %3'),(o %3).
- conds 3,5,6 and vc pe2o3>o1 gives added cond
(o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),
(n %3'),(e %3'),(o %3),(o %1).
- conds 2,5,7 and vc po1e3>o2 gives added cond
(o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),
(n %3'),(e %3'),(o %3),(o %1),(o %3").
= unfold of o2 with ind hyp plus added conds, proved
1 (o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),
(n %3'),(o %3'),(o %3).
- conds 3,5,6 and vc po2o3>e1 gives added cond
(o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),
(n %3'),(o %3'),(o %3),(e %1).
- conds 2,5,7 and vc pe1o3>o2 gives added cond
(o (s (s %2")))< (t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),
(n %3'),(o %3'),(o %3),(e %1),(o %3").
= unfold of o2 with ind hyp plus added conds, proved
Recall that if a valid clause conclusion is not a valid expression,
such as the atom `not_valid, then the conditions of that clause can never
be valid. We use this property to assert that some even/odd
combinations for multiplication are not possible:
to1o2e3>nv `nv < (t %1 %2 %3), (o %1), (o %2), (e %3).
- odd times odd cannot give even result
unfold t
0 `nv < (n %), (o %), (o 0), (e 0).
- cond 3 cannot be valid, so proved
1 `nv < (t %1 %2' %3'), (p %1 %3' %3), (o %1), (o (s %2')), (e %3).
- unfold cond 4 wrt EOA:
`nv < (t %1 %2' %3'), (p %1 %3' %3), (o %1), (e %2'), (e %3).
- conds 2,1,3 and vc pe3o1>e2 give added cond:
`nv < (t %1 %2' %3'), (p %1 %3' %3), (o %1), (e %2'), (e %3), (o %3').
unfold t
10 `nv < (n %), (p % 0 %3), (o %), (e 0), (e %3), (o 0).
- cond 6 cannot be valid, so proved
11 `nv < (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3), (o %1),
(e (s %2")), (e %3), (o %3').
- unfold cond 5 wrt EOA:
`nv < (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3), (o %1),
(o %2"), (e %3), (o %3').
- conds 2,4,7 and vc po3o1>e2 give added cond:
`nv < (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3), (o %1),
(o %2"), (e %3), (o %3'), (e %3").
= ind hyp plus added conds - proved
to1e2o3>nv `nv < (t %1 %2 %3), (o %1), (e %2), (o %3).
- odd times even cannot give odd result
unfold t
0 `nv < (n %), (o %), (e 0), (o 0).
- cond 4 cannot be valid, so proved
1 `nv < (t %1 %2' %3'), (p %1 %3' %3), (o %1), (e (s %2')), (o %3).
- unfold cond 4 wrt EOA
`nv < (t %1 %2' %3'), (p %1 %3' %3), (o %1), (o %2'), (o %3).
- conds 2,3,5 and vc po3o1>e2 give added cond:
`nv < (t %1 %2' %3'), (p %1 %3' %3), (o %1), (o %2'), (o %3), (e %3').
- conds 1,3,6 and vc to1o2e3>nv give added cond:
`nv < (t %1 %2' %3'),(p %1 %3' %3),(o %1),(o %2'),(o %3),(e %3'), `nv .
- cond 7 cannot be valid, so proved
te1o2o3>nv `nv < (t %1 %2 %3), (e %1), (o %2), (o %3).
- even times odd cannot give odd result
unfold t
0 `nv < (n %), (e %), (o 0), (o 0).
- conds 3 & 4 cannot be valid, so proved
1 `nv < (t %1 %2' %3'), (p %1 %3' %3), (e %1), (o (s %2')), (o %3).
- unfold cond 4 wrt EOA
`nv < (t %1 %2' %3'), (p %1 %3' %3), (e %1), (e %2'), (o %3).
- conds 2,3,5 and vc po3e1>o2 gives added cond:
`nv < (t %1 %2' %3'), (p %1 %3' %3), (e %1), (e %2'), (o %3), (o %3').
unfold t
10 `nv < (n %), (p % 0 %3), (e %), (e 0), (o %3), (o 0).
- cond 6 cannot be valid, so proved
11 `nv < (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %1), (e (s %2")), (o %3), (o %3').
- unfold cond 5 wrt EOA
`nv < (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %1), (o %2"), (o %3), (o %3').
- conds 2,4,7 and vc po3e1>o2 gives added cond:
`nv < (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %1), (o %2"), (o %3), (o %3'), (o %3").
= ind hyp plus added conds - proved
te1e2o3>nv `nv < (t %1 %2 %3), (e %1), (e %2), (o %3).
- even times even cannot give odd result
unfold t
0 `nv < (n %), (e %), (e 0), (o 0).
- cond 4 cannot be valid, so proved
1 `nv < (t %1 %2' %3'), (p %1 %3' %3), (e %1), (e (s %2')), (o %3).
- unfold cond 4 wrt EOA
`nv < (t %1 %2' %3'), (p %1 %3' %3), (e %1), (o %2'), (o %3).
- conds 2,3,5 and vc gives added cond:
`nv < (t %1 %2' %3'), (p %1 %3' %3), (e %1), (o %2'), (o %3), (o %3').
- conds 1,3,4,6 and vc te1o2o3>nv gives added cond
`nv < (t %1 %2' %3'),(p %1 %3' %3),(e %1),(o %2'),(o %3),(o %3'), `nv .
- cond 7 cannot be valid, so proved
If multiplication result is even, at least one argument must be even:
te3o2>e1 (e %1)< (t %1 %2 %3), (e %3), (o %2).
unfold cond t
0 (e %)< (n %), (e 0), (o 0).
- cond 3 is not valid, so proved
1 (e %1)< (t %1 %2' %3'), (p %1 %3' %3), (e %3), (o (s %2')).
unfold cond 4 (wrt EOA axioms)
(e %1)< (t %1 %2' %3'), (p %1 %3' %3), (e %3), (e %2').
unfold cond t
0 (e %)< (n %), (p % 0 %3), (e %3), (e 0).
- unfold cond 2
(e %)< (n %), (n %), (e %), (e 0). - tautology, so proved
1 (e %1)<(t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),(e %3),
(e (s %2")).
- unfold cond 5
(e %1)<(t %1 %2" %3"),(p %1 %3" %3'),(p %1 %3' %3),(e %3),
(o %2").
= ind hyp plus added conds, proved
te3o1>e2 (e %2)< (t %1 %2 %3), (e %3), (o %1).
unfold cond t
0 (e 0)< (n %), (e 0), (o %). - conclu is valid, so proved
1 (e (s %2'))< (t %1 %2' %3'), (p %1 %3' %3), (e %3), (o %1).
unfold cond t
0 (e (s 0))< (n %), (p % 0 %3), (e %3), (o %).
unfold cond p
(e (s 0))< (n %), (n %), (e %), (o %).
- conds 3,4 and vc eo>nv gives added cond
(e (s 0))< (n %), (n %), (e %), (o %), `nv.
- cond 5 not valid, so proved
1 (e (s (s %2")))< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %3), (o %1).
- conds 3,4,5 and vc pe3o1>o2 gives added cond
(e (s (s %2")))< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %3), (o %1), (o %3').
- cond 2,5,6 and vc pe3o2>e2 gives added cond
(e (s (s %2")))< (t %1 %2" %3"), (p %1 %3" %3'), (p %1 %3' %3),
(e %3), (o %1), (o %3'), (e %3").
= unfold e>e with ind hyp plus added conds, proved
If multiplication result is even, at least one argument must be even:
te3>1ve1e2 (1v (e %1) (e %2))< (t %1 %2 %3), (e %3).
- cond 1 and vc t>n1 give added cond:
(1v (e %1) (e %2))< (t %1 %2 %3), (e %3), (n %1).
- cond 3 and vc n>1veo give added cond:
(1v (e %1) (e %2))< (t %1 %2 %3), (e %3), (n %1), (1v (e %1) (o %1)).
unfold cond 4:
0 (1v (e %1) (e %2))< (t %1 %2 %3), (e %3), (n %1), (e %1).
= unfold 1v0 with cond 4 tautology - proved
1 (1v (e %1) (e %2))< (t %1 %2 %3), (e %3), (n %1), (o %1).
= unfold 1v1 with te3o1>e2 - proved
-- end of multiplication proofs --