Extended Axiomatic Language

Using the Complement of a Valid Expression Set for Specification

Axiomatic language is a powerful formalism for defining recursively enumerable sets of hierarchical symbolic expressions. When one specifies a recursively enumerable set, one is simultaneously specifying the complement of that set, which may not be recursively enumerable. This complement set may be useful for specification. This web page defines "extended axiomatic language", which uses this complement set to define new valid expressions and effectively provides a form of negation.

1. Extended Axiomatic Language -- A Preliminary Definition

We will refer to the original language as "basic axiomatic language" and the set of generated expressions as "basic valid expressions". The term "complementary expression" will refer to an expression that has no instance that is a valid expression. Thus if our set of basic axioms consists of just the identical expressions axiom,

```  (== % %).
```
then (== a a) and (== (b %) (b %)) are basic valid expressions, and (== a b) and (== (%1 x) (%2 y)) are complementary expressions, but (== %1 %2) is neither valid nor complementary since some instances are valid and some are not.

A "complementary axiom" is one that has one or more "complementary conditions", denoted by a tilde after the condition expression:

conclu < ..., cond~, ....

A set of "extended axioms" consists of basic and complementary axioms and generates a set of "extended valid expressions". The conclusion of an extended axiom instance is an extended valid expression if all the "positive" conditions are extended valid expressions and all the complementary conditions are complementary expressions. Note that the set of complementary expressions (defined from just the basic axioms) remains fixed as the extended valid expressions are generated. Note also that the set of extended valid expressions includes the basic valid expressions as a subset.

Extended axiomatic language makes it easier to define negative predicates:

```! some basic axioms:

(member % (\$1 % \$2)).            ! member of a sequence

(reverse () ()).                 ! reverse of a sequence
(reverse (% \$seq) (\$rev %))< (reverse (\$seq) (\$rev)).

(sequence (\$)).                  ! set of sequences

! some complementary axioms:

(not_member %x %seq)< (sequence %seq), (member %x %seq)~.
! not a member of a sequence

(not_palindrome %)< (sequence %), (reverse % %)~.
! sequences that are not palindromes
```
Extended axiomatic language also lets us define the set of all atoms and an inequality relation between distinct atoms, which is not built-in:
```  (atom %)< (sequence %)~.        ! set of atoms

(/=atoms %1 %2)< (atom %1), (atom %2), (== %1 %2)~.  ! distinct atoms
```
These relations can be defined in basic axiomatic language, but not as concisely or completely. See the Calculator Program for an example of using extended axiomatic language to define error handling.

2. Extended Axiomatic Language -- Generalized

One observation about the above preliminary definition is that we might want to make use of the complement of the extended valid expressions. A natural generalization of the above definition is to let the "complementation" process that is applied to the basic valid expressions be applied to the extended valid expressions to define a new "level" of extended valid expressions. We refer to the set of basic valid expressions and their complement as "level 0" or EAL0. The EAL0 complementary expressions match the complementary conditions in complementary axioms as described above to generate the "level 1" or EAL1 valid expressions and their complement. This process could be repeated to define levels 2,3,....

The relationships of the different levels of extended axiomatic language can be shown by the following bar graphs that partition the complete set of ground expressions (i.e., expressions without variables) into those that are valid and those that are complementary. Non-ground expressions (those with variables) are valid/complementary if all their instances are valid/complementary, respectively, or they may be neither valid nor complementary if instances are both. For level 0 extended axiomatic language (basic axiomatic language) the partition of ground expressions into valid (EAL0v) and complementary (EAL0~) can be represented as follows:

```   ______________0____________________________________________________
|______EAL0v___|______EAL0~_________________________________________|
```
The complementary expressions EAL0~ applied to the extended axioms yields the level 1 extended valid expressions and their complement:
```   ______________0_____________________1______________________________
|________________________EAL1v_______|____EAL1~_____________________|
```
(The numbers above the bar show the successive partitions.) As stated above, the level 1 extended valid expressions EAL1v include the basic valid expressions EAL0v:
```    EAL1v ⊇ EAL0v  (EAL1~ ⊆ EAL0~)
```
We now apply the complementary expressions EAL1~ to our extended axiom set to yield level 2 extended valid expressions and their complement:
```   ______________0____2________________1______________________________
|__________EAL2v____|______EAL2~____________________________________|
```
Our set of level 2 valid expressions EAL2v is still a superset of the basic valid expressions EAL0v:
```    EAL2v ⊇ EAL0v  (EAL2~ ⊆ EAL0~)
```
Since the complementary expressions EAL1~ that generate EAL2v are a subset of the EAL0~ expressions that generate EAL1v, we have
```    EAL2v ⊆ EAL1v  (EAL2~ ⊇ EAL1~)
```
Now we apply the complementary expressions EAL2~ to our extended axiom set to yield level 3 extended valid expressions and their complement:
```   ______________0____2__________3_____1______________________________
|____________________EAL3v_____|____EAL3~___________________________|
```
Since the EAL2~ expressions that generate EAL3v are a superset of the EAL1~ expressions that make EAL2v, we have
```    EAL3v ⊇ EAL2v  (EAL3~ ⊆ EAL2~)
```
Since the EAL2~ expressions are a subset of the EAL0~ expressions, we have
```    EAL3v ⊆ EAL1v  (EAL3~ ⊇ EAL1~)
```
We continue with the level 4 extended expressions defined from EAL3~:
```   ______________0____2___4______3_____1______________________________
|_______________EAL4v___|____EAL4~__________________________________|
```
Since EAL3~ is a subset of EAL2~, we have
```    EAL4v ⊆ EAL3v  (EAL4~ ⊇ EAL3~)
```
and since EAL3~ is a superset of EAL1~, we have
```    EAL4v ⊇ EAL2v  (EAL4~ ⊆ EAL2~)
```
It appears that the valid expression sets for the even-numbered levels EAL0v, EAL2v, EAL4v, ..., are non-decreasing and bounded from above by the odd-numbered levels EAL1v, EAL3v, ..., which are non-increasing. We now give a proof of this property.

Let i0 be some even level number and let i1,i2,... represent level numbers i0+1,i0+2,.... Our inductive hypothesis is that the following relations hold:

```  ________________0____2_________1___________________________
EALi2v ⊆ EALi1v    (EALi2~ ⊇ EALi1~)
EALi2v ⊇ EALi0v    (EALi2~ ⊆ EALi0~)
```
As shown above, these relations are true when i0 = 0, so the base case is satisfied. Letting level i3 = i2+1 be defined from complementary expressions EALi2~, we get:
```  ________________0____2______3__1___________________________
EALi3v ⊇ EALi2v    (EALi3~ ⊆ EALi2~)
-- since EALi2~ ⊇ EALi1~
EALi3v ⊆ EALi1v    (EALi3~ ⊇ EALi1~)
-- since EALi2~ ⊆ EALi0~
```
Now we define level i4 = i2+2 expressions from the complementary expressions EALi3~:
```  ________________0____2__4___3__1___________________________
EALi4v ⊆ EALi3v    (EALi4~ ⊇ EALi3~)
-- since EALi3~ ⊆ EALi2~
EALi4v ⊇ EALi2v    (EALi4~ ⊆ EALi2~)
-- since EALi3~ ⊇ EALi1~
```
But these are the same relations as our induction hypothesis when we let i0 = i0+2, so the relations are true for all even i0.

We formally define extended axiomatic language as the limit of the even-numbered levels as i0 goes to infinity. This would be a fixed point in the sense that if EALv is this limit, then applying the EAL complementation step twice will produce the same set of (even level) valid expressions. We can illustrate the levels of extended axiomatic language with some examples.

[Example 1]  Suppose our set of extended axioms consists of just this single complementary axiom:

```  P < P ~.
```
Since there are no basic axioms, the set of basic valid expressions EAL0v is empty:
```  EAL0v:  empty               EAL0~:  everything
```
Since the symbol P is in the complementary expression set EAL0~, our level 1 valid expressions will include P:
```  EAL1v:  P                   EAL1~:  everything except P
```
Now since P is not in the complementary expression set EAL1~, our level 2 valid expressions will not include P:
```  EAL2v:  empty               EAL2~:  everything
```
But this is the same as level 0. Thus the even levels will not contain P but the odd levels will. And according to our formal definition, the extended valid expressions will not contain P. This is the extended axiomatic language solution to the above apparently contradictory axiom.

[Example 2]  For our next example of extended axiomatic language levels, consider the following set of axioms:

```  (num 0).                    ! basic axioms for set of natural numbers
(num (s %))< (num %).

(even 0).                          ! 0 is even
(even (s %))< (num %), (even %)~.  ! if k not even, k+1 is even
```
The basic valid expressions include the natural numbers in successor notation, so these expressions are in all extended valid expression levels below. We thus limit our analysis to the 'even' predicate with natural number arguments:
```  EAL0v:  (even 0)
EAL0~:  (even k), k>=1
```
Applying our complementary expressions EAL0~ we get:
```  EAL1v:  (even 0), (even k), k>=2
EAL1~:  (even (s 0))
```
Applying EAL1~ we get:
```  EAL2v:  (even 0), (even (s (s 0)))
EAL2~:  (even (s 0)), (even k), k>=3
```
Applying EAL2~:
```  EAL3v:  (even 0), (even (s (s 0))), (even k), k>=4
EAL3~:  (even (s 0)), (even (s (s (s 0)))
```
Applying EAL3~:
```  EAL4v:  (even 0), (even (s (s 0))), (even (s (s (s (s 0)))))
EAL4~:  (even (s 0)), (even (s (s (s 0))), (even k),k>=5
```
Each successive even-numbered level adds an 'even' expression with another even number. The limit defines the even predicate for all even numbers, so this, along with the 'num' predicate, is the set of extended valid expressions.

[Example 3]  For our last example of extended axiomatic language levels, we will combine an arbitrary set of basic axioms with a single complementary axiom that defines a predicate for complementary expressions:

```  <some basic axioms>
(~ %)< % ~.       ! ~ is predicate for complementary expressions
```
We use the symbol consisting of just the tilde character ~ as the name of the predicate for complementary expressions. (This predicate name is just an arbitrary symbol and is distinct from the use of tilde after a complementary condition.) We let 'b' represent the set of basic valid expressions generated by the basic axioms. For this example, none of the basic valid expressions will include the predicate ~. Our level-0 extended axiomatic language valid expressions are just the b expressions:
```  EAL0v:  b          -- the set of basic valid expressions
(none of which are of the form (~ expr))
```
To help define expression sets, we will use the symbol % to denote the set of all expressions and the symbol * to represent all expressions except those involving the complementary predicate (~ expr). We will also use + and - to denote set union and difference. Thus the set of all expressions % can be partitioned into those those not including and those including the complementary predicate:
```  % = * + (~ %)      -- partition of set of all expressions
* = atoms + () + (%) + (not~ %) + (% % % \$)
-- all expressions except those of form (~ %)
-- \$ represents set of all strings, so
(% % % \$) is set of all sequences of length >=3
atoms = % - (\$)  -- set of all atoms
not~ = % - ~     -- set of all expressions other than the tilde symbol
```
We can now express the level-0 complement expressions as follows:
```
EAL0~:  everything but b
:  % - b              -- all expressions except b valid exprs
:  {* + (~ %)} - b    -- partitioning the set of expressions
:  *-b + (~ %)        -- (b has no expressions of form (~ expr))
-- *-b is complement of b except for the (~ expr) exprs
```
Applying our complementary expressions EAL0~, we get level 1:
```  EAL1v:  b + (~ {*-b + (~ %)})
b + (~ *-b) + (~ (~ %))

EAL1~:  % - {b + (~ *-b) + (~ (~ %))}
{* + (~ %)} - b - (~ *-b) - (~ (~ %)))
* - b + (~ %) - (~ *-b) - (~ (~ %))
*-b + (~ {% - *-b - (~ %)})
*-b + (~ {* + (~ %)} - *-b - (~ %))
*-b + (~ {* - *-b} + (~ {% - %}))
*-b + (~ b)
```
Applying EAL1~ we get:
```  EAL2v:  b + (~ {*-b + (~ b)})
b + (~ *-b) + (~ (~ b))

EAL2~:  % - {b + (~ *-b) + (~ (~ b))}
{* + (~ %)} - b - (~ {*-b - (~ b)})
*-b + (~ {% - *-b - (~ b)})
*-b + (~ {* + (~ %)} - *-b - (~ b))
*-b + (~ {* - *-b} + (~ % - b))
*-b + (~ b) + (~ (~ {* + (~ %)} - b))
*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ %)))
```
Applying EAL2~:
```  EAL3v:  b + (~ {*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ %)))})
b + (~ *-b) + (~ (~ b)) + (~ (~ (~ *-b))) + (~ (~ (~ (~ %))))

EAL3~:  % - {b + (~ *-b) + (~ (~ b)) + (~ (~ (~ *-b))) + (~ (~ (~ (~ %))))}
{* + (~ %)} - b - (~ *-b - (~ b - (~ *-b - (~ %))))
*-b + (~ % - *-b - (~ b - (~ *-b - (~ %))))
*-b + (~ b + (~ % - b - (~ *-b - (~ %))))
*-b + (~ b + (~ *-b + (~ % - *-b - (~ %))))
*-b + (~ b + (~ *-b + (~ b - (~ % - %))))
*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ b)))
```
Applying EAL3~:
```  EAL4v:  b + (~ {*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ b)))})
b + (~ *-b) + (~ (~ b)) + (~ (~ (~ *-b))) + (~ (~ (~ (~ b))))

EAL4~:  % - {b + (~ *-b) + (~ (~ b)) + (~ (~ (~ *-b))) + (~ (~ (~ (~ b))))}
*-b + (~ % - *-b - (~ b - (~ *-b - (~ b))))
*-b + (~ b + (~ % - b - (~ *-b - (~ b))))
*-b + (~ b + (~ *-b + (~ % - *-b - (~ b))))
*-b + (~ b + (~ *-b + (~ b + (~ % - b))))
*-b + (~ b + (~ *-b + (~ b + (~ *-b + (~ %)))))
*-b + (~ b) + (~ (~ *-b)) + (~ (~ (~ b))) + (~ (~ (~ (~ *-b))))
+ (~ (~ (~ (~ (~ %)))))
```
Based on the pattern of EALv0,2,4, we conjecture that the complete set of extended valid expressions will be:
```  b +             (~ *-b)       +             (~ (~ b))
+       (~ (~ (~ *-b)))     +       (~ (~ (~ (~ b))))
+ (~ (~ (~ (~ (~ *-b)))))   + (~ (~ (~ (~ (~ (~ b))))))
...                         ...
```
This needs an induction proof, of course.

3. Examples

This section gives examples showing the usefulness of extended axiomatic language for specification. Section A uses the predicate for the set of complementary expressions to define the "plain vanilla meta-interpreter" for extended axiomatic language. Section B defines universal and existential quantification for valid expressions and uses it to define the set of "valid clauses".

3.A. Complementary Expression Predicate

Example 3 of Section 2 above introduced the complementary expression predicate ~ that states that its argument is a complementary expression:

```  (~ %comp)< %comp ~.     ! complementary expression predicate
```
Combined with the axioms of Section 1 above, we get the following extended valid expressions:
```  (~ (== a b))
(~ (== (a %a) (b %b)))       -- all instances are valid
(~ (atom (\$)))               -- all instances are valid
(~ (~ (== x x)))
(~ (~ (~ (== a b))))
(~ (~ (~ (~ (== x x)))))
```
You will note that these satisfy the pattern of the set of extended valid expressions for Example 3, above. Using the ~ predicate for complementary conditions we can represent a set of extended axioms as data in a single expression, i.e., the "plain vanilla meta-interpreter":
```  (axiom_set
((== % %))
((sequence (\$)))
((atom %) (~ (sequence %)))
((/=atoms %1 %2) (atom %1) (atom %2) (~ (== %1 %2)))
).

(axiom \$axiom)< (axiom_set \$axioms1 (\$axiom) \$axioms2).

(all_valid).                ! all expressions in list are valid
(all_valid %expr \$exprs)< %expr , (all_valid \$exprs).

%conclu < (axiom %conclu \$conds), (all_valid \$conds).
```
Some other higher-order forms involving complementary expressions that may be useful are as follows:
```! all~ - all expression in list are complementary

(all~).
(all~ %~expr \$~exprs)< %~expr ~, (all~ \$~exprs)).

! one~ - (at least) one expression in list is complementary

(one~ \$1 %~expr \$2)< %~expr ~.

! exactly_one~ - exactly one expression is complementary (the rest are valid)

(exactly_one~ \$v1 %~expr \$v2)< %~expr ~, (all_valid \$v1 \$v2).

! exactly_one_valid - exactly one expression is valid (the rest complementary)

(exactly_one_valid \$~1 %valid \$~2)< %valid , (all~ \$~1 \$~2).
```
Note that we could have written (~ %~expr) instead of the complementary condition %~expr ~ in these axioms.

3.B. Quantification on Encoded Expressions

Extended axiomatic language allows us to define a form of quantification on valid expressions. We can assert, for example, that all instances of an expression are valid. To do this we will use (non-variable) ground symbols to represent real variables. Symbols beginning with # and & will represent expression and string variables, respectively. To represent actual symbols beginning with # and &, we will prepend an underscore _. To represent symbols _#.. and _&.., we prepend another _, etc. The utility file enc_inst.eax uses extended axiomatic language to define the following predicate that maps an encoded expression (with {_}#.. and {_}&.. symbols) to a real expression instance:

```  (enc_inst <enc_expr> <real_inst>)
<enc_expr>  -- an expression with encoded variables
<real_inst>  -- corresponding expression with real variables
(possibly instantiated)

#...     -- symbol representing an expression variable
_#...  ->  #...    -- symbols representing symbols
__#...  ->  _#...       ... with leading _ removed
...

&...     -- symbol representing a string variable
_&...  ->  &...
__&...  ->  _&...
...

some example valid expressions:
(enc_inst (== # #) (== (a \$) (a \$)))
(enc_inst (append1 (&) # (& #)) (append1 (\$) % (\$ %)))
(enc_inst (symbols: _#a _&b ___#c) (symbols: #a &b __#c))  -- no vars
```
Our quantification definitions involve quantification over all the variables in an encoded expression. We first define the predicate 'E' which asserts that its encoded expression argument has a real instance that is a valid expression:
```! E - there exists an instance that is valid

(E %enc)< (enc_inst %enc %inst), %inst .       ! (a)
```
An example valid expression would be (E (== #a #b)) since the instance (== c c) is valid. Similarly, we can define predicate 'E~' which asserts that an instance is complementary:
```! E~ - there exists an instance that is complementary

(E~ %enc)< (enc_inst %enc %inst), %inst ~.      ! (b)
```
An example valid expression would be (E~ (== #a #b)) since the instance (== c d) is complementary. Using the complement of the 'E' and 'E~' predicates, we can define universal quantification:
```! A - all instances are valid
! (no instance is complementary)

(A %enc)< (E~ %enc)~.                          ! (c)

! A~ - all instances are complementary
! (no instance is valid)

(A~ %enc)< (E %enc)~.                          ! (d)
```
Some example valid expressions are (A (== (&) (&))) and (A~ (== (a #) (b #))).

A "valid clause" is a conclusion and zero or more conditions, just like an axiom, that has the property that if we add it to the set of axioms, no new valid expressions are generated. The valid clause is thus "implied" by the set of axioms. Some example valid clauses given the above axioms are as follows:

```  (== (a %) (a %)).
(num (s (s %))< (num %).
```
Using these quantification predicates along with some higher-order forms we can define a predicate for the set of valid clauses:
```! enc_valid_clause - encoded expression represents a valid clause

(enc_valid_clause %enc_conclu \$enc_conds)<           ! (e)
(A (one_valid %enc_conclu (~ (all_valid \$enc_conds)))).
! -- An "encoded" clause is valid if
!    for all instances of the encoded variables,
!    either the conclusion is valid or the conjunction of
!    the conditions is complementary.

! example encoded valid expressions generated:
!   (enc_valid_clause (num (s (s #))) (num #))
!   (enc_valid_clause (== (a &1) (a &2)) (== (&1) (&2)))

! valid_clause - set of valid clauses (with real variables)

(valid_clause \$clause)< (enc_valid_clause \$enc_clause),      ! (f)
(enc_inst (\$enc_clause) (\$clause)).

! example valid expressions:
!   (valid_clause (num (s (s 0))) (num 0))   -- valid because conclu valid
!   (valid_clause (num (s (s a))) (num a))   -- valid because cond not valid
!   (valid_clause (num (s (s %))) (num %))   -- valid because all insts valid
```
Valid clauses can be used to state assertions about a set of axioms as a way to check a specification. For example, an addition predicate should be commutative, else we have an error:
```  Error! < (valid_clause (== %3a %3b) (plus %1 %2 %3a)
(plus %2 %1 %3b))~.
```
If any instance of the valid clause condition is not valid, then the 'Error!' symbol is generated as a valid expression and that indicates the addition predicate has an error.

The above quantification axioms also generate valid expressions that represent nested quantification. For example, the statement that "for all X, there exists a Y equal to X" is represented by the valid expression:

```  (A (E (== #x _#y)))                     (g)
```
Axiom (a) above first generates valid expressions such as (E (== a #y)) and (E (== (b c) #y)). In fact, all instances of (E (== % #y)) are generated as valid expressions. Thus, using axiom (c) we get the valid expression (g). Note that the existential variable #y must be encoded with a leading underscore _.

Another example of nested quantification uses the following basic axiomatic language predicate '<=len' which says that the first argument sequence has length less than or equal to that of the second argument sequence:

```! <=len - first argument sequence length <= second argument length

(<=len () (\$)).
(<=len (%1 \$1) (%2 \$2))< (<=len (\$1) (\$2)).
```
The statement "there exists an expression (namely the empty sequence) that has length <= that of all other sequences" is represented by the following valid expression:
```  (E (A (<=len #x (_&y))))                (h)
```
Axiom (c) above generates the valid expression (A (<=len () (&y))). Combining this with axiom (a) gives the valid expression (h).