back to Axiomatic Language Proof Page

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 numberNote 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 .

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 -- provedNow 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 -- provedSince each axiom of one set is a valid clause with respect to the other set, the two axiom sets EOA and EOB are equivalent.

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 - provedThe 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 - provedProofs of even/odd valid clauses involving addition are collected here: addition even/odd proofs Proofs involving multiplication are here: multiplication even/odd proofs

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