CLS-expressions are similar to CL-expressions (Circle and Letter expressions), except that the letters become upper-case and acquire subscripted 'indices'. So instead of simple lower-case letters such as a, b, c we have symbols such as the following:

A_{pq}, B_{v}, C_{xyz}.

Forms such as these we call 'atoms'. Each atom consists of an upper-case letter together with a 'subscriptum'.
The subscriptum is an ordered set of indices, which are lower-case letters.('Ordered' just means
that the order of the indices, if there are several of them *matters*.) Each index belongs to one of two
types: i) mutable, printed in light type ii) immutable, printed in bold type. To make the distinction even
clearer, on this page mutables are also printed in blue; but this is optional. When writing CLS-expressions
by hand one may distinguish immutable indices by underlining them. A subscriptum may contain no
indices, in which case nothing is written.

Now for a major complicating factor: any immutable may itself have a subscriptum - i.e. an ordered set
(possibly empty) of indices. And if any of *those* indices happen to be immutable, they too may have subscripta -
and so on *ad infinitum*.

If the same upper-case letter appears several times in an expression, it is expected that it will have a subscriptum of the same cardinality (i.e. containing the same number of indices) each time it appears. (If not, we must assume that the same letter is being used to denote an essentially different entity - which is confusing and best avoided.) The number of indices in the subscriptum is sometimes called the 'arity' of the upper-case letter.

Each immutable also has an arity, which is the same for each occurrence of the immutable. If the arity is zero, nothing is written.

In the example-atoms given above, the immutables all had arity zero, while the upper-case letters all had arity greater than zero. But forms such as the following are also permissible:

D, E_{abcdefgghi}.

It is not always convenient, typographically, to use nested subscripts. In such a case one may use curly brackets to indicate the level of subscripting. Thus the forms just given could be written

D, E{**a**{`bc`**d**{`e`**f**{`g`}}}`gh`**i**}.

Indeed, the top level of curly brackets may often be omitted without causing ambiguity, giving us forms such as

D, E**a**{`bc`**d**{`e`**f**{`g`}}}`gh`**i**, F`xyz`.

By a 'term' we mean any form that is suitable to be used as an index, that is, a mutable, or an immutable together with its subscriptum (if any).

A CLS expression consists, then, of a set of possibly nested circles, with a set of atoms, each one placed in one of the spaces within or without the circles. (One or other or both of the sets may be empty.)

Our concern will be with the transformation of CLS expressions into *equivalent*
expressions. To this end, we need to delineate the allowed, equivalence-preserving
transformations. But first we need to familiarize ourselves with a type of transformation (not
in itself necessarily equivalence-preserving) called a 'substitution'.

Let a, b, c, .. g be a set of mutables, and let s, t, u, ..z be an equinumerous collection of terms, mutable or immutable, and not necessarily distinct (thus repeats are allowed). Suppose E is a CLS-expression; then let

E[s/a,t/b,u/c, ... z/g]

denote the expression
that results from replacing every occurrence of a in E by s, every occurrence of b by t, and so on.
In case any of s, t, u... is an immutable with a subscriptum, its indices may be mutables, or unsubscripted immutables,
or subscripted immutables. There is indeed a vast range of possibilities -
this is Liberty Hall! There is just one restriction: *none of the mutables (a, b, c, ...) may appear
anywhere in the terms s, t, u, ... (including their subscripta, if any)*. Thus the substitution has
the effect of removing
all trace of the mutables a, b, c, ... from the expression on which it acts.
It is often convenient to let a letter,
typically θ (or φ, ψ, etc.)
stand for the operation of substitution, and to let Eθ stand for the result of operating
upon E with that substitution:

Eθ = E[s/a,t/b,u/c, ... z/g].

Clearly substitutions may be compounded and we write

θ = φ•ψ

to signify that θ is the substitution that is the result of performing first φ and then ψ.

We are now in a position to define the equivalence-preserving transformations of CLS-expressions.

1. Expressions, or sub-expressions may be subjected to the transformations permitted in the CL-calculus. These are the transformations generated by combining the (bi-directional) 'Bricken initials':

wrap, unwrap e ↔ ((e))

delete, undelete e( ) ↔ ( )

copy, uncopy e(f) ↔ e(ef) ,

where e, f stand for any sub-expressions of an expression E. We will refer to any such combination of steps as a CL-operation. Note that in 'copy' or 'uncopy', the copy of e must be identical in all respects (including subscripta, to all depths) to the original. (If any of this is unfamiliar to the reader, he or she should return to the page Clara's World: the Calculus of Circles and Letters.)

2. Expressions, or top-level factors of expressions, (but *not* sub-expressions in general) may be transformed as follows:

E → E Eθ.

That is to say, E (which is either a whole expression or a factor of an expression) may
be replaced by E *together with* a substituted version of E. As θ is our symbol
for a generic substitution, as described above (where a set of mutables is taken out of an expression
and replaced by a set of terms) we
will call the new kind of allowed transformation 'theta-copy'. First E is copied (a valid CL step),
then the copy is transformed by substitution.

We emphasize that theta-copy may not be applied to a sub-expression of an expression, other than to a top-level factor.

To define what is allowed in another way, we may say that an expression of the form FG may be transformed as follows:

F G → F G Gθ .

Note that any expression whatsoever may be put in the form FG by taking F to be the void expression.

3. Reverse theta-copy, or theta-absorption, is another allowed transformation. If one factor of an expression can be construed as a substituted version of another factor, then the substituted version may be removed:

F G Gθ → F G .

4. We will find it convenient not to use the usual equals sign = between expressions that have been transformed by theta-copy or reverse theta-copy, but the modified sign ≅. (We will keep the usual equals sign for CL-equivalence.) Any expression H that is the result of acting on an expression E by a combination of theta-copies, theta-absorptions and CL-operations is said to be CLS-equivalent to E; and we indicate this by writing

E ≅ H.

The relation symbolized by ≅ is easily shown to be an equivalence relation (exercise for the reader: it is required to show A≅A; A≅B implies B≅A; if A≅B and B≅C then A≅C).

If A, B, C are expressions such that B ≅ C then

A B ≅ A C .

The equivalence of B and C says that there is a sequence of CL-operations and theta-copies and reverse theta-copies which transforms B into C. The same operations will transform AB into AC, because the additional presence of A makes no difference to the operations ◊

Pa(Pb)

≅ Pa (Pb) (Pb)[a/b] [instance of theta-copy]

= Pa (Pb) (Pa) [by definition of [a/b]]

= Pa (Pb) O [by uncopy]

= O [by delete].

Thus

Pa(Pb) ≅ O .

But *nota bene*: this must not be taken to imply that

(Pa(Pb)) ≅ _ ,

which is what one would get if one *were* allowed to apply theta-copy to a
sub-expression (that is, to 'Pa(Pb)', in this particular example). What we are
allowed to do is to apply theta-copy to the whole, circled expression, giving us

(Pa(Pb)) ≅ (Pa(Pb)) (Pa(Pa)) = (Pa(Pb)) .

Unfortunately, that gets us nowhere!

P**ab** (Pxy(Pyx))

≅ P**ab** (Pxy(Pyx)) (Pxy(Pyx))[**a**/x,**b**/y]

= P**ab** (Pxy(Pyx)) (P**ab**(P**ba**))

= P**ab** (Pxy(Pyx)) ((P**ba**))

= P**ab** (Pxy(Pyx)) P**ba**

A is said to 'dominate' B, and B is said to be 'derivable' from A, if and only if

A ≅ AB.

In such a case we may write for brevity

A » B .

Exercise for the reader: show (i) if A≥B, that is, if A dominates B in the CL sense, then A»B (ii) A»A (iii) if A»B and B»C, then A»C (iv) if A»B and B»A than A≅B.

If A, B, C are expressions such that B » C, then

A B » A C .

The premise tells us

B ≅ B C .

Therefore, by Lemma 1.1,

A B ≅ A B C = A B A C

(by copy). Therefore AB dominates AC ◊

We may rewrite the steps of Example 1.2 as follows:

P**ab** (Pxy(Pyx))

» P**ab** (Pxy(Pyx))[**a**/x,**b**/y]

= P**ab** (P**ab**(P**ba**))

= P**ab** ((P**ba**))

= P**ab** P**ba**

» P**ba**,

therefore,

P**ab** (Pxy(Pyx)) » P**ba** .

Thus P**ba** is derivable from the initial
expression P**ab** (Pxy(Pyx)). With a little practice, such derivations may be written
down immediately, without having to go through the intervening steps.

These, then, are the somewhat peculiar rules of the CLS Calculus. It is hard to believe that any good could come of them. All the more surprising, then, that they turn out to be the very key to logical thought - the distilled essence of Predicate Logic.