back to Axiomatic Language Home Page

Proof in Axiomatic Language


1. Axiom Sets and Valid Expressions

In axiomatic language a finite set of axioms generates a (usually) infinite set of valid expressions. (Review language definition here). For example, the following axioms define the set of natural numbers in successor notation: 
  (num 0).                 ! n0: zero is a number
  (num (s %n))< (num %n).  ! n1: successor of n is number if n is number
We refer to these axioms as n0,n1. This set of two axioms generates the following infinite set of valid expressions representing the set of natural numbers: 
  (num 0)
  (num (s 0))
  (num (s (s 0)))
  (num (s (s (s 0))))
     ...
Suppose we were to add the following axiom n2 to the above set of natural number axioms: 
  (num (s (s %n)))< (num %n).   ! n2: 2+n is number if n is number
Note that adding this axiom does not add any new natural number valid expressions. On the other hand, if in place of n2 we add axiom q, 
  (qnum %)< (num %).    ! q
then the following additional valid expressions are created: 
  (qnum 0)
  (qnum (s 0))
  (qnum (s (s 0)))
      ...
So adding an axiom to a set of axioms may generate additional valid expressions or it may not, but it will never remove them.


2. Valid Clauses

Let us define a "clause" the same as an axiom:

   clause – a conclusion expression and zero or more condition expressions

A clause has a clause instance by an assignment of values to the expression and string variables. For a set of axioms, if all the conditions of a clause instance are valid expressions then the conclusion is a generated expression. A clause is a valid clause with respect to a set of axioms if all its generated expressions are valid expressions. For clause n2 above, all its generated expressions with respect to axiom set n0,n1 are valid expressions (natural numbers), so it is a valid clause with respect to n0,n1. But clause q is not.

One can say that a valid clause is "implied" by the set of axioms. It can be considered a "true statement" about the axioms. For example, our definition of natural numbers given by axioms n0,n1 implies the statement "if n is a number, then succ(succ(n)), or 2+n, is a number", which is what clause n2 says.

Note that if a clause conclusion is already a valid expression, the clause is valid:

   valid_expr < ..conds...

Similarly, if a clause condition has no instance that is a valid expression, the clause is valid:

   conclu < ..., no_valid_inst, ....


3. Equivalent Axiom Sets

Let us add to axioms n0,n1 the following axioms to define addition of natural numbers: 
  (plus % 0 %)< (num %).                     ! p0
  (plus %1 (s %2) (s %3))< (plus %1 %2 %3).   ! p1
The combined axiom set n0,n1,p0,p1 generates the same set of natural number valid expressions given above, but it also generates valid expressions that give the addition of all pairs of natural numbers: 
  (plus 0 0 0)
  (plus (s 0) 0 (s 0))
  (plus 0 (s 0) (s 0))
  (plus (s (s 0)) 0 (s (s 0)))
  (plus (s 0) (s 0) (s (s 0)))
      ...
There are alternative ways of defining natural number addition. For example the following two axioms do the induction on the first argument instead of the second: 
  (plus 0 % %)< (num %).                     ! pa0
  (plus (s %1) %2 (s %3))< (plus %1 %2 %3).   ! pa1
Axiom set n0,n1,pa0,pa1 generates the same set of valid expressions as set n0,n1,p0,p1. Adding clauses pa0 or pa1 to axiom set n0,n1,p0,p1 produces no new valid expressions so pa0 and pa1 are valid clauses with respect to set n0,n1,p0,p1. Similarly, p0,p1 are valid clauses with respect to axiom set n0,n1,pa0,pa1.

Given two axiom sets A and B, if all the axioms of set A are valid clauses with respect to set B and all the axioms of set B are valid clauses with respect to set A, then we say that A and B are equivalent axiom sets – they generate the same set of valid expressions. This concept would be used to assert the equivalence between specification axioms and axioms that define an efficient implementation.


4. Proving Valid Clauses

How can we prove that clause n2 above is a valid clause with respect to axiom set n0,n1? This section gives some simple rules that follow from the definitions and rules of axiomatic language:

r1. An axiom is a valid clause.

r2. An instance of a valid clause is a valid clause.

r3. Adding a condition to a valid clause gives a valid clause.

r4. For every expression e we have a valid clause 
  e < e .
These rule r4 valid clauses are instances of this single valid clause: 
  % < % .
r5. Given clauses A and B, 
  A:  cA0 < cA1,...,cAna.
  B:  cB0 < CB1,...,CBnb.
where cA0,cB0 are conclusions and cA1..cAna,cB1..cBnb are conditions, if some condition cAk is identical to conclusion cB0, then we can construct valid clause C from clause A where condition cAk is replaced by conditions cB1,..,cBnb: 
  C:  cA0 < cA1,..,cAk-1,cB1,..,cBnb,cAk+1,..,cAna.
We refer to this as an unfold of valid clause A with respect to valid clause B.

A proof that n2 is a valid clause for axiom set n0,n1 is shown by the following valid clauses and their justifications: 

  a:  (num (s %n))< (num %n).          r1 - axiom n0
  b:  (num (s (s %n)))< (num (s %n)).  r2 - instance of a
  n2: (num (s (s %n)))< (num %n).      r4 - unfold of b wrt a
We can also rename valid clause variables.


5. Induction Rule for Valid Clauses

We need to be able to prove that pa0 and pa1 are valid clauses with respect to axiom set n0,n1,p0,p1, and conversely prove that p0,p1 are valid with respect to axioms n0,n1,pa0,pa1. For this we need an induction rule.

Consider clause C with condition ci, 
  C:  c0 < c1,..,ci-1, ci, ci+1,..,cn;
and let A be an axiom: 
  A:  a0 < a1,..,ak;
A "most-general unifier" is a "most-general" assignment of expression and string values to the variables of C and A that makes C's condition ci and A's conclusion a0 identical. After this assignment an unfold (rule 4 above) can be done to produce a new clause C': 
  C':  c0' < c1',..,ci-1', a1',..,ak', ci+1',..,cn';
Typically a unifier for condition ci will exist for only a subset of axioms in an axiom set, so only those will produce C' clauses, which we will denote C'1..C'm. We call this operation a "complete unfold" of clause C's condition ci with respect to the axiom set.

We claim that the set of generated expressions for clause C exactly equals the union of the generated expressions for clauses C'1..C'm. Therefore, if we prove that C'1..C'm are all valid, then we have proved C valid. We also claim that we can use C as an "induction hypothesis" in the proof of clauses C'1..C'm. We can unfold valid clauses against induction hypothesis C according to rule 4 above to prove C'1..C'm. These statements need justification but the principles seem to work in the example proofs below.

Example – prove clauses pa0 and pa1 valid wrt axiom set n0,n1,p0,p1 
axiom set (repeated from above):
  n0:  (num 0).
  n1:  (num (s %))< (num %).
  p0:  (plus % 0 %)< (num %).
  p1:  (plus %1 (s %2) (s %3))< (plus %1 %2 %3).

by rules 1-5 we have these valid clauses:
  p0x:  (plus 0 0 0)< (num 0).      - instance of p0
  p00:  (plus 0 0 0).               - unfold p0x with n0
  p0y:  (plus (s %) 0 (s %))< (num (s %)).  - another instance of p0 
  p01:  (plus (s %) 0 (s %))< (num %).      - unfold p0y with n1
  p1x:  (plus 0 (s %) (s %))< (0 % %).      - instance of p1
  p1y:  (plus (s %1) (s %2) (s (s %3)))< (plus (s %1) %2 (s %3)).  - inst of p1

prove pa0: (plus 0 % %)< (n %).
complete unfold of pa0 condition 1 wrt ax set:
  pa0'0  (plus 0 0 0).
    = valid clause p00 -- proved
  pa0'1  (plus 0 (s %) (s %))< (n %).
    = unfold of p1x with induction hypothesis pa0 -- proved
  -- all pa0' clauses proved, so pa0 is proved!

prove pa1: (plus (s %1) %2 (s %3))< (plus %1 %2 %3).
unfold pa1 cond 1 wrt ax set:
  pa1'0:  (plus (s %) 0 (s %))< (num %).
    = valid clause p01 -- proved
  pa1'1:  (plus (s %1) (s %2) (s (s %3)))< (plus %1 %2 %3).
    = unfold of p1y with induction hypothesis pa1 -- proved
  -- all pa1' clauses proved, so pa1 is proved!
Analogously, we can show that p0,p1 are both valid clauses with respect to axiom set n0,n1,pa0,pa1. Thus, we have that axiom sets n0,n1,p0,p1 and n0,n1,pa0,pa1 are equivalent.

A final observation for the induction rule is that a complete unfold of a clause condition with respect to an axiom set can be done instead with respect to any equivalent axiom set, as will be done for the commutativity proof below.


6. Example – Proving Commutativity of Addition

For our commutativity proof we re-state the above axioms n0,n1,p0,p1 with abbreviated symbols for conciseness: 
  n0:  (n 0).
  n1:  (n (s %))< (n %).
  p0:  (p % 0 %)< (n %).
  p1:  (p %1 (s %2) (s %3))< (p %1 %2 %3).
We will also be using the equivalent addition axioms pa0,pa1: 
  pa0:  (p 0 % %)< (n %).
  pa1:  (p (s %1) %2 (s %3))< (p %1 %2 %3).
We add to our axiom set the following axiom that defines identical expressions: 
  ==:  (== % %).
We will also need the following valid clause, 
  ==s:  (== (s %a) (s %b))< (== %a %b).
which is proved as follows: 
unfold ==s cond 1 wrt ax set n0,n1,p0,p1,==:
  ==s':  (== (s %) (s %)).
    = instance of axiom == -- proved
  -- so ==s proved
The commutativity of addition can be expressed as the following valid clause: 
  C:  (== %3a %3b)< (p %1 %2 %3a), (p %2 %1 %3b).
This clause asserts that swapping the addition arguments produces an identical result. If addition were not commutative, then (== ...) expressions with non-identical arguments would be generated and thus C would not be a valid clause. The proof that C is a valid clause with respect to axiom set n0,n1,p0,p1,== (and equivalent axiom set n0,n1,pa0,pa1,==) is as follows: 
unfold clause C cond 1 wrt ax set n0,n1,p0,p1,==:
  C'0:  (== % %3b)< (n %), (p 0 % %3b).
  unfold C'0 cond 2 wrt equiv ax set n0,n1,pa0,pa1,==:
    C'0'0:  (== % %)< (n %), (n %).
      = axiom == with added conditions (rule r3) -- proved
    -- so C'0 proved
  C'1:  (== (s %3a') %3b)< (p %1 %2' %3a'), (p (s %2') %1 %3b).
  unfold C'1 cond 2 wrt equiv ax set n0,n1,pa0,pa1,==:
    C'1'0  (== (s %3a') (s %3b'))< (p %1 %2' %3a'), (p %2' %1 %3b').
      = unfold of ==s with induction hypothesis C -- proved
    -- so C'1 proved
  -- so C proved!

7. Example – Proof of Functionality of Addition

For future proofs we need to prove the functionality of addition. That is, we want to show that plus yields just one result. This is expressed by the following clause: 
  pf:  (== %3a %3b)< (p %1 %2 %3a), (p %1 %2 %3b).  - plus is function
We prove this clause valid with respect to the axiom set n0,n1,p0,p1,== as follows: 
unfold clause pf cond 1 wrt ax set:
  pf'0:  (= % %3b)< (n %), (p % 0 %3b).
  unfold pf'0 cond 2 wrt ax set:
    pf'0': (== % %)< (n %), (n %).
      = ax == with added conditions -- proved
  pf'1:  (== (s %3a') %3b)< (p %1 %2' %3a'), (p %1 (s %2') %3b).
  unfold pf'1 cond 2 wrt ax set:
    pf'1':  (== (s %3a') (s %3b'))< (p %1 %2' %3a'), (p %1 %2' %3b').
      = unfold of ==s wrt induction hypothesis pf -- proved
    -- so pf'1 proved
  -- and pf proved!

8. Example – Proof of Associativity of Addition

This section proves the associativity of addition: 
  (x1 + x2) + x3 = x1 + (x2 + x3)       (A)
Our induction proof follows this pattern: 
  Show A true for x2 = 0.
  Assume A true for x2 = n,
    Show A true for x2 = (s n).
The associativity of addition is expressed by the following clause: 
  A:  (== %4a %4b)< (p %1 %2 %12), (p %12 %3 %4a),
                    (p %2 %3 %23), (p %1 %23 %4b).
We prove this clause valid with respect to axiom set n0,n1,p0,p1,== (and equivalent axiom set n0,n1,pa0,pa1,==) as follows: 
unfold clause A cond 1 wrt ax set n0,n1,p0,p1,==:
  A'0:  (== %4a %4b)< (n %1), (p %1 %3 %4a),
                      (p 0 %3 %23), (p %1 %23 %4b).
  unfold A'0 cond 3 wrt ax set n0,n1,pa0,pa1,==:
    A'0': (== %4a %4b)< (n %1), (p %1 %3 %4a),
                        (n %3), (p %1 %3 %4b).
      = pf with added conditions -- proved
  A'1:  (== %4a %4b)< (p %1 %2' %12'), (p (s %12') %3 %4a),
                      (p (s %2') %3 %23), (p %1 %23 %4b).
  unfold A'1 cond 2 wrt ..,pa0,pa1,..:
    A'1':  (== (s %4a') %4b)< (p %1 %2' %12'), (p %12' %3 %4a'),
                              (p (s %2') %3 %23), (p %1 %23 %4b).
    unfold A'1' cond 3 wrt ..,pa0,pa1,..:
      A'1'':  (== (s %4a') %4b)< (p %1 %2' %12'), (p %12' %3 %4a'),
                                 (p %2' %3 %23'), (p %1 (s %23') %4b).
      unfold A'1'' cond 4 wrt ..,p0,p1,..:
        A'1''':  (== (s %4a') (s %4ab'))< (p %1 %2' %12'), (p %12' %3 %4a'),
                                          (p %2' %3 %23'), (p %1 %23' %4b').
          = unfold of ==s wrt induction hypothesis A -- proved
    -- so A'1'', A'1', A'1 proved
  -- and A proved!

9. Proof of Reverse Specification/Implementation Equivalence

As stated earlier, proving that axiom sets are equivalent can be used to guarantee equivalence between specification axioms and axioms that define an efficient implementation. This webpage proves equivalence between a specification and an implementation for the reverse function: Reverse Equivalence Proof


10. Proofs of Even/Odd Properties for Natural Numbers

Valid clauses and proofs of even/odd properties for natural number addition and multiplication can be found here: Even/Odd Proof  In particular, we prove the theorem that for all natural numbers n, if n^2 is even then n is even.


11. Future Tasks

Some proof tasks on my list of things to do are as follows:

t1. Do more proof examples. (See Coq examples.)

t2. Justify the correctness of the induction rule. Formally derive all proof rules from the rules of axiomatic language.

t3. Define a formal languge for representing axiomatic language proofs.

t4. Define in axiomatic language a "checker" program for checking axiomatic language proofs.

t5. (long term) Add proof to the axiomatic language transformation system to provide a guarantee of equivalence between a user's specification and the generated efficient program.

t6. (long term) Define a knowledge-based system for proving valid clauses. (This is similar to the problem of knowledge-based transformation.)

back to Axiomatic Language Home Page