Extended Axiomatic Language

**Using the Complement of a Valid Expression Set
for Specification**

back to Axiomatic Language Home Page

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 "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 palindromesExtended 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 atomsThese 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~: everythingSince the symbol P is in the complementary expression set EAL0~, our level 1 valid expressions will include P:

EAL1v: P EAL1~: everything except PNow since P is not in the complementary expression set EAL1~, our level 2 valid expressions will not include P:

EAL2v: empty EAL2~: everythingBut 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 evenThe 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>=1Applying 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>=3Applying 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>=5Each 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 expressionsWe 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 symbolWe 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) exprsApplying 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 predicateCombined 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

**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 varsOur 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~ - there exists an instance that is complementary (E~ %enc)< (enc_inst %enc %inst), %inst ~. ! (b)An example valid expression would be

! 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 "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 validValid 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

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