GEORGIAN MATHEMATICAL JOURNAL: Vol. 6, No. 2, 1999, 179-190

A N. BOURBAKI TYPE GENERAL THEORY AND THE

PROPERTIES OF CONTRACTING SYMBOLS AND CORRESPONDING CONTRACTED FORMS

SH. PKHAKADZE †

Abstract. A system of contracting symbols is introduced for a N. Bourbaki type general mathematical theory corresponding to a general classical mathematical theory T .

The classical formal mathematical theory corresponding to the formal theory T^{∗} of N. Bourbaki [1] is studied in [2], where a notation theory for N. Bourbaki’s formal theory is developed. The goal of this paper is to study similar questions for a N. Bourbaki type general mathematical theory corresponding to the general classical mathematical theory T defined in [3].

1. The Notation Theory for T

We first recall very briefly and somewhat informally some basic definitions concerning the introduction of contracting symbols in the theory T . We do not define the employed concepts in their full generality, and refer to [3] for more details.

The alphabet A of T may contain (a) an enumeration of n-ary predicate variables and/or improper constants, called also n-ary predicate letters or n-ary relational special letters or simply n-ary predicates. 0-ary predicate variables (constants, letters) are also called propositional variables (constants, letters); (b) an enumeration of n-ary substantive special variables and/or improper constants, called also n-ary substantive special letters or n-ary functions. 0-ary function variables (constants, letters) are called also

179 object variables (constants, letters); (c) operator signs and (d) simple operators. Improper predicate and function constants are similar to variables in that they can be bound. All the above symbols are called main, in order to distinguish them from the defined or contracting symbols to be introduced below. Variables and improper constants introduced in (a) and (b) are also called quantifier letters.

1991 Mathematics Subject Classification. 03B99.

Key words and phrases. General classical mathematical theory T , N. Bourbaki type general mathematical theory, extension of the theory T with contracting symbols, notation theory, contracting symbol.

* This paper is the English version of the original Russian manuscript by the late Prof. Shalva Pkhakadze (1919–1994) translated by Dr. Z. Khasidashvili who also added Section 1 which is a survey of [3].

1072-947X/99/0300-0179$12.50/0 \begin{matrix}c \\ ◯ \end{matrix} 1997 Plenum Publishing Corporation

Every simple operator has a weight or an arity n, and every operator sign σ has a weight or arity (n, m), such that all or some (specified below) words of the form σa_{1} … a_{m}, where a_{1} … a_{m} are variables or improper constants (i.e., quantifier letters), are compound operators or quantifiers with weight (arity) n. Each a_{i} ranges (independent of other a_{j}’s) over all quantifier variables or letters of one of the types (a) or (b) above. Further, n = 0 implies m = 0. The occurrences of a_{1} … a_{m} in σa_{1} … a_{m} are called the operator letters of σa_{1} … a_{m}. (Thus operator letters are occurrences of quantifier letters; the latter are not occurrences.)

Every quantifier σa_{1} … a_{m} (and the corresponding quantifier sign σ) has a binding indicator which is a tuple (m_{1}, …, m_{l}), where m_{1}, …, m_{l} is a subsequence of 1, …, m. The binding indicator specifies the binding scope of the quantifier. When (m_{1}, …, m_{l}) ≠ (1, …, m), the operator is partial; otherwise it is total. For example, the integral ∫_{A_{1}}^{A_{2}} A dx in our notation is written as ∫ xA_{1}A_{2}A, where ∫ is a quantifier sign with arity (3, 1), logicality indicator ( ), and binding indicator (3); x is an object variable, i.e., 0-ary function variable; and A_{1}, A_{2}, A are terms (to be defined below). So the quantifier ∫ x binds free occurrences of x only in A.

Further, every operator has a logicality indicator – a tuple (n_{1}, …, n_{k}), where n_{1}, …, n_{k} is a subsequence of 1, …, n. If (n_{1}, …, n_{k}) = ( ), resp. (n_{1}, …, n_{k}) = (1, …, n), then the operator is called special, resp. logical; otherwise, it is logical-special. Finally, every operator is either relational or substantive. This classification of operators is needed to correctly construct (and distinguish between) formulas and terms, and will be clear in the next paragraph.

In T , syntactically correct expressions are forms; a form is either a term or a formula. Terms are forms of the same type, and so are formulas – the former are object forms, and the latter are propositional forms. Terms and formulas are defined inductively as follows: propositional letters are formulas and object letters are terms. Further, if σa_{1} … a_{m} is an n-ary (simple or compound) operator (m ≥ 0, n > 0) with logicality indicator (n_{1}, …, n_{k}) and A_{1}, …, A_{n} are such forms that A_{n_{1}}, …, A_{n_{k}} is the maximal subsequence of formulas in the sequence A_{1}, …, A_{n}, then σa_{1} … a_{m}A_{1}, …, A_{n} is either a formula or a term depending on whether the operator σ is relational or substantive.

Free and bound occurrences (of variables and improper constants) in a form are defined as usual, where it is understood that if the binding indicator of a quantifier σa_{1} … a_{m} is (m_{1}, …, m_{l}), then its (explicit) occurrence in a form σa_{1} … a_{m}A_{1}, …, A_{n} binds free occurrences of a_{i} only in the arguments A_{m_{1}}, …, A_{m_{l}}. Two forms are called congruent if one is obtained from the other by renaming the bound variables. A word of the form (A_{1} … A_{n}/a_{1} … a_{n})A_{0}, where A_{1} … A_{n}, A_{0} are forms, a_{1} … a_{n} are 0ary quantifier variables (i.e., propositional or object variables or improper constants), and A_{i} and a_{i} are of the same type, denotes the result of simultaneous substitution of A_{1} … A_{n} for free occurrences of a_{1} … a_{n} in A_{0}. This may require the renaming of the bound variables and improper constants in A_{0} to avoid capture of free variables of A_{i} after the substitution.

Let a_{1}, …, a_{m} be metavariables such that each a_{i} ranges over the class of all predicate or object quantifier variables or letters; and let A_{1}, …, A_{n} be metavariables such that each A_{j} ranges over the class of all formulas or all terms (of the theory T or its extension). Forms constructed using the metavariables a_{1}, …, a_{m}, A_{1}, …, A_{n} and ( / )-substitutions are defined similarly to forms, by (a) declaring that the metavariables A_{1}, …, A_{n} are forms of the corresponding type; (b) identifying the metavariables a_{1}, …, a_{m} with letters of the corresponding type; and (c) declaring that words of the form (A′_{1} … A′_{k}/a′_{1} … a′_{k})A′_{0} are forms, where A′_{j} are forms, a′_{i} are metavariables from the list a_{1}, …, a_{m}, and the types match (i.e., A′_{i} and a′_{i} are of the same type, i = 1, …, k).

Now we can introduce definitions of contracting symbols in the theory T . The theory obtained from T by adding contracting symbols in the alphabet (as main symbols of corresponding types) is denoted by T̃. New symbols – operators and operator signs – are introduced in some order, and each definition has the form

σa_{1} … a_{m}A_{1} … A_{n}  B,  (1)

where a_{1}, …, a_{m}, A_{1}, …, A_{n} are metavariables, each ranged over a class of quantifier letters or forms (as specified above), and B is a form constructed using metavariables and ( / )-substitutions. Besides main operators, B may contain only the previously introduced contracting symbols.

Depending on further conditions imposed on B, the contracting symbols are classified into types I, II, II′, III, IV, IV′, V, V I, V I′ and V II. Descriptions of types I, II, II′, III and IV′ can be obtained by weakening some conditions in the definition of type IV. The remaining types V, V I, V I′ and V II are introduced [3] mainly to demonstrate that, after weakening some of the restrictions imposed on the other types, many desirable properties of the class of contracting symbols are no longer valid. Therefore we do not consider these types of contracting symbols here. It will be clear from the definition below that the weight, logicality indicator and binding indicator of a contracting symbol can be determined from its definition.

Type IV: Besides the conditions specified above, the right-hand side B of definition (1) satisfies the following conditions (a_{1S}), (b_{S}), (c_{1}) and (d_{S}):

(a_{1S}) B is a form constructed using ( / )-substitutions and metavariables

a_{1} … a_{m}, A_{1} … A_{n}, b_{1}, …, b_{k}  (2)

and containing these metavariables, where b_{i} is a metavariable ranged over a class of quantifier letters or quantifier variables of some type (i = 1, …, k). All explicit occurrences of quantifier letters in B, as well as occurrences of metavariables a_{1}… a_{m}, b_{1}, …, b_{k}, are bound. Further, there is a subsequence m_{1}, …, m_{l} of 1, …, n such that every one of the metavariables A_{m_{1}}, …, A_{m_{l}} is in the binding scope of quantifiers among whose operator variables occur a_{1}, …, a_{m}, and possibly (only) some of the metavariables b_{1}, …, b_{k}; the remaining metavariables A_{i} (i.e., with i ≠ m_{1}, …, m_{l}) may be in the scope of quantifiers whose operator variables are occurrences of some of the metavariables b_{i}.^{1} Furthermore, l = 0 iff m = 0. Finally, the order of metavariables in the list b_{1}, …, b_{k} is determined by their first occurrences in B.

(b_{S}) Groups of bound letters of B remain groups of bound letters after replacing the metavariables a_{1} … a_{m} by any letters from their range.

(d_{S}) The metavariables b_{1}, …, b_{k}, unlike other metavariables, cannot be instanciated independent of the values of other metavariables. Namely, the system of values

a′_{1} … a′_{m}, A′_{1} … A′_{n}, b′_{1}, …, b′_{k}

of metavariables (2) is admissible if and only if the following two conditions are satisfied: (d_{1S}) The letters b′_{1}, …, b′_{k} are mutually different, are different

from the letters a′_{1} … a′_{m}, do not have free occurrences in the forms A′_{1} … A′_{n}, and do not have (any) occurrences in B.

(d_{2}) The indexes of the letters b′_{1}, …, b′_{k} are chosen minimal (recall that these letters are chosen from the alphabetic enumeration of quantifier letters of the corresponding type).

(c_{1}) Let α be an admissible system of metavariables (2) with respect to an extension T̃_{a} of T̃; let A′ be the form of T̃_{a} obtained from the left-hand side of (1) by substituting the system α; and let B′ be the form of T̃_{a} obtained from B first by substituting the system α for corresponding metavariables, and then evaluating all ( / )- substitutions (if any) in the left to right inside-out order. Then the forms A′ and B′ have the same sets of free variables.^{2} The expression

1The tuple (m_{1}, …, m_{l}) is actually the binding indicator of σ.

A′  B′  (3)

is called an instance of definition (1). The definition of contracting symbols of type IV′ is obtained from the

above definition by removing the condition (d_{2}). If we require that B contain no ( / )-substitutions, then from definitions of types IV and IV′ we get definitions of types II and II′, respectively (the condition (c_{1}) above is trivially valid for such B). And if we require that the list of additional metavariables b_{1}, …, b_{k} be empty, we get definitions of types I and III from the definitions of types II and IV, respectively.

The following is an example of a definition of a contracting symbol of type IV (resp. IV′):

∃_{1}aA ∃aA ∧ ∀a∀b(A ∧ (b/a)A → a = b),

where a is an object quantifier letter (i.e., an object variable or improper constant), and b is the object quantifier letter with the minimal index (resp. any object quantifier letter) that is different from a and does not have free occurrences in A. The following (simpler) definition introduces a contracting symbol, ⊆, of types II and II′, which is not a contracting symbol of type I.

⊆ AB ∀b(b ∈ A → b ∈ B).

By definition, a form A of the theory T̃ denotes or is a contracted form of any form of the theory T obtained from A by eliminating the occurrences of contracting symbols in an inside-out order, i.e., by repeated replacement of occurrences of left-hand sides of definition instances (3) with the corresponding right-hand sides, in an inside-out order. It is proved in [3] that such processes (called γ′-processes) are all finite (recall that in the righthand side of a definition only previously defined contracting symbols may occur) and end with congruent forms of T . Thus any term of T̃ denotes exactly one form of T , up to congruence. This allows us to define the axioms and inference rules in the theory T̃ from the axioms and rules of the theory T .

More general processes of reconstruction of forms of T from the contracted forms, called α-processes, are also introduced in [3], which allow the elimination of contracting symbols in any order. It is shown that, for the case of contracting symbols of types I, II, II′, all such processes again terminate with the same result, up to congruence. Algorithms for computing the exact upper and lower bounds for the number of steps of α-processes, as well as algorithms for constructing the longest and shortest α-processes, are also presented. Further results on α-processes are obtained in [4], [5].

2We need to consider an extension _{T_{a}} of _{T} only if the alphabet of _{T} does not contain enough symbols to detect ‘erasure’ of occurrences of free variables in the operands (arguments) of σa_{1} … a_{m}.

2. The Theory T^{∗}

A N. Bourbaki type general mathematical theory T^{∗} corresponding to the general classical mathematical theory T is defined as follows. The alphabet A^{∗} of the theory T^{∗} consists of symbols of the alphabet A of the theory T and of some of the symbols from the following lists:

□_{0}, □_{1}, □_{2}, …,  (4)
□^{0}, □^{1}, □^{2}, ….  (5)

Further, the alphabet A^{∗} contains □_{n} if and only if the alphabet A of the theory T contains n-ary quantifier function letters, and A^{∗} contains □^{n} if and only if the alphabet A contains n-ary quantifier predicate letters. Symbols from the lists (3) and (4) are called quasiletters. Further, □_{n} is called (quantifier) n-ary substantive (function) quasiletter, and □^{n} is called (quantifier) an n-ary predicate quasiletter. Moreover, □_{0} is also called an object quasiletter and □^{0} is also called a propositional quasiletter. By definition, n-ary predicate quasiletters and n-ary predicate letters are of the same type, and similarly for n-ary function quasiletters and n-ary function letters.

In the case of the formal theory of N. Bourbaki, the alphabet contains only one quasiletter – an object quasiletter, and the symbol □ is used for □_{0}.

All definitions in the theory T concerning the notion of operator (in particular, quantifier) remain valid for the theory T^{∗}.

Let σδ_{1} … δ_{m} be a quantifier, where σ is an operator sign and δ_{1} … δ_{m} are operator letters. We call σ □′_{1} … □′_{m} a quasiquantifier if □′_{i} is a quasiletter of the same type as δ_{i} (i = 1, …, m) and □′_{i}\underline{\overline{∘}}□′_{j} if and only if δ′_{i}\underline{\overline{∘}}δ_{j}. In the latter case, σ □′_{1} … □′_{m} is called the quasiquantifier corresponding to σδ_{1} … δ_{m}. The quasiquantifier corresponding to σδ_{1} … δ_{m} is determined uniquely. However, the same quasiquantifier may correspond to different quantifiers. Moreover, the number of quantifiers corresponding to a given quasiquantifier is infinite.

The operator letters of a quantifier (which are occurrences of letters) fall into groups of graphically equal letters. These groups are enumerated by positive natural numbers according to the order of their first members, from left to right. Operator quasiletters in a quasiquantifier are grouped and enumerated similarly.

Symbols of the alphabet A^{∗} of the theory T^{∗} will also be called signs. An assemblage of the theory T^{∗}, by definition, is a word of the alphabet

A^{∗} of T^{∗} with links, where a link in an assemblage is defined as follows. A link in an assemblage A consists of vertical segments coming out of symbols of A, and of a minimal horizontal segment connecting the upper endpoints of all the above vertical segments. Further, the number of vertical segments in a link must be at least two, and there may be at most one vertical segment coming out of a symbol in the assemblage belonging to that link. It is required that the number of links in an assemblage be finite, horizontal segments not intersect, any different links cross only at separated (finite number of) points. From the conditions above it follows easily that vertical segments do not intersect. The links in an assemblage are enumerated by positive natural numbers according to the order of their first vertical segments, from left to right.

Let A be an assemblage, let C be its link, let A be the set of all symbols from which vertical segments of C are coming out, and let B be an arbitrary non-empty subset of A. Then we say that C binds or links symbols in the set B. The phrase C binds a symbol a, where a is an element of A, is interpreted similarly. By the set of symbols bound by the link C we mean the maximal set of symbols bound by C.

Clearly, any word of the alphabet A^{∗} is an assemblage of A^{∗}. The empty word is called the empty assemblage.

The following is an example of an assemblage:

σ ∨ ∧ ∈ x y ∈ z ∧ □_{1} □^{0} □_{2}

Here the first link binds three symbols, and the second one binds four symbols.

The base of an assemblage, by definition, is the word obtained from the assemblage by removing all links. Hence an assemblage consists of a base and a system of links.

Let A be an assemblage, let C be a link of A, and let B be a part of the base of A. We say that the link C is above the part B if it is possible to draw a vertical segment out of a symbol of B that crosses the horizontal segment of C. Here B can be a symbol of the base of A.

In the above example of an assemblage, every link is above the first occurrence of the symbol ∈. The first and second links are above the symbol σ (that is, above the first occurrence of the symbol σ).

We say that an assemblage B has an occurrence in an assemblage A if A can be represented as A_{1}, B, A_{2}, where A_{1} and A_{2} are assemlages. The triple (A_{1}, B, A_{2}) will be called an occurrence of the assemblage B in the assemblage A. The occurrences of B in A are enumerated according to the growth (of the length) of the first component. An occurrence will be identified with its second component.

An occurrence of an assemblage in an assemblage A will be called a part of the assemblage A. It is easy to see that if B is a part of an assemblage A, then the system of links of the part (assemblage) B coincides with the system of all links of A that are above B.

By definition, two assemlages are graphically equal if their bases are graphically equal, the numbers of their links are equal, and the corresponding links (i.e., links with the same numbers) bind corresponding sets of symbols (of the bases). We write the fact that A and B are graphically equal as A\underline{\overline{∘}}B. Clearly, the graphical equality of assemlages is a generalization of the graphical equality of words.

In the theory T^{∗}, formulas and terms are called forms, where formulas and terms are defined as follows:

1. If A is a propositional letter, then A is a formula.

2. If A is an object letter, then A is a term.

3. If σ is a simple n-ary operator (n > 0) with the logicality indicator (n_{1}, …, n_{k}) and A_{1}, …, A_{n} are such forms of the theory T^{∗} that A_{n_{1}}, …, A_{n_{k}} is the maximal subsequence of formulas in the sequence A_{1}, …, A_{n}, then σA_{1}, …, A_{n} is either a formula or a term depending on whether the operator σ is relational or substantive.

4. If σδ_{1} … δ_{m} is an n-ary quantifier of the theory T^{∗} (or equivalently, of the theory T ) with operator letters δ_{1} … δ_{m}, logicality indicator (n_{1}, …, n_{k}), and binding indicator (m_{1}, …, m_{e}), and A_{1}, …, A_{n} are such forms of the theory T^{∗} that A_{n_{1}}, …, A_{n_{k}} is the maximal subsequence of formulas in the sequence A_{1}, …, A_{n}, then σδ_{1} … δ_{m}A_{1}, …, A_{n} denotes the assemblage obtained from the assemblage B\underline{\overline{∘}}σδ_{1} … δ_{m}A_{1}, …, A_{n} in the following way. Let □′_{k_{i}} denote □^{k_{i}} or □_{k_{i}} depending on whether δ_{i} is a k_{i}-ary predicate symbol or a k_{i}-ary function symbol (i = 1, …, m). Further, let δ_{i_{1}}, …, δ_{i_{k}} be obtained from δ_{1}, …, δ_{m} by removing the repeated occurrences (i_{1} = 1). Then we construct a number of short vertical segments coming out of the explicit occurrence of σ in B, and enumerate them, from left to right, by positive natural numbers. Further, for every j ∈ {1, 2, …, k}, we replace every occurrence of the letter δ_{i_{j}} in the parts δ_{1}, …, δ_{m}, A_{m_{1}}, …, A_{m_{e}} of the assemblage B by the quasiletter □′_{k_{i_{j}}} and, for every j ∈ {1, …, k}, we construct a link connecting the explicit occurrence of σ in B with the substituted occurrences of the quasiletter □′_{k_{i_{j}}} in such a way that the link contains the j-th vertical segment coming out of the explicit occurrence of σ in B. The thus obtained assemblage is denoted by the assemblage σδ_{1} … δ_{m}A_{1}, …, A_{n}.

5. A is a formula or a term if and only if this follows from Items 1–4

above. The initial part of the base of the form B′, denoted by the assemblage

σδ_{1}… δ_{m}A_{1}, …, A_{n} from the Item 4 of the previous definition, consisting of m + 1 symbols is a quasiquantifier. In a process of construction of larger forms using the form B′ that quasiquantifier does not change.

By definition, a part of a form A is a part of an assemblage A that is a form. A part of the form A is called a propositional part or an object part depending on whether it is a formula or a term.

Remark. The definition of a part of a form in the theory T^{∗} is simpler than for the theory T (as in the case of T^{∗} forms do not contain quantifier variables). In the theory T , in a process of constructing larger forms from shorter ones, the latter forms become parts of the constructed (larger) forms. In the theory T^{∗}, this is not always the case. Shorter forms sometimes change. Sometimes shorter forms do not change, but still they do not remain parts of larger formulas when the latter are considered as assemlages. If a shorter form becomes a part of a larger form (considered as an assemblage), then it is also a part of the larger form. The above observations suggest that the language of the theory T is more convenient than the language of the theory T^{∗} (for studying some questions).

Let us mention some properties of forms of the theory T^{∗} whose proofs are not difficult.

(1) Every link of a form A of T^{∗} connects an operator sign of the form A and some occurrences of the same quasiletter to the right of that operator sign.

(2) If L_{1} and L_{2} are two different links of a form of T^{∗} and A and B are the sets of corresponding occurrences of symbols (i.e., the sets of symbols bound by these links), then either A and B do not intersect, or their intersection is a singleton consisting of an operator sign.

Formulas (of T^{∗}) will be called propositional forms and terms will be called object forms. We call formulas, respectively terms, forms of the same type. Forms defined in Items 1 and 2 are called simplest forms – simplest formulas and simplest terms respectively.

It is easy to see that:

Proposition 1. Let σ be an operator sign with weight (n, m), logicality indicator (n_{1}, …, n_{k}) and binding indicator (m_{1}, …, m_{p}), and let δ_{1}, …,δ_{m}, δ′_{1}, …, δ′_{m} and A_{1}, …, A_{n}, A′_{1}, …, A′_{n} be such sequences of letters and forms (respectively) that

σδ_{1} … δ_{m}A_{1}, …, A_{n} and σδ′_{1} … δ′_{m}A′_{1}, …, A′_{n}

are forms of the theory T^{∗} (i.e., are denotations of forms of T^{∗}). Further, let the following conditions be satisfied; 1. A_{i}\underline{\overline{∘}}A′_{i}, i ∈ \{1, 2, …, m\} \ \{m_{1}, …, m_{p}\}.

2. If i, j ∈ \{1, 2, …, m\}, then δ′_{i}\underline{\overline{∘}}δ′_{j} iff δ_{i}\underline{\overline{∘}}δ_{j}.

3. The letters δ′_{1} … δ′_{m} do not have occurrences in the bases of the assemlages A_{m_{1}}, …, A_{m_{p}}.

4. For every i ∈ {1, …, p}, the assemblage A′_{m_{i}} is obtained from A_{m_{i}} by simultaneous substitution of letters δ′_{1} … δ′_{m} for δ_{1} … δ_{m}.

Then the forms σδ_{1} … δ_{m}A_{1}, …, A_{n} and σδ′_{1} … δ′_{m}A′_{1}, …, A′_{n} of the theory T^{∗} are graphically equal.

Remark. The possibility of simultaneous substitutions mentioned in Item 4 above follows from condition 2. Simultaneous substitution of letters δ′_{1} … δ′_{m} for letters δ_{1} … δ_{m} in a form A requires (exactly) the replacement of every occurrence of δ_{i} in A by δ′_{i}. This is not always possible. For example, this is impossible if δ_{1}\underline{\overline{∘}}δ_{2} but δ′_{1} \underline{\overline{∘̸}}δ′_{2}.

We will consider a form A of the theory T as a denotation of the uniquely determined form A^{∗} of the theory T^{∗}, defined by the following algorithm Γ.

We add to the alphabet of T a proper propositional constant t and a proper object constant a, and obtain an extension \overline{T} of T . We denote this alphabet by \overline{A}. The theory \overline{T^{∗}} is obtained similarly.

Steps of the algorithm Γ determine a finite sequence of assemlages of the alphabet \overline{A} ∪ \{(,)\}

A_{0}\underline{\overline{∘}}A, A_{1}, …, A_{k},

whose last member is A^{∗}. Further, A_{k} is obtained from A_{k−1} by removing all parentheses; and every A_{i} (i = 0, 1, …. , k − 1) satisfies the following conditions:

A part of the assemblage A_{i} may be an expression enclosed in a pair of parentheses. Every such an expression without the enclosing pair of parentheses is a form of T^{∗}; and if we identify these expressions with t or a depending on their type, then A_{i} becomes a form of the theory \overline{T} . Furthermore, A_{k−1} does not contain quantifiers, and all the preceding members do.

Finally, A_{i+1} is obtained from A_{i} (i = 0, 1, …, n − 2) as follows.

We find in A_{i} the first from the right quantifier σδ_{1} … δ_{m} with operands A′_{1}, …, A′_{n}, where every expression enclosed in a pair of parentheses as above is considered as the formula t or the term a. Further, by considering the expressions with parentheses as forms of the theory T^{∗} (by removing the parentheses), these operands become forms A′′_{1}, …, A′′_{n} of the theory T^{∗} (as they do not contain quantifiers). Further, we find the assemblage denoted by the assemblage σδ_{1} … δ_{m}A′′_{1}, …, A′′_{n} (as this is done in Item 4 of the definition of a form). We enclose thus obtained form of the theory T^{∗} in parentheses and substitute it for the part σδ_{1} … δ_{m}A′_{1}, …, A′_{n} in A_{i}.

Now it is easy to prove

Theorem 1. Any form A of the theory T is a denotation of the uniquely determined form A^{∗} of the theory T^{∗}. Further, two forms of the theory T denote the same form of the theory T^{∗} if and only if the two forms are congruent. And if a form A of the theory T is a denotation of the form A^{∗} of the theory T^{∗}, then either both forms are formulas, or both are terms (of the corresponding theories).

It follows from the above theorem that, in order to determine the class of all forms of the theory T that denote a form A^{∗} of the theory T^{∗}, it is enough to determine one denotation A of A^{∗}. (The class of denotations of the form A^{∗} is the class of all forms of T that are congruent to A^{∗}.)

A form A of the theory T which denotes a given form A^{∗} of the theory T^{∗} can be determined by the following algorithm Γ_{1}.

1. The zero step of the algorithm Γ needs to determine whether the assemblage A^{∗} contains an operator sign with a link. If there is a such an operator sign in A^{∗}, then the algorithm Γ does not halt with the zero step. Otherwise, the algorithm halts with the result A_{0}\underline{\overline{∘}}A^{∗}, and A_{0} (i.e., A^{∗}) is a form of the theory T and is a denotation of the form A^{∗}. In the latter case, A^{∗} does not contain an operator sign and its denotation is determined uniquely (the class of forms congruent to A_{0} (A_{0}\underline{\overline{∘}}A^{∗}) is a singleton containing A_{0} (i.e., A^{∗})).

2. If i > 0 and the algorithm does not halt with the (i−1)-th step, then the i-th step is defined as follows (it is assumed that A_{k} denotes the result of the k-th step). Find in the assemblage A_{i} the first from the right quantifier sign σ with a link. Let C be the first link associated with σ. Replace all symbols different from σ and linked by C by the quantifier letter δ satisfying the following conditions:

(a) The type of δ and the type of the symbols that it replaces are the same (the replaced symbols are graphically equal quasiletters; that quasiletter will be denoted by □).

(b) For every j ∈ {i_{1}, …, i_{k}}, δ is admissible as the j-th operator letter in the quantifier obtained from σ, where i_{1}, …, i_{k} are the numbers of occurrences of □ in the part of the assemblage A_{i−1} consisting of m symbols following σ.

(c) δ does not occur in A_{i−1}.

(d) The subscript of δ in minimal. The existence of such a quantifier variable δ follows from the definition of forms. It is not difficult to choose such a quantifier letter, and the last condition is introduced to guarantee its uniqueness. Finally, we need to remove the above link C. The thus obtained assemblage is the result of the i-th step and is denoted by A_{i}. The i-th steps needs also to determine whether the assemblage A_{i} contains an operator sign with a link. If there is such an operator sign in A_{i}, then the algorithm does not halt. Otherwise, the algorithm halts with the result A_{i} – A_{i} is a form of the theory T and is the desirable denotation of the form A^{∗} (any link of a form in the theory T^{∗} is associated with an operator sign). Clearly, the type of the form A_{i} coincides with the type of the form A^{∗}.

We will use forms of the theory T̃ to denote forms of theory T^{∗} (where T̃ is the extension of the theory T with contracting symbols of types I − IV, II′ and IV′) as follows: If the form Ã of the theory T̃ denotes a form A of the theory T , and A denotes the form A^{∗} of the theory T^{∗}, then we will assume that Ã is a denotation of the form A^{∗} of the theory T^{∗}, and that contracting symbols of the theory T , of one of the types above, are contracting symbols for the theory T^{∗} of the same type.

References

1. N. Bourbaki, Éléments de mathématique. Théorie des ensembles, Chapitres 1 et 2. Troisième édition, Hermann, Paris, 1966.

2. Kh. M. Rukhaia, The description of a derived formal mathematical T^{∗} theory. (Russian) Tbiliss. Gos. Univ. Inst. Prikl. Mat. Trudy 21(1983), 75–98.

3. Sh. S. Pkhakadze, Some problems of the notation theory. (Russian) Tbilisi University Press, Tbilisi, 1977.

4. V. Sh. Pkhakadze, Some properties of α-processes. (Russian) Tbiliss. Gos. Univ. Inst. Prikl. Mat. Trudy 26(1988), 34–59.

5. V. Sh. Pkhakadze, Substitution theorems and connection between δ-processes and α-processes. (Russian) Tbiliss. Gos. Univ. Inst. Prikl. Mat. Trudy 26(1988), 60–106.

(Received 17.05.1994; translated and revised 22.09.1997)