Victor Porton

Finite and infinite formulas are considered axiomatically.

# Part 1. Axiomatic Theory of Formulas

## Preface

### Overview

This new mathematical theory developed by the book author researches the *properties of mathematical formulas* (aka *expressions*). Naturally this theory is essential for the mathematics.

Formulas are encountered in all areas of mathematics. Probably of special interest are propositional formulas in math logic. Using Operator Theory of Formulas may probably simplify proofs of math logic theorems.

The Theory of Formulas is a new foundation for math logic which is the foundation of mathematics. That is the Theory of Formulas is the *foundation of the foundation of mathematics*.

This theory researches mathematical formulas as well as any other objects which have constituent parts of different kinds (*without* the limit that a whole cannot be a part of its part, that is loops are not disallowed). For example, consider relations between objects in the memory of a computer or components of an electronic scheme connected with different kinds of links.

The Operator Theory of Formulas is not limited only to finite neither only to acyclic formulas. Infinite and cyclic (e.*g*. *a*(*b*(*a*(*b*(…))))) formulas are also modeled by this theory. A common example of a system of infinite formulas is the set of irrational numbers. Another example of an infinite formula may be the entire mathematics in the form of some formalism (e.*g*. all groups of Group Theory).

This book contains a new axiomatic theory, the theory of *constructs*, and its specializations, including the theory of *formulas*:

- Informally, a construct is anything what has indexed components (parts).
*E*.*g*., the*a*-(*b*+*c*) can be considered as a construct which has “*a*” as the part with index 1, “-” as the part with index 2, and (*b*+*c*) (a subformula) as the part with index 3. - Formulas is a particular case of constructs. Informally, a formula is a construct which contains symbols.
*E*.*g*.*a*-(*b*+*c*) would be a formula which contains symbols such as*a*,*b*,*c*, +, -.

To increase flexibility and power of the theory I study operators (functions) on the sets of constructs rather than the constructs themselves. So different kinds of constructs can be researched with a uniform method.

An important aspect of the theory of formulas accordingly this book is so called *specialization* that is adding additional subexpressions to expressions. For example if + would mean an abelian group operation, +_{1} (+ with added additional subformula “1”) would mean e.g. addition of whole numbers which is a specialization of abelian group operation etc. Specialization can be used instead of variable substitution.

Recall that *formalist philosophy* is a school in philosophy of mathematics which considers mathematical formulas as physical objects. For this new theory of formulas which includes infinite logical formulas that philosophy (“formalism”) is not applicable as infinite formulas cannot be written and are not physical objects in this sense. So this theory also changes the philosophy of mathematics.

### Draft Status

*This is *a* preliminary version. If you will find any mistakes, please contact me.*

## Bases

### Definition of **a** Basis

Before studying systems of constructs and formulas, I will introduce the concept which I call a *basis*:

A *basis*^{1} is a pair of a set *E* and some set *X* (set of *indices* or *indexes*) of functions on *E*.

**Remark.** In other words, a basis is an universal algebra (with possibly infinite set of operations *X*) having only unary operations. Such algebras are sometimes called *unary algebras*. (There are a subtle difference about different operations to which corresponds the same function, but I will lay aside this issue, to be more concise.)

I will call a function from *E*_{1} to *E*_{2} an *operator* from a basis Base_{1} to a basis Base_{2}. An operator from a basis to itself will be called an operator *on* this basis.

I will denote bases as Base, Base_{1}, Base_{2}, …

**Obvious.** Indices are operators on the basis.

By definition *S* (I call it the *set of sequences*) is the set of all finite sequences *p*_{n}…*p*_{0} of zero or more indices *p*_{i} ∈ *X*. To a sequence of indices corresponds an operator on *E*: (*p*_{n}…*p*_{0})α = *p*_{n}(p_{n}_{ – 1}…(*p*_{0}α)…).

**Remark.** *S* is a monoid with empty sequence () being the identity element.

### Morphisms of Bases

Below I will analyze relations between several bases. For simplicity of explanation I will consider only the case when *X*_{1} = *X*_{2} = … = *X*.

The case of two bases (*E*_{1}, *X*_{1}) and (*E*_{2}, *X*_{2}) such that *X*_{1} ≠ *X*_{2} can be eliminated using *reindexing*. *Reindexation* as defined below is a generalization of coordinate system transformation (as found for example in linear algebra).

#### Reindexation (Coordinate Transformation)

For two sets *E*_{1} and *E*_{2} some *f* can be operator on both *E*_{1} and *E*_{2} (for example if *f* is a function *E*_{1} ∪ *E*_{2} → *E*_{1} ∩ *E*_{2}).

For simplicity I will implicitly assume below that *E*_{1} ∩ *E*_{2} = ∅. (If *E*_{1} ∩ *E*_{2} ≠ ∅ we can replace *E*_{1} with *E*_{1} × {1} and *E*_{2} with E_{2} × {2}.)

**Definition.** Let *X*, λ*X* be sets, λ (called a *reindexation function*) be an operator *X* → λ*X* and let (*E*_{2}, λ*X*) be a basis. For *i* ∈ *X*, β ∈ *E*_{2} we will define *i*β = (λ*i*)β. After this definition *i* became an operator also on *E*_{2} and (*E*_{2}, *X*) becomes a basis. The basis (*E*_{2}, *X*) = λ^{-1}(*E*_{2}, λ*X*) is called *reindexed* (with λ) basis (*E*_{2}, λ*X*).

Reind(λ) (called *reindexation*) is a function from (*E*_{2}, λ*X*) to λ^{-1}(*E*_{2}, λ*X*) = (*E*_{2}, *X*) that maps every element to itself (but changes the meaning of indices as shown in the following proposition).

**Proposition.** *i*Reind(λ) = Reind(λ)(λ*i*) for *i* ∈ *X*.

**Proof.** Let α is a construct of the system of constructs (*E*_{2}, λ*X*). Then Reind(λ)α is a construct from (*E*_{2}, *X*). So *i*Reind(λ)α = Reind(λ)(λ*i*)α. **End of proof.**

**Remark.** The above proposition may be not true for *i* ∈ *S*!

When we have two bases (*E*_{1}, *X*_{1}), (*E*_{2}, *X*_{2}) and a pair (Ψ, λ) of an operator Ψ from *E*_{1} to *E*_{2} and a reindexation function λ from *X*_{1} to *X*_{2}, we can first apply reindexing to get the basis (*E*_{2}, *X*_{1}) and then consider Ψ as an operator from (*E*_{1}, *X*_{1}) to (*E*_{2}, *X*_{1}). (I recall that below we will consider only the cases of bases with the same set of indices.)

##### Coordinate Transformation with an Operator

Let (*E*, *X*) be a basis. Let *f* be an operator on *E*.

**Definition.** Functions λ_{L}(*f*) and λ_{R}(*f*) on *X* are defined as λ_{L}(*f*)*i* = *fi*; λ_{R}(*f*)*i* = *if*.

**Definition.** *Left coordinate transformation* and *right coordinate transformation* of a basis are defined correspondingly as:

*L*(*f*) = Reind(λ_{L}(*f*)) and *R*(*f*) = Reind(λ_{R}(*f*)).

**Proposition.** *iL*(*f*) = *L*(*f*)*fi* and *iR*(*f*) = *R*(*f*)*if* for *i* ∈ *X*.

**Proof.** By properties of reindexation. **End of proof.**

**Proposition.** For *p*_{1}, …, __p___{n} ∈ *X*

*p*_{n}…*p*_{1}*R*(*f*) =*R*(*f*)*p*_{n}*f*…*p*_{1}*f*;*p*_{n}…*p*_{1}*L*(*f*) =*R*(*f*)*fp*_{n}…*fp*_{1}.

**Proof.** By properties of reindexation:

*p*_{n}…*p*_{1}*R*(*f*) =*p*_{n}…*p*_{2}*R*(*f*)*p*_{1}*f*=*p*_{n}…*p*_{3}*R*(*f*)*p*_{2}*fp*_{1}*f*= … =*R*(*f*)*p*_{n}*f*…*p*_{1}*f*.*p*_{n}…*p*_{1}*L*(*f*) =*p*_{n}…*p*_{2}*L*(*f*)*fp*_{1}=*p*_{n}…*p*_{3}*L*(*f*)*fp*_{2}*fp*_{1}= … =*L*(*f*)*fp*_{n}…*fp*_{1}.**End of proof.**

#### Morphisms of Bases

Morphisms of bases (with fixed set of indices *X*) are particular cases of universal algebra morphisms. Indeed for completeness I will define these here without using universal algebra.

By definition a *basis homomorphism* (or as a less fortunate term, *basis morphism*) from a basis (*E*_{1}, *X*) to a basis (*E*_{2}, *X*) is a function Ψ: *E*_{1} → *E*_{2} such that ∀*i* ∈ *X* : Ψ*i* = *i*Ψ.

**Proposition.** Ψ is a homomorphism iff ∀*i* ∈ *S* : Ψ*i* = *i*Ψ.

**Proof.** *Reverse implication.* Obvious.

*Direct implication.* Ψ*p*_{n}…*p*_{0} = *p*_{n}Ψ*p*_{n}_{-1}…*p*_{1} = … = *p*_{n}…*p*_{1}Ψ*p*_{0} = *p*_{n}…*p*_{0}Ψ. **End of proof.**

By definition a *basis **monomorphism* is an injective basis homomorphism.

By definition a *basis epi**morphism* is a basis homomorphism such that im Ψ = *E*_{2}.

By definition *basis isomorphism* is a basis homomorphism which is both monomorphism and epimorphism.

### Parts. Closed Sets

Let (*E*, *X*) is a basis.

**Definition.** The set of *direct parts* of α ∈ *E* is {*i*α | *i* ∈ *X*}.

**Definition.** The set of *parts* of α ∈ *E* is parts(α) = {*i*α | *i* ∈ *S*}.

**Definition.** The set *A* ⊆ *E* is *closed* iff ∀α ∈ *A* : parts(α) ⊆ *A*.

**Proposition.** If A is a set of element of a basis, the following statements are equivalent:

*A*is subconstruct closed.- ∀α ∈
*A*,*i*∈*X*:*i*α ∈*A*. - ∀α ∈
*A*,*i*∈*S*:*i*α ∈*A*.

**Proof.** (1) ⇔ (3) is obvious. (3) ⇒ (2) is obvious. (2) ⇒ (3) is easily provable by induction. **End of proof.**

Let the set *H* ⊆ *E* is closed. A basis Sys = (*E*, *X*) *limited* to the set *H* is by definition the basis Sys|_{H} = (*H*, *X*).

(The requirement that *H* is closed warrants that Sys|_{H} is really a system of constructs.)

## Operator Theory of Constructs

### Definition of Constructs

In the operator theory of constructs *constructs* are defined axiomatically:

I will call the *system of constructs* a pair consisting of a basis (*E*, *X*) and a 0 ∈ *E* (*null* or *nil* construct) such that ∀*i* ∈ *X* : *i*0 = 0.

**Remark.** We could generalize to consider instead a subset *Z* ⊆ *E* (elements of *Z* are called *null* or *nil* constructs) such that ∀*i* ∈ *X*, 0 ∈ *Z* : *i*0 = 0. But whether such a generalization has significant applications is unclear.

Elements of *E* will be called *constructs*. I will denote constructs (as well as formulas, see below) with small Greek letters.

**Remark.** The above is a reasonable formalization of often used informal notion of *mathematical construct*.

**Remark.** To a system of constructs corresponds an universal algebra with indices being unary operations and null constructs being constant symbols (nullary operations). That is a system of constructs is essentially the same as an algebra *having only nullary and unary operations* (the number of operations in not required to be finite) with axioms *i*0 = 0 for every unary operation *i* and the nullary operation 0.

**Remark.** An other variant of definition of *systems of constructs* is a pair of a set *E* and a set *X* of partial functions on *E*. (To switch to this definition, replace *E* by *E *\ {0} and remove points where functions on *E* take value 0. To switch back to the original definition replace *E* by *E *\ {0} for an arbitrary 0 ∉ *E* and extend every function *i* ∈ *E* by the formula *i*0 = 0.)

I will denote systems of constructs as Sys, Sys_{1}, Sys_{2}, … and the corresponding sets of constructs as *E*, *E*_{1}, *E*_{2}, …, corresponding sets of indices as *X*, *X*_{1}, *X*_{2}, … etc.

**Example.** Let *Y* is an arbitrary set (its element are called *symbols* or *terminals*). Let 0 ∉ *Y*. Let *E* is the set consisting of 0, *Y* and (recursively) of lists (finite sequences) of elements of *E*. Let *X* = ℕ. Let for *i* ∈ ℕ, α ∈ *E* define *i*α = 0 if α ∈ *Y* or α is a list shorter than *n*+1 elements, and otherwise *i*α is the *i*-th component of α (considered as a list). Then (*E*, *X*, 0) is a system of constructs. (Moreover (*E*, *X*, {0}, *Y*) is a system of formulas, see below.) This system is called *lists of lists*.

Let the set 0 ∈ *H* ⊆ *E* is closed. A system of constructs Sys = (*E*, *X*, 0) *limited* to the set *H* is by definition the system of constructs Sys|_{H} = (*H*, *X*, 0). Sys|_{H} is called a *subsystem* of Sys.

### Operators on Systems of Constructs

I will call an *operator* from a system of constructs (*E*_{1}, *X*, 0) to a system of constructs (*E*_{2}, *X*, 0) a function from *E*_{1} to *E*_{2} such that *f*0 = 0.

**Obvious.** Indices are operators.

#### Conditional Pass Operator

Let *p* is an operator. The *conditional pass* operator [*p*] is defined by the equations:

[*p*]α = α ⇐ *p*α ≠ 0; [*p*]α = 0 ⇐ *p*α = 0.

It is really an operator because *p*0 = 0 and so [*p*]0 = *p*0 = 0.

**Proposition.** *p*[*p*] = *p*.

**Proof.** *p*α ≠ 0 ⇒ *p*[*p*]α = *p*α and *p*α = 0 ⇒ [*p*]α = *pp*α = *p*α. **End of proof.**

**Proposition.** *p*α = 0⇒ [*p*]α = 0.

**Proof.** *p*α = 0 ⇒ [*p*]α = *p*α = 0.

**Theorem.** [*p*]*q* = *q*[*pq*] for any operators *p* and *q*.

**Proof.** *pq*α ≠ 0 ⇒ [*pq*]α = α; *pq*α = 0 ⇒ [*pq*]α = *pq*α;

*pq*α ≠ 0 ⇒ [*p*]*q*α = *q*α; *pq*α = 0 ⇒ [*p*]*q*α = *pq*α;

*pq*α ≠ 0 ⇒ *q*[*pq*]α = *q*α; *pq*α =* 0* ⇒ *q*[*pq*]α = *qpq*α = *pq*α.

So *pq*α ≠ 0 ⇒ *q*[*pq*]α = [*p*]*q*α and *pq*α = 0 ⇒ *q*[*pq*]α = [*p*]*q*α. ∀α ∈ *E* : *q*[*pq*]α = [*p*]*q*α. **End of proof.**

**Obvious consequence.** [*p*_{0}]*p*_{1}…*p*_{n} = *p*_{1}…*p*_{n}[*p*_{0}*p*_{1}…*p*_{n}] for any operators *p*_{0}, …, *p*_{n}.

**Theorem.** [*p*_{m}…*p*_{0}][*p*_{n}…*p*_{0}] = [*p*_{max(}_{n}_{,}_{m}_{)}…*p*_{0}].

**Proof.** It enough to prove [*qp*][*p*] = [*p*][*qp*] = [*qp*]. We have [*qp*][*p*] = [*p*][*qp*[*p*]] = [*p*][*qp*].

*p*α = 0 ⇒ [*p*]α = *p*α = 0 ⇒ [*qp*][*p*]α = *qp*[*p*]α = *qp*α; *p*α = 0 ⇒ *qp*α = 0 ⇒ [*qp*]α = *qp*α; *p*α = 0 ⇒ [*qp*][*p*]α = [*qp*]α.

*p*α ≠ 0 ⇒ [*p*]α = α ⇒ [*qp*][*p*]α = [*qp*]α.

So in any case [*qp*][*p*]α = [*qp*]α. **End of proof.**

### Construct Morphisms

#### Reindexation of Constructs

Let Sys_{1} = (*E*_{1}, *X*_{1}, 0_{1}) and Sys_{2} = (*E*_{2}, *X*_{2}, 0_{2}) be two systems of constructs. Let λ be a reindexation function from the basis (*E*_{1}, *X*_{1}) to the basis (*E*_{2}, *X*_{2}). Let the basis (*E*_{2}, *X*_{1}) be the reindexed (with λ) basis (*E*_{2}, *X*_{2}).

Then λ is called *reindexation function* from the system of constructs Sys_{1} to the system of constructs Sys_{2}. The system of constructs (*E*_{2}, *X*_{1}, 0_{2}) = λ^{-1}(*E*_{2}, *X*_{2}, 0_{2}) is called *reindexed* (with λ) system of constructs (*E*_{2}, *X*_{2}, 0_{2}).

To show that (*E*_{2}, *X*_{1}, 0_{2}) is really a system of constructs we need to prove that *i*0_{2} = 0_{1} for *i* ∈ *X*_{1}. We have *i*0_{2} = (λ*i*)0_{1} = 0_{1}.

The things said above about coordinate transformations of bases by functions apply as well to transforming a system (*E*, *X*, 0) of constructs (with additional requirement that Ψ0 = 0.)

As a conclusion, we can limit our further consideration to the case of systems of constructs having the same indices and the same null: (*E*_{1}, *X*, 0) and (*E*_{2}, *X*, 0). (However in the second part of this book we will again return to the topic of reindexation.)

#### Homomorphisms and Isomorphisms

By definition *construct homomorphism* is such a basis homomorphism Ψ that Ψ0 = 0. (I recall that we have limited our consideration to the case 0_{1} = 0_{2} = … = 0.)

**Obvious.** Composition of construct homomorphisms is a construct homomorphism.

**Definition.** *Construct monomorphism* is an injective construct homomorphism. *Construct epimorphism* is construct homomorphism such that its image of *E*_{1} is *E*_{2} and of 0_{1} is 0_{2}. *Construct isomorphism* is construct homomorphism which is both construct homomorphism and construct epimorphism.

**Obvious****.** The reverse of a construct isomorphism is a construct isomorphism.

#### Pseudomorphisms

**Definition.** *Construct pseudomorphism* from Sys_{1} to Sys_{2} is such operator from *E*_{1} to *E*_{2} that ∀*i* ∈ *X* : Ψ*i* = *i*Ψ[*i*].

**Proposition.** An operator Ψ from *E*_{1} to *E*_{2} is a construct pseudomorphism iff ∀*i* ∈ *S* : Ψ*i* = *i*Ψ[*i*].

**Proof.** *Reverse implication.* Obvious.

*Direct implication.* By induction by *n* for *p*_{i} ∈ *X*:

Ψ*p*_{n}…*p*_{0} = *p*_{n}…*p*_{1}Ψ[*p*_{n}…*p*_{1}]p_{0} = *p*_{n}…*p*_{1}Ψ*p*_{0}[*p*_{n}…*p*_{0}] = *p*_{n}…*p*_{0}Ψ[*p*_{0}][*p*_{n}…*p*_{0}] = *p*_{n}…*p*_{0}Ψ[*p*_{n}…*p*_{0}]. **End of proof.**

**Proposition.** Construct homomorphism is a construct pseudomorphism.

**Proof.** Let Ψ*i* = *i*Ψ. Then *i*α ≠ 0 ⇒ Ψ*i*α = *i*Ψα = *i*Ψ[*i*]α; *i*α = 0 ⇒ Ψ*i*α = *i*α = *i*Ψ*i*α = *i*Ψ[*i*]α. **End of proof.**

**Proposition.** Composition of construct pseudomorphisms is a construct pseudomorphism.

**Proof.** Let Ψ_{1} and Ψ_{2} are construct pseudomorphisms. We have Ψ_{2}Ψ_{1}*i*α = Ψ_{2}*i*Ψ_{1}[*i*]α = *i*Ψ_{2}[*i*]Ψ_{1}[*i*]α.

Ψ_{1}[*i*]α ≠ 0 ⇒ Ψ_{2}Ψ_{1}*i*α = *i*Ψ_{2}Ψ_{1}[*i*]α; Ψ_{1}[*i*]α = 0 ⇒ Ψ_{2}Ψ_{1}*i*α = Ψ_{1}[*i*]α = *i*Ψ_{2}Ψ_{1}[*i*]α.

So Ψ_{2}Ψ_{1}*i*α = *i*Ψ_{2}Ψ_{1}[*i*]α. **End of proof.**

##### Pseudomorphic Image

**Definition.** Let α ∈ *E*_{1}, β ∈ *E*_{2}, Then Pseud(α, β) ⇔ β is a *pseudomorphic image* of α ⇔ there exists a pseudomorphism Ψ from Sys_{1} to Sys_{2} such that β = Ψα.

**Proposition.** Pseud(α, β) ∧ Pseud(β, γ) ⇒ Pseud(α, γ) for α ∈ *E*_{1}, β ∈ *E*_{2}, γ ∈ *E*_{3}.

**Proof.** Because composition of pseudomorphisms is a pseudomorphism. **End of proof.**

**Theorem.** Pseud(α, β) iff ∀*i*, *j* ∈ *S* : (*i*α = *j*α ≠ 0 ⇒ *i*β = *j*β).

**Proof.** *Direct implication.* Let β = Ψα where Ψ is a construct pseudomorphism and *i*α = *j*α ≠ 0. Then

*i*β = *i*Ψα; *i*α ≠ 0 ⇒ *i*β = *i*Ψ[*i*]α = Ψ*i*α; *i*α = *j*α ≠ 0 ⇒ *i*β = Ψ*i*α = Ψ*j*α = *j*β.

*Reverse implication.* Let ∀*i*, *j* ∈ *S* : (*i*α = *j*α ≠ 0 ⇒ *i*β = *j*β). Then ∀*i* ∈ *S* : (*i*β = *fi*α ⇐ *i*α ≠ 0) where *f* is some function defined on parts(α). From this β = *f*α. We will prove that *f* is a pseudomorphism that is *fi* = *if*[*i*]. It is enough to prove *fi*γ = *if*[*i*]γ for γ = *j*α ≠ 0 where *j* ∈ *S*. We have *fi*γ = *fij*α = *ij*β[*ij*α] = *ifj*α[*ij*α] = *if*γ[*i*γ] = *if*[*i*]γ. **End of proof.**

**Definitio****n.** Let Pseud(α, β) where α ∈ *E*_{1}, β ∈ *E*_{2}. β/α (*factor* of β by α) is the operator which is a construct pseudomorphism from Sys_{1}|_{parts(α)} to Sys_{2}|_{parts(β)} such that (β/α)α = β. (Below we will prove that there exist only one factor β/α.)

**Proposition.** If Pseud(α, β) then ∀*i* ∈ *S* : (*i*α ≠ 0 ⇒ (β/α)*i*α = *i*β).

**Proof.** If *i*α ≠ 0 then (β/α)*i*α = *i*(β/α)[*i*]α = *i*(β/α)α = *i*β. **End of proof.**

**Obvious consequence.** If Pseud(α, β) then β/α = {(*i*α, *i*β) | *i* ∈ *S*, *i*α ≠ 0}.

**Remark.** The above statement allows to extend the definition of β/α to the case when ¬Pseud(α, β) but in this case β/α would be a relation rather than a function.

**Consequence.** If Pseud(α, β) then exist exactly one β/α.

**Proof.** We need to prove that if both *f* and *g* are factors of β by α then ∀*i* ∈ *S* : *fi*α = *gi*α. We have *i*α ≠ 0 ⇒ *fi*α = *i*β = *gi*α. So *fi*α = *gi*α. **End of proof.**

**Theorem.**

- Let Pseud(α, β) where α ∈
*E*_{1}, β ∈*E*_{2}. If Ψ is a construct pseudomorphism from Sys_{2}to Sys_{3}then Pseud(α, Ψβ) and Ψ(β/α) = (Ψβ)/α. - If α, β ∈
*E*_{1}and Pseud(α, β) and Ψ is a construct monomorphism from Sys_{1}to Sys_{2}then Pseud(Ψα, Ψβ).

**Proof.** 1. We have (β/α)α = β; Ψβ = Ψ(β/α)α. From the previous formula, taking in account that Ψ(β/α) is a pseudomorphism (as a composition of pseudomorphisms). Ψ(β/α) is a pseudomorphism defined on parts(α) such that ((Ψβ)/α)α = Ψβ; from this by definition of factor we have (Ψβ)/α = Ψ(β/α).

2. We have ∀*i*, *j* ∈ *S* : (*i*α = *j*α ≠ 0 ⇒ *i*β = *j*β) and need to prove

∀*i*, *j* ∈ *S* : (*i*Ψα = *j*Ψα ≠ 0 ⇒ *i*Ψβ = *j*Ψβ)

what is equivalent to ∀*i*, *j* ∈ *S* : (Ψ*i*α = Ψ*j*α ≠ 0 ⇒ Ψ*i*β = Ψ*j*β).

Taking in account that Ψ is a injection, Ψ*i*α = Ψ*j*α ≠ 0 ⇒ *i*α = *j*α ≠ 0 ⇒ *i*β = *j*β ⇒ Ψ*i*β = Ψ*j*β. **End of proof.**

## Reconstructions and Systems of Formulas

### Reconstructions

A *re**base* is a pair of two bases Base_{1} and Base_{2} and a relation → (called “*can be replaced with*”) between *E*_{1} and *E*_{2}.

A *reconstruction* is a rebase between construct.

**Remark.** → can denote such things as allowed variable substitutions. *[TODO: More about this.]*

*Re**base** homomorphism* from a rebase (Base_{1}, Base_{2}, →) to a rebase (Base_{1}‘, Base_{2}‘, →’) is a pair (Ψ_{1}, Ψ_{2}) of construct homomorphisms Ψ_{1} from Base_{1} to Base_{1}‘ and Ψ_{2} from Base_{2} to Base_{2}‘ such that

∀α, β ∈ *E*_{1} : (α → β ⇒ Ψ_{1}α →’ Ψ_{2}β).

*Reconstruction homomorphism* is a rebase homomorphisms between reconstructions such that (Ψ_{1}, Ψ_{2}) are construct homomorphisms.

*R**ebase and r**econstruction monomorphism**s* are such rebase and reconstruction homomorphism that both Ψ_{1} and Ψ_{2} are injective.

These monomorphisms have the *reverse* defined as (Ψ_{1}, Ψ_{2})^{ -1} = (Ψ_{1}^{-1}, Ψ_{2}^{-1}).

*Re**base and re**construction epimorphism**s* are such rebase and reconstruction homomorphism that Ψ_{1}, Ψ_{2} are homomorphisms and

∀α, β ∈ *E*_{1} : (α → β ⇔ Ψ_{1}α →’ Ψ_{2}β).

*Reconstruction isomorphism* is reconstruction homomorphism which is both reconstruction monomorphism and reconstruction epimorphism.

**Proposition.** The reverse of a rebase/reconstruction isomorphism is a rebase/reconstruction isomorphism.

**Proof.** Ψ_{1} and Ψ_{2} are construct isomorphisms; consequently Ψ_{1}^{-1} and Ψ_{2}^{-1} are also construct isomorphisms. We have left to prove that ∀α, β ∈ *E*_{2} : (α →’ β ⇒ Ψ^{ -1}α → Ψ^{ -1}β) what directly follows from the definition of reconstruction epimorphism. **End of proof.**

**Definition.** Two reconstructions are *isomorphic* iff there exist a reconstruction isomorphism between them.

### Systems of Formulas

A *system of formulas* is a pair of a system of constructs (*E*, *X*, 0) and a set *Y* ⊆ *E*. Elements of *Y* are called *symbols* (or *constant symbols*).

**Remark.** Often ∀ω ∈ *Y*, *i* ∈ *X* : *i*ω = 0 (that is symbols are *terminals* of the formula). But this is not required by our axiomatic; for example, it can be instead *i*ω = ω. Then the graph of subformulas would have loops in the place of symbols.

*[TODO: Research also systems of formulas with variable symbols and variable substitution.]*

**Remark.** Our method is more flexible and powerful than traditional variable substitution as (provided that we have enough indices) we can in principle specialize any formula (not only formulas with variables).

To every system of formulas (*E*, *X*, 0, *Y*) corresponds a reconstruction with Sys_{1} = Sys_{2} = (*E*, *X*, 0) and “can be replaced with” relation defined as α → β ⇔ α = β ∨ (α ∉ *Y* ∧ β ≠ 0).

**Obvious.** For systems of formulas the following statements are equivalent:

- α → β;
- α = β ∨ (α ∉
*Y*∧ β ≠ 0); - (α ∈
*Y*∨ β = 0) ⇒ α = β; - α ≠ β ⇒ (α ∉
*Y*∧ β ≠ 0).

**Remark.** It seems that it is God who has chosen the letters (*X*, 0, *Y*) above straight from the end of the alphabet (I have chosen the letters from the words “inde* x*”, “

*ero”, “s*

**z***mbol”, not the last alphabet letters.) But why then 0 and*

**y***Y*are reversed in the order? Isn’t it a hint that we should first define formulas without 0 straight from the bases and only then add the concept of nulls? Anyway He made

*Y*and

*Z*symmetric (after I replaced a single 0 with more general case of arbitrary set of nulls

*Z*). “It is already not I who writes this, but Christ writes through me.” (a

*modified*quote from Bible).

**Theorem.** “Can be replaced with” relation for a system of formulas is reflexive and transitive.

**Proof.** *Reflexivity.* Obvious.

*Transitivity.* If α → γ then α → α ∧ α → γ.

Let α → β ∧ β → γ. If α ∉ *Y* and γ ≠ 0, then α → γ is obvious. If α ∈ *Y*, then α → β ⇔ α = β and so α → β ∧ β → γ ⇒ α = β ∧ β → γ ⇒ α → γ. If γ = 0, then β = γ; α → γ. **End of proof.**

*[TODO: It seems that studying formulas (an probably even reconstructions) can be reduced to studying constructs (This seems useful in practice because constructs are simpler than formulas.) by “encoding” symbols as different topological structures of constructs. Probably it may be further reduced to studying bases. This is similar to that symbols (e.g. letters) in typography are encoded by different shapes.]*

### Specialization Functions

**Definition.** A *specialization function* Ψ on a reconstruction (Sys_{1}, Sys_{2}, →) is a pseudomorphism Ψ from Sys_{1} to Sys_{2} such that Ψ ⊆ (→) that is ∀α ∈ *E*_{1} : α → Ψα.

**Definition.** A *specialization function* on a system of formulas is a specialization function on the corresponding reconstruction.

**Proposition.** Ψ is a specialization function on a system Sys of formulas iff all of the following is true:

- Ψ is a pseudomorphism;
- ∀α ∈
*E*: (α ∈*Y*∨ Ψα = 0 ⇒ α = Ψα).

**Proof.** α → β ⇔ α = Ψα ∨ (α ∉ *Y* ∧ Ψα ≠ 0) ⇔ (α = Ψα ∨ α ∉ *Y*) ∧ (α = Ψα ∨ Ψα ≠ 0) ⇔

α ∈ *Y* ∨ Ψα = 0 ⇒ α = Ψα for any α, β ∈ *E*. **End of proof.**

**Proposition.** If *f* and *g* are specialization functions on reconstructions (Sys_{1}, Sys_{2}, →_{1}) and (Sys_{2}, Sys_{3}, →_{2}) correspondingly, then *gf* is a specialization function on (Sys_{1}, Sys_{3}, (→_{2})◦(→_{1})).

**Proof.** That *gf* is a pseudomorphism is proved above. We have left to prove that *gf* ⊆ (→_{2})◦(→_{1}). It follows from that *f* ⊆ (→_{1}), *g* ⊆ (→_{2}). **End of proof.**

**Obvious consequence.** Composition of specialization functions on a system of formulas is a specialization function on this system of formulas.

### Specialization

By definition (for α ∈ *E*_{1}, β ∈ *E*_{2}) α ≤ β ⇔ ∀*i* ∈ *S* : (*i*α ≠ 0 ⇒ *i*α → *i*β). *[TODO: Change the notation, it is not *a* partial order.]*

**Proposition.** On a system of formulas ≤ is reflexive and transitive.

**Proof.** Directly follows from reflexivity and transitivity of → on systems of formulas. **End of proof.**

*Specialization* α(…) (regarding the reconstruction (Sys_{1}, Sys_{2}, →)) of the formula α is the set

α(…) = {β ∈ E_{2} | α ≤ β ∧ Pseud(α, β)}.

**Remark.** α(…) ⊆ *E*_{2}.

**Obvious.** α ∈ α(…) for a system of formulas.

The following theorem shows that similarly named concepts of *specialization* and *specialization function* are really related:

**Theorem.** Let α ∈ *E*_{1}, β ∈ *E*_{2}. Then (1) ⇒ (2) ⇒ (3):

- β ∈ α(…).
- Exists a specialization function Ψ on (Sys
_{1}|_{parts(α)}, Sys_{2}|_{parts(β)}, →|_{parts(α) × parts(β)}) such that Ψα = β. - Pseud(α, β) and β/α is a specialization function on (Sys
_{1}|_{parts(α)}, Sys_{2}|_{parts(β)}, →|_{parts(α) × parts(β)}).

If also ∀β ∈ *E*_{2} : 0 → β, then the above statements are equivalent.

**Proof.** **(2) ⇒ (3).** Pseud(α, β) because a specialization function is a pseudomorphism. Ψ = β/α because β/α is the only pseudomorphism from Sys_{1}|_{parts(α)} to Sys_{2}|_{parts(β)} whose value on α is equal to β.

**(1) ⇒ (2).** We have α ≤ β ∧ Pseud(α, β). That is

∀*i* ∈ *S* : (*i*α ≠ 0 ⇒ *i*α → *i*β) and ∀*i*, *j* ∈ *S* : (*i*α = *j*α ≠ 0 ⇒ *i*β = *j*β).

So exists an operator Ψ defined on parts(α) such that ∀*i* ∈ *S* : (*i*α ≠ 0 ⇒ Ψ*i*α = *i*β).

We have ∀*i*, *j* ∈ *S* : (*ji*α ≠ 0 ⇒ Ψ*ji*α = *j*Ψ*i*α).

That is ∀γ ∈ dom Ψ, *j* ∈ *S* : (*j*γ ≠ 0 ⇒ Ψ*j*γ = *j*Ψγ), what is the same as

∀γ ∈ dom Ψ, *j* ∈ *S* : Ψ*j*γ = *j*Ψ[*j*]γ.

So Ψ is a pseudomorphism from Sys_{1}|_{parts(α)} to Sys_{2}|_{parts(β)}.

From the above ∀*i* ∈ *S* : (*i*α ≠ 0 ⇒ *i*α → Ψ*i*α). Consequently ∀γ ∈ parts(α) : γ → Ψγ, that is Ψ is a specialization function.

**(3) ⇒ (1).** (Provided ∀β ∈ *E*_{2} : 0 → β) Let ∀*i*, *j* ∈ *S* : (*i*α = *j*α ≠ 0 ⇒ *i*β = *j*β) and β/α is a specialization function on (Sys_{1}|_{parts(α)}, Sys_{2}|_{parts(β)}, →|_{parts(α) × parts(β)}). Because β/α is a specialization function, ∀γ ∈ parts(α) : γ → (β/α)γ.

We have ∀*i* ∈ *S* : *i*α → (β/α)*i*α. But *i*α ≠ 0 ⇒ (β/α)*i*α = *i*β. So ∀*i* ∈ *S* : (*i*α ≠ 0 ⇒ *i*α → *i*β), ∀*i* ∈ *S* : *i*α → *i*β, that is α ≤ β. Finally β ∈ α(…) because Pseud(α, β). **End of proof.**

By definition <*f*>*x* = *fx* ⇐ *x* ∈ dom *f*; <*f*>*x* = *x* ⇐ *x* ∉ dom *f*.

**Consequence.** Let Sys is a system of formulas, α, β ∈ *E*. Then β ∈ α(…) (regarding Sys) iff <β/α>|_{E} is a specialization function on Sys. *[TODO: Check once more that the proof is correct in all cases.]*

**Proof.** We need to prove that Ψ = <β/α>|_{E} is a specialization function on Sys iff β/α is a specialization function on (Sys_{1}|_{parts(α)}, Sys_{2}|_{parts(β)}, →|_{parts(α) × parts(β)}).

The direct implication of the above is obvious.

Let β/α is a specialization function on (Sys_{1}|_{parts(α)}, Sys_{2}|_{parts(β)}, →|_{parts(α) × parts(β)}). We need to prove that Ψ is a pseudomorphism and that

∀γ ∈ *E* : (γ ∈ *Y* ∨ Ψγ = 0 ⇒ γ = Ψγ).

On γ ∈ parts(α) this follows from that β/α is a specialization function on (Sys_{1}|_{parts(α)}, Sys_{2}|_{parts(β)}, →|_{parts(α) × parts(β)}).

On γ ∉ parts(α) this follows from γ = Ψγ.

To prove that Ψ is a pseudomorphism it is enough to prove that Ψ*i*γ = *i*Ψ[*i*]γ for *i*γ ∉ parts(α) because for *i*γ ∈ parts(α) we have Ψ*i*γ = (α/β)*i*γ = *i*(α/β)[*i*]γ = *i*Ψ[*i*]γ. Let iγ ∉ parts(α). We have *Ψ**iγ* = *i*γ.

If *i*γ = 0, then Ψ*i*γ = *i*γ *= 0* and *i*Ψ[*i*]γ = *i*γ. If *i*γ ≠ 0, then *i*Ψ[*i*]γ = *i*Ψγ = *i*γ because γ ∉ parts(α). So *i*Ψ[*i*]γ = *i*γ = Ψ*i*γ. **End of proof.**

**Proposition.** Let Sys is a system of formulas, α, β, γ ∈ *E*. Then β ∈ α(…) ∧ γ ∈ β(…) ⇒ γ ∈ α(…).

**Proof.** It follows from distributivity of both Pseud and → (on systems of formulas). **End of proof.**

**Remark.** The above proposition can be easily generalized for the case of arbitrary reconstructions.

**Proposition.** If Ψ = (Ψ_{1}, Ψ_{2}) is a reconstruction homomorphism from (Sys_{1}, Sys_{2}, →) to (Sys_{1}‘, Sys_{2}‘, →’), then α ≤ β ⇒ Ψ_{1}α ≤ Ψ_{2}β for α ∈ *E*_{1}, β ∈ *E*_{2}.

**Proof.** Let α ≤ β that is ∀*i* ∈ *S* : (*i*α ≠ 0_{1} ⇒ *i*α → *i*β). Let also Ψ*i*α ≠ 0′. We need to prove Ψ_{1}*i*α →’ Ψ_{2}*i*β. We have *i*α ≠ 0. So *i*α → *i*β; Ψ_{1}*i*α →’ Ψ_{2}*i*β. **End of proof.**

**Proposition.** Let Sys_{1}, Sys_{2}, Sys_{1}‘, Sys_{2}‘ be systems of constructs, Ψ_{1} is construct isomorphism from Sys_{1} to Sys_{1}‘ and Ψ_{2} is construct homomorphism from Sys_{2} to Sys_{2}‘. Then Pseud(α, β) ⇒ Pseud(Ψ_{1}α, Ψ_{2}β).

**Proof.** We have ∀*i*, *j* ∈ *S* : (*i*α = *j*α ≠ 0 ⇒ *i*β = *j*β). Let *i*Ψ_{1}α = *j*Ψ_{1}α ≠ 0 or equivalently Ψ_{1}*i*α = Ψ_{1}*j*α ≠ 0. Then because Ψ_{1} is a bijection, *i*α = *j*α and moreover *i*α = *j*α ≠ 0. So *i*β = *j*β. From this Ψ_{2}*i*β = Ψ_{2}*j*β or equivalently *i*Ψ_{2}β = *j*Ψ_{2}β. **End of proof.**

**Theorem.** If Ψ = (Ψ_{1}, Ψ_{2}) is a reconstruction isomorphism from (Sys_{1}, Sys_{2}, →) to (Sys_{1}‘, Sys_{2}‘, →’), then β ∈ α(…) ⇔ Ψ_{2}β ∈ (Ψ_{1}α)(…) for α ∈ *E*_{1}, β ∈ *E*_{2}.

**Proof.** β ∈ α(…) ⇒ Ψ_{2}β ∈ (Ψ_{1}α)(…) directly follows from two previous statements. Because Ψ_{1}, Ψ_{2} are bijections, then also analogously Ψ_{2}β ∈ (Ψ_{1}α)(…) ⇒ β ∈ α(…). **End of proof.**

#### Least Common Specialization

Let (Sys_{1}, Sys’, →_{1}), (Sys_{2}, Sys’, →_{2}), (Sys_{3}, Sys’, →_{3}) be some reconstructions.

The *least common specialization* LCS(α, β) of constructs α ∈ Sys_{1} and β ∈ Sys_{2} is construct γ ∈ Sys_{3} such that α(…) ∩ β(…) = γ(…).

**Remark.** The above definition may probably somehow vary in a future version of this document.

**Remark.** LCS is similar to least common dividend (LCD) in arithmetic. *[TODO: Explain this similarity.]* BTW, we could attempt to associate some logical formulas with numbers and consider number theory in some logical form. Maybe it will lead to a new proof of Last Fermat Theorem, etc. We can also reversely study formulas with number theory like Godel was doing.

**Proposition.** Let Sys_{3} = Sys’ be a system of formulas and →_{3} is the “can replace with” relation on that system of formulas. If

∀γ, δ ∈ *E*‘ : (γ ∈ δ(…) ∧ δ ∈ γ(…) ⇒ γ = δ),

then exists no more than one LCS(α, β). *[TODO: Formulate this better.]*

**Proof.** Let γ and δ are both LCS(α, β). Then (because Sys’ is a system of formulas) γ ∈ γ(…) ⊆ α(…). So γ ∈ α(…); analogously γ ∈ β(…). From this γ ∈ α(…) ∩ β(…) = δ(…), that is γ ∈ δ(…); analogously δ ∈ γ(…). So γ = δ. **End of proof.**

**Definition.** Formulas α and β are *top-comatched* iff α(…) ∩ β(…) ≠ ∅.

**Unsolved problem.** Find the condition to warrant that if two constructs are top-comatched then they have LCS. *[Previously I have tried without success to solve it for the particular cases of lists of lists and binary trees. Now I expect it to be simpler in more abstract formulation, but I have not yet attempted to solve it.]*

*[TODO: Find an algorithm for calculating **LCS(α, β)** knowing **α** and **β** (in such cases as lists of lists). **A**pparently this algorithm exists only for the concrete representation.**]*

*[TODO: Also greatest common generalization.]*

# Part 2. Representation Related Properties of Formulas

## Preface

### Overview

This is the second part “Representation of Formulas” of the book that describes new axiomatic theory of mathematical formulas (including infinite formulas) as well as of anything what has indexed parts.

This part “Representation of Formulas” is about concrete representations of formulas such as:

- lists of lists,
*n*-ary trees,- binary trees,
- graphs,

etc. as well as about some more complex properties of formulas, including pattern substitutions in formulas.

## Infinite Trees

Let *X* (the set of *indexes* or *indices*) is a set.

By definition *S* is the set of all finite sequences (zero or more elements) of elements of *X*.

Given some sets *Q* and *X*, the set of *infinite trees* is the set *Q*^{S} of all functions from *S* to *Q*.

By definition *i*α = {(*p*, α(pi)) | *p* ∈ *S*} for α ∈ *Q*^{S}.

Tree(*Q*, *X*) = (*Q*^{S}, *X*) is a basis, called the *system of infinite trees*.

If element 0 ∈ *Q* then Tree(*Q*, *X*, 0) by definition is the system of constructs (Q^{S}, *X*, {(*i*, 0) | *i* ∈ *S*}).

### Constantness of a Construct

**Definition.** Given a reconstruction (Sys_{1}, Sys_{2}, →) *constantness* Ωα of a construct α ∈ *E*_{1} is

Ωα = {β ∈ *E*_{2} | ¬(α → β)}.

That is constantness of a construct is the set of these constructs by which it cannot be replaced.

**Proposition.** For systems of formulas:

- α ∈
*Y*⇒ Ωα =*E*\ {α}; - α ∉
*Y*⇒ Ωα = ∅.

**Proof.** Obvious.

To every construct α corresponds the *tree of constantness*: Form α = {(*i*, Ω*i*α) | *i* ∈ *S*}.

**Proposition.** Form is a construct homomorphism.

**Proof.** *j*Form α = {(*p*, Ω*pj*α) | *p* ∈ *S*} = Form *j*α for *j* ∈ *S*. **End of proof.**

**Proposition.** Form α = Form β ⇔ ∀*i* ∈ *S* : Ω*i*α = Ω*i*β ⇔ ∀*i* ∈ *S*, γ ∈ E_{2} : (*i*α → γ ⇔ *i*β → γ).

**Proof.** Obvious.

**Theorem.** For systems of formulas the following statements are equivalent:

- Form α = Form β;
- ∀
*i*∈*S*: (*i*α ∈*Y*∨*i*β ∈*Y*⇒*i*α =*i*β); - ∀
*i*∈*S*: (*i*α ≠*i*β ⇒*i*α,*i*β ∉*Y*); - α ≤ β ∧ β ≤ α.

**Proof.** (1) ⇔ (2) ⇔ (3) is obvious.

α ≤ β ⇔ ∀*i* ∈ *S* : (*i*α ∈ *Y* ⇒ *i*β = *i*α).

So α ≤ β ∧ β ≤ α ⇔ ∀*i* ∈ *S* : (*i*α ∈ *Y* ∨ *i*β ∈ *Y* ⇒ *i*β = *i*α). **End of proof.**

### Shadow of **a** Construct. Equivalence of Constructs

*Shadow* of a construct α is by definition Shadow α = {(*i*, *i*α ≠ 0) | *i* ∈ *S*}.

**Proposition.** Shadow is a construct homomorphism from the system of constructs to the system of infinite trees Tree({0, 1}, *X*, 0).^{2}

**Proof.** *[TODO]*

**Definition.** Constructs α and β are equivalent ⇔ α ~ β ⇔ Form α = Form β ∧ Shadow α = Shadow β.

**Theorem.** The following statements are equivalent:

- α ~ β regarding a system of formulas (
*E*,*X*, 0,*Y*); - Form α = Form β regarding the system of formulas (
*E*,*X*, 0,*Y*∪ {0}).

**Proof.** We will prove *[TODO: Explain why it is enough]* that

α ~ β ⇔ ∀*i* ∈ *S* : (*i*α = *i*β ∈ *Y* ∪ {0} ∨ *i*α, *i*β ∉ *Y* ∪ {0}).

We have α ~ β ⇔ Form α = Form β ∧ Shadow α = Shadow β ⇔

∀*i* ∈ *S* : ((*i*α, *i*β ∉ *Y* ∨ *i*α = *i*β ∈ *Y*) ∧ *i*α = 0 ⇔ *i*β = 0).

Equivalently transforming the propositional formula under the quantifier, we get

*i*α, *i*β ∉ *Y* ∨ *i*α = *i*β ∈ *Y*) ∧ *i*α = 0 ⇔ *i*β = 0 ⇔

(iα, iβ ∉ *Y* ∨ iα = iβ ∈ *Y*) ∧ (*i*α, *i*β ∉ {0} ∨ *i*α = *i*β ∈ {0}) ⇔

*i*α, *i*β ∉ *Y* ∪ {0} ∨ *i*α = *i*β ∈ {0} \ *Y* ∨ (*i*α = *i*β ∈ *Y* ∧ *i*α, *i*β ∉ {0}) ∨ *i*α = *i*β ∈ *Y* ∩ {0} ⇔

*i*α, *i*β ∉ *Y* ∪ {0} ∨ *i*α = *i*β ∈ {0} ∨ (*i*α = *i*β ∈ *Y* ∧ *i*α, *i*β ∉ {0}) ⇔

*i*α, *i*β ∉ *Y* ∪ {0} ∨ *i*α = *i*β ∈ *Y* ∪ {0}.

**End of proof.**

**Theorem.** For systems of formulas if α ∉ *Y* and ∀*i* ∈ *X* : α ≠ *i*α then then Form α can be restored from {(*i*, Form *i*α) | *i* ∈ *X*}.

**Proof.** α ∉ *Y* ⇒ Ωα = ∅. So Ωiα can be restored for any *i* ∈ *S*. **End of proof.**

## Applying Operators to Parts of Formulas

### Applying an Operator to a Subformula

I will denote *i* ≤ *j* iff the sequence *i* is a start part of the sequence *j* for *i*, *j* ∈ *S*. (Note that *i* = *j* ⇒ *i* ≤ *j*.)

Let α ∈ *E*, *i* ∈ *X*, *f* is an operator on the set of formulas (or more generally constructs).

If *i* ∈ *X* then by definition applying *f* to the *i*-th (*i* ∈ *S*) *component* (or *i*-th *part*) of α is

(*f*@*i*)α = {(*k*, Ω*k*α) | *k* ∈ *S*, ¬(*i* ≤ *k*)} ∪ {(*ji*, Ω*jfi*α) | *j* ∈ *S*}.

**Remark.** (*f*@*i*)α may be a tree of constantness of some formula β. Then (*f*@*i*)α ~ β.

**Proposition.**

- ((
*f*@*i*)α)*k*= Ω*k*α ⇐ ¬(*i*≤*k*); - ((
*f*@*i*)α)(*ji*) = Ω*jfi*α.

**Proof.** Obvious.

**Proposition.** *f*@(*ji*) = (*f*@*j*) @ *i*.

**Proof.** *[TODO]*

*[TODO: **@** and **R**, **@** and **≥** are somehow related. It seems that **R** corresponds to the customary notion of repeated applying an operator.]*

### [TODO] Better Variant

Attaching a set *A* to a basis (*E*, *X*) by a function *f*: *A* → *E* is by definition the basis (*E* ∪ *A*, *X*) with indices extended onto the set *A* by the formula *i*α = *if*α for α ∈ *A*, *i* ∈ *X*.

iα = *i*<*f*>α

(*E*, *X*) ∪ *f*^{ -1}A

### Recursive Applying an Operator

Now let’s define *recursive applying an operator to parts of an object*.

Let (*E*, *X*) is a basis.

#### Recursive Applying an Operator with Closed Image

*[TODO: Illustrations for this section.]*

##### On a Basis

First consider the particular case of an operator *f*: *A* → *B* where sets *A*, *B* ⊆ *E* such that:

*A*∩*B*= ∅ ;*B*is closed.

Let *f*_{D} = *f* ∪ (=)|_{B}. (*f*_{D} is an operator (*A* ∪ *B*) → *B*.)

**Definition.** *Recursive applying operator* *f* is the operator Rec(*f*) = *R*(*f*_{D}). *[TODO: What if we would replace **R**by**L** in this formula? (**L** seems less perspective than **R** however.)]*

**Remark.** See below about the reason of usage of the word *recursive*.

Let α ∈ *E*.

**Lemma.** ∀*i* ∈ *X* : *i*Rec(*f*)α = Rec(*f*)*if*_{D}α.

**Proof.** *i*Rec(*f*)α = *iR*(f_{D})α = *R*(*f*_{D})*if*_{D}α = Rec(*f*)*if*_{D}α. **End of proof.**

**Lemma.** For *i* ∈ *X*

*i*Rec(*f*)α = Rec(*f*)*i*α ⇐ α ∈*B*;*i*Rec(*f*)α = Rec(*f*)*if*α ⇐ α ∈*A*.

**Proof.** Obvious consequence of the previous lemma. **End of proof.**

**Theorem.** For *i* ∈ *S*

*i*Rec(*f*)α = Rec(*f*)*i*α ⇐ α ∈*B*;*i*Rec(*f*)α = Rec(*f*)*if*α ⇐ α ∈*A*∧*i*≠ ().

**Proof.** 1. From the lemma, taking in account that *B* is closed.

2. *p*_{n}…*p*_{1}Rec(*f*)α = *p*_{n}…*p*_{2}Rec(*f*)*p*_{1}*f*α = Rec(*f*)*p*_{n}…*p*_{2}*p*_{1}*fα*. (I used the previous item.) **End of proof.**

##### On **a** System of Formulas

Let we have a system Sys of formulas.

From the above

- Ω
*i*Rec(*f*)α = Ω*i*α ⇐ α ∈*B*; - Ω
*i*Rec(*f*)α = Ω*if*α ⇐ α ∈*A*∧*i*≠ ().

So

*i*Rec(*f*)α ~*i*α ⇐ α ∈*B*;*i*Rec(*f*)α ~*if*α ⇐ α ∈*A*∧*i*≠ ().

If we will consider equivalent formulas equal, that is will replace ~ by = in the above formulas, we will get exactly the traditional definition (with *i* ∈ *X*) of recursive applying a function to parts of a formula, except of that Rec(*f*)ω = ω (not *f*ω as it is defined traditionally) for ω ∈ *Y*.

So our operator Rec(*f*) is a generalization of the traditional concept of recursive applying a function to parts of a formula.

**Remark.** The issue about the value of Rec(*f*) (and also of *R*(*f*)) on symbols can be reasonably solved by never taking into consideration formulas consisting of single symbols, nor any operators which map a formula which isn’t a symbol into a formula which is a symbol. For example (in the case of a system of lists of lists) instead of the formula ω consisting of single symbol we would use the formula (ω) and instead of the substitution (see below) (ω → ψ) (where ω, ψ ∈ *Y*) we would use the formula ((ω) → (ψ)). We also could mean (ω) when we write ω. *[TODO: Explain this more clearly. Probably we should introduce special term “single symbol” (distinguished from symbol) to overcome this problem.]*

#### The General Case of Recursive Applying an Operator

Above we have defined Rec(*f*) in certain special case.

Now let (*E*, *X*) be a basis and *f* be a function from a subset of *E* to *E*. We will define Rec(*f*) in this general case.

Let *D* be an arbitrary bijection from *E* to any set *E** such that *E* ∩ *E** = ∅ (that is *E** is a duplicate of *E*).

Let *X** be a set related to *X* by a bijective relation *i* ↔ *i** for *i* ∈ *X*, *i** ∈ *X**. (I also assume *X* ∩ *X** = ∅ .) By definition *i**α = *i***D*α = *Di*α. So (*E* ∪ *E**, *X**) is a basis.

Let the sets *A* = dom *f*; *B* = (*E* \ A) ∪ *E**. Easy to show that these sets conform to the requirements for *A* and *B* from the previous subsection, that is that the set *B* is closed (regarding indices *X**).

So then Rec(*D **◦ **f*) defined accordingly the previous subsection is a reindexation of the basis (*E* ∪ *E**, *X**).

We will denote it simply Rec(*f*) instead of Rec(*D **◦ **f*). *[See “TODO” below.]*

Rec(*f*) defined this way is exactly the customary notation of recursively applying a function (except of that thing that *f* was replaced by *D **◦ **f*, what is not essential because *D* is a bijection, and except of the above mentioned issue with values of Rec(*f*) on symbols).

*[TODO: There is *a* little glitch in the definition of recursive applying an operator, because the special case (“with closed image”) and the general case (defined in this section) are not the same but differ to the extent of the bijection **D**. This mess should be somehow eliminated in *a* good way.]*

**Remark.** Traditional recursive applying function (that is operation Rec(*f*)) from my viewpoint looks being defined so unbeautifully that I’d recommend to not use operation Rec(*f*) anymore for any serious work (except of probably teaching math children) but instead use *R*(*f*) instead of Rec(*f*) exclusively.

**Remark.** Probably the above is a general method of solving many kinds of recursion related problems (by reducing Rec(*f*) to *R*(*f*)). I have not yet tried it with solving particular problems yet however.

**Conjecture.** If *f* is a pseudomorphism then:

- Rec(
*f*) is a pseudomorphism. - Rec(
*f*)|_{dom }_{f}=*D ◦ f*.

**Remark.** Additionally to the above conjecture we could define *pseudomorphic continuation* and show that Rec(*f*) is *D* combined with pseudomorphic continuation.

## Formulas with Variables

Now we will model traditional mathematical formulas in our system.

Let there are following sets none of which intersect others:

- {0} (
*null*or*nil*); *V*(set of*variables*or*variable symbols*);*Y*_{0},*Y*_{1},*Y*_{2}, …,*Y*_{n}, … be correspondingly nullary, unary, binary, …,*n*-ary operations.

We will define: *Y* = *Y*_{0} ∪ *Y*_{1} ∪ *Y*_{2} ∪ …; *X* = ℕ.

*E** is recursively defined as the union of:

*V*;- all lists of the form (ω
_{n}α_{0}… α_{n}_{-1}) where ω_{n}∈*Y*_{n}, α_{i}∈*E**.

*E* = *E** ∪ {0}.

Applying an index *i* to a list is defined as its *i*-th element, or 0 if there are no such element. Applying an index to an element of *V* ∪ *Y* ∪ {0} is always 0.

(*E*, *X*, 0, *Y*) is a system of formulas. (It can be called *the traditional system of finite formulas* or *the traditional system of finite expressions*.)

**Remark.** If we want to use the same symbol as operations of different arity, we can make *Y*_{i} = *Y** × {*i*} where *Y** is the set of symbols denoting operations.

**Theorem.** For the traditional system of finite formulas specialization is the same as *variable substitution* (as it is defined traditionally).

**Proof.** It can be proved by induction:

- Let α ∈
*V*, β ≠ 0. Then α ≠ 0 ∧ α ∉*Y*. So α can be replaced with β: α → β. - ∀
*i*∈*S*\ {()} :*i*α = 0 ∉*Y*. So ∀*i*∈*S*\ {()} :*i*α →*i*β. Assembling this we have ∀*i*∈*S*:*i*α →*i*β that is β ≥ α. - ∀
*i*,*j*∈*S*: (*i*α =*j*α ≠ 0 ⇒*i*β =*j*β) because*i*α ≠ 0 ⇒*i*= (). So Pseud(α, β). As a result β ∈ α(…). - Let α ∈
*Y*. Then α → β ⇔ α = β. - Let α = (ω
_{n}α_{0}… α_{n}_{-1}) where ω_{n}∈*Y*_{n}, α_{i}∈*E**. - α → β ⇔ α = β ∨ (α ∉
*Y*∧ β ≠ 0). - Traditional variable substitution is replacing all variables with some formulas, the same variables with the same formulas. Replacing the same variables with the same formulas is equivalent to replacing all subformulas with the same formulas. It is exactly the requirement β ≥ α that is ∀
*i*∈*S*:*i*α →*i*β.

## Substitutions

By definition *top-substitution* of α by β in γ is (α –top→ β) = {(γ, Rec(γ/α)β) | γ∈α(…)}.

In other words,

- dom(α –top→ β) = α(…);
- (α –top→ β)γ = Rec(γ/α)β for γ ∈ α(…).

*[TODO: Demonstrate that it corresponds to the traditional definition of top-substitution.]*

**Example.** ((*A*+*B*)→(*A*#*B*))(U^{2}+V^{3}) = U^{2}#V^{3} if *A* and *B* are variables. *[TODO: Explain details, especially define the concept of variables.]*

**Proposition.** If γ ∈ dom(α –top→ β) then (α –top→ β)γ ∈ β(…). *[TODO: Check.]*

**Proof.** If γ ∈ dom(α –top→ β) then γ ∈ α(…), γ/α is a specialization function, (α –top→ β)γ = (γ/α)β is a specialization of β. **End of proof.**

By definition (α→β)γ = {((α –top→ β) @ *i*)γ | *i* ∈ *S*, *i*γ ∈ α(…)}.

(α→β)γ is called *substitution* of α by β in γ.

Informally (α→β)γ is the set of all replacements of subformulas of γ which match pattern α with corresponding specialization of β.

**Remark.** Substitutions have many usages:

- asymmetric analog of equality (with left part which may be indefinite);
- inference rule;
- a sign that a subformula can be substituted with other formula;
- α→β means “β is α”.
- a step in an algorithm;
- declaration that the class α is derived from the class β (in the sense of object oriented programming).

See references below for a list of books where different usages of substitutions are considered.

**Definition.** *Substitution of all matching patterns* operator α –all→ β = Rec(α –top→ β).

**Definition.** *Full substitution* or *repeated substitution* operator α –full→ β = *R*(<α –top→ β>).

(I recall that by definition <*f*> = *fx* ⇐ *x* ∈ dom *f* and <*f*>*x* = *x* ⇐ *x* ∉ dom *f*.)

**Remark.** I deem full substitution a more perspective operation (at least for fundamental mathematics) than traditional substitution of all matching patterns.

## Different Representations of Formulas

We have already considered *lists of lists* and *infinite trees* above.

Now we will consider some other examples of systems of formulas.

### Symbol With Arguments Representation of Formulas

Let *Y* be a set. The system of *symbols with arguments* is a subsystem of the lists of lists where the first argument of every list is a symbol (that is an element of *Y*) and the rest arguments of every list are not symbols (but are lists).

Formulas in the form of symbols with arguments may be denoted as ω(α_{0} … α_{n}) instead of (ω α_{0} … α_{n}).

By definition *H*(ω(α_{0} … α_{n})) = ω for *n* ≥ 0. (*H* is called the *head* of the formula ω(α_{0} … α_{n})).

For ω ∈ *Y* we can define either *H*ω = ∅ or *H*ω = ω depending on the problem domain and on our tastes. After this we may replace the first element of the set *X* by ω and get a new (reindexed) system of formulas. *[TODO: Say this clearly.]*

We can add special symbol “formula” to denote a formula consisting of several symbols:

**Example.** 2+(3/4) may be represented as formula (2() +() formula (3() /() 4())) in the form of a symbol with arguments.

**Example.** Omitting the symbol “formula” in the above formula, we’d get (2() +() (3() /() 4())), removing also empty parentheses we get (2 + (3 / 4)).

**Remark.** This could be also represented simpler as +(2 /(3 4)) but this form is less flexible regarding possible specializations.

### Binary Tree Representation of Formulas

I call *(infinite) binary trees* infinite trees with the set *X* = {0, 1}.^{3}

**Theorem.** If Sys = (*E*, *X*, 0, *Y*) is a system of formulas and the set card *X* ≤ card ℕ then Sys is isomorphic to a subsystem of the system of binary trees. *[TODO: Formulate exactly and prove this theorem.]*

### Graph Representation of Formulas

*[TODO: This section should be illustrated.]*

#### Directed Multigraph with Indexed Edges

Let *X* be a set.

I will call a *directed multigraph with indexed edges* (*DMGWIE*) a pair of sets (called the *set of vertices* and the *set of edges*) such that the set of edges contains triples (*a*, *b*, *n*) (called *arrows* from *a* to *b*) where *a* and *b* are vertices and *n* ∈ *X*.

I will call *top vertex* (*bottom vertex*) of a DMGWIE a vertex to (from) which there are no arrows.

I will call a *DMGWIE homomorphism* a function *f* on the set of vertices extended to the set of edges so that *f*(*a*, *b*, *n*) = (*f*(*a*), *f*(*b*), *n*).

An injective homomorphism is called *monomorphism*, homomorphism whose image is the union of the entire set of vertices and the set of edges is called *epimorphism*. A homomorphism which is both monomorphism and epimorphism is called *isomorphism*.

Let *G* be a DMGWIE, *a* ∈ vertices(*G*), *n* ∈ *X*. I will denote *n*_{G}*a* such *b* ∈ vertices(*G*) that (a, *b*, *n*) ∈ edges(*G*).

Let *G* be a DMGWIE and *v* ∈ vertices(*G*). I will denote *Q*(*G*, *v*) the DMGWIE consisting of all vertices which can be reached from *v* moving in the direction of the arrows (including *v* itself) and all arrows between these vertices.

#### A System of Constructs as a DMGWIE

*[TODO: About graph representation of bases and bases corresponding to graphs.]*

*[TODO: Show that the above relations of systems of constructs with DMGWIE are the reverse of each other.]*

*[TODO: Show how construct morphisms and DMGWIE morphisms correspond to each other.]*

*[TODO: Two different definitions of depth of *a* construct.]*

### Human Representation of Formulas

*[TODO: This section is severely incomplete. You can skip its reading for now.]*

The following representation of formulas is practically identical to the conventional human mathematical notation. So I call it the human representation of formulas:

A formula is a pair of the main part and the list of modifiers:

- the main part is either a symbol or a list of formulas;
- the list of modifiers is a list of formulas.

The modifiers can be conveniently denoted as lower indices in formulas.

**Remark.** Modifiers are similar to indexes in the traditional math notation. (I use the word “modifier” instead of “index” to not mess with numeric indexes of elements of lists.) For example, two different kinds of additions (e.*g*. in two abelian groups or calculated by two different algorithms) may be denoted as +_{1} and +_{2}. It can be formalized in our system as the constant symbol “+” with a modifier: 2+_{1}2 and 2+_{2}2.

Formally human form can be represented e.*g*. as lists of formulas with special element | intended to separate the modifiers from the main part: ((2|) (+|) (2|) |).

Informally, in the human form a specialization is adding additional modifiers to a formula.

**Example.**

- (
*a*+*b*)_{1}∈ (*a*+*b*)(…)*or*((*a*|) (+|) (*b*|) | 1) ∈ ((*a*|) (+|) (*b*|) |)(…); - (
*a*+_{1}*b*) ∈ (*a*+*b*)(…)*or*((*a*|) (+|1) (*b*|) |) ∈ ((*a*|) (+|) (*b*|) |)(…).

**Example.** We could denote real number variables as the constant symbol “real” with indexes (specializations of “real”). Then the school algebra equation *a*+*b* = *b*+*a* could be formalized as real_{a}+real_{b} = real_{b}+real_{a}.

1Plural form of the word *basis* is *bases*.

2In this formula the first “0” means boolean false, and the second “0” means null construct from the set *E*.

3They are called *binary* (from Latin *binarius* meaning “double”) trees because the set {0, 1} is two-element.