1. Introduction
Axiomatic language starts at the most fundamental, symbolic level --
even arithmetic is not built-in. The concept of even and odd
for natural numbers must also be defined. This web page defines
some simple proofs relating to even and odd numbers.
We first need the following labeled axioms for natural numbers in successor notation and their addition and multiplication:
Natural numbers and their addition and multiplication:
n0: (num 0). ! 0 is a natural number
n1: (num (s %))< (num %). ! successor of a nat num is a nat num
p0: (plus % 0 %)< (num %). ! n + 0 = n
p1: (plus %1 (s %2) (s %3))< (plus %1 %2 %3). ! n1 + 1+n2 = 1+n3 if n1+n2=n3
t0: (times % 0 0)< (num %). ! n * 0 = 0
t1: (times %1 (s %2) %4)< (times %1 %2 %3), (plus %1 %3 %4).
! n1 * (1+n2) = (n1+n3) if n1 * n2 = n3
sq: (sqr %n %nsqr)< (times %n %n %nsqr). ! square of a natural number
Note that we also have an axiom "sq" that defines a function for the square of a natural number.
For these proofs we will also use a higher-order form "one_valid"
that states that at least one expression in a list of two expressions
is a valid expression:
At least one expression in list is a valid expression:
1v0: (one_valid %v %)< %v .
1v1: (one_valid % %v)< %v .
2. Even/Odd Axioms
We use "even" and "odd" predicates to designate even and odd natural numbers. The following set of axioms "EOA" gives one definition
for these predicates:
Axiom set EOA for even and odd natural numbers:
e0: (even 0).
e>o: (odd (s %e))< (even %e).
o>e: (even (s %o))< (odd %o).
It will also be helpful in proofs below to have this equivalent set of "EOB"
axioms for the even and odd predicates:
Alternative axiom set EOB for even and odd:
e0: (even 0).
e>e: (even (s (s %e)))< (even %e).
o1: (odd (s 0)).
o>o: (odd (s (s %o)))< (odd %o).
We need to show that these two axiom sets, EOA and EOB, are equivalent -- that is, they generate the same set of even/odd valid expressions.
We first show that each of the EOB axioms is a valid clause with respect to axiom set EOA:
EOB axioms are valid clauses wrt axiom set EOA:
e0 (even 0).
= axiom e0 of EOA -- proved
o1 (odd (s 0)).
= unfold of EOA axiom e>o with e0 -- proved
e>e (even (s (s %e)))< (even %e).
= unfold EOA o>e with e>o -- proved
o>o (odd (s (s %o)))< (odd %o).
= unfold EOA e>o with o>e -- proved
Now we show that each EOA axiom is a valid clause with respect to axiom set
EOB:
EOA axioms are valid clauses wrt axiom set EOB:
e0 (even 0).
= axiom e0 of EOB -- proved
e>o (odd (s %e))< (even %e).
unfold cond 1 (wrt EOB axioms):
0 (odd (s 0)).
= axiom o1 -- proved
1 (odd (s (s (s %e))))< (even %e).
= unfold of o>o wrt induction hypothesis e>o -- proved
o>e (even (s %o))< (odd %o).
unfold:
0 (even (s (s %0))).
= e>e unfolded with e0 -- proved
1 (even (s (s (s %o))))< (odd %o).
= unfold of e>e wrt induction hypothesis o>e -- proved
Since each axiom of one set is a valid clause with respect to the other set, the two axiom sets EOA and EOB are equivalent.
3. Some Supporting Proofs
The following valid clauses define valid expressions for useful
even/odd constants:
Valid clauses for some constant even/odd valid expressions:
o1 (odd (s 0)). = unfold of e>o instance with e0
e2 (even (s (s 0))). = unfold of o>e with o1
o3 (odd (s (s (s 0)))). = unfold of e>o with e2
... ...
We will also make use of the following expressions, which can be shown
to be non-valid:
Invalid even/odd expressions:
(odd 0) -- zero is not odd
(even (s 0)) -- one is not even
(odd (s (s 0))) -- two is not odd
... ...
The following valid clauses use "one_valid":
Both "one_valid" expressions are the same:
1vxx>x % < (one_valid % %).
unfold:
0 % < % . - tautology - proved
1 % < % . - tautology - proved
Successor of even or odd number:
1vseo (one_valid (even (s %)) (odd (s %)))< (one_valid (even %) (odd %)).
unfold:
0 (one_valid (even (s %)) (odd (s %)))< (even %).
= unfold of 1v1 with e>o - proved
1 (one_valid (even (s %)) (odd (s %)))< (odd %).
= unfold of 1v0 with o>e - proved
Every natural number is either even or odd:
n>eo (one_valid (even %) (odd %))< (num %).
unfold:
0 (one_valid (even 0) (odd 0)).
= unfold of 1v0 with e0 - proved
1 (one_valid (even (s %)) (odd (s %)))< (num %).
= unfold of 1vseo with induction hypothesis n>eo - proved
The atom `not_valid is not a valid expression generated by the
above axioms. Thus, if a valid clause has this `not_valid atom as a
conclusion, then no instance of its conditions can be valid
expressions. We use this convention to prove that certain
even/odd properties are not possible:
A number and its successor cannot both be even:
ese>nv `not_valid < (even %), (even (s %)).
unfold cond 2 wrt ax set EOB:
`not_valid < (even (s %'), (even %').
= induction hypothesis - proved
A number and its successor cannot both be odd:
oso>nv `not_valid < (odd %), (odd (s %)).
unfold 2 wrt ax set EOB:
`not_valid < (odd (s %'), (odd %').
= induction hypothesis - proved
Nothing can be both even and odd:
eo>nv `not_valid < (even %), (odd %).
unfold cond 1 wrt ax set EOA:
0 `not_valid < (odd 0). - cond invalid - proved
1 `not_valid < (odd %'), (odd (s %')).
= valid clause oso>nv - proved
Proofs of even/odd valid clauses involving addition are collected here:
addition even/odd proofs
Proofs involving multiplication are here:
multiplication even/odd proofs
4. Proof of N^2 Even Theorem
Finally, using the previously-proved valid clauses, we wish to prove
the theorem that for any natural number n, if n^2 is even,
then n is even. This statement is defined by the following
valid clause and its proof is given:
Thm: n^2 even implies n even
en^2>en (even %n)< (sq %n %n^2), (even %n^2).
unfold sq cond:
(even %n)< (times %n %n %n^2), (even %n^2).
= unfold 1vxx>x with te3>1ve1e2 - proved
back to Axiomatic Language Proof Page
back to Axiomatic Language Home Page