Victor Porton

Finite and infinite formulas are considered axiomatically.

Part 1. Axiomatic Theory of Formulas



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.


Definition of a Basis

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

A basis1 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 E1 to E2 an operator from a basis Base1 to a basis Base2. An operator from a basis to itself will be called an operator on this basis.

I will denote bases as Base, Base1, Base2, …

Obvious. Indices are operators on the basis.

By definition S (I call it the set of sequences) is the set of all finite sequences pnp0 of zero or more indices piX. To a sequence of indices corresponds an operator on E: (pnp0)α = pn(pn – 1…(p0α)…).

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 X1 = X2 = … = X.

The case of two bases (E1, X1) and (E2, X2) such that X1X2 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 E1 and E2 some f can be operator on both E1 and E2 (for example if f is a function E1E2E1E2).

For simplicity I will implicitly assume below that E1E2 = ∅. (If E1E2 ≠ ∅ we can replace E1 with E1 × {1} and E2 with E2 × {2}.)

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

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

Proposition. iReind(λ) = Reind(λ)(λi) for iX.

Proof. Let α is a construct of the system of constructs (E2, λX). Then Reind(λ)α is a construct from (E2, X). So iReind(λ)α = Reind(λ)(λi)α. End of proof.

Remark. The above proposition may be not true for iS!

When we have two bases (E1, X1), (E2, X2) and a pair (Ψ, λ) of an operator Ψ from E1 to E2 and a reindexation function λ from X1 to X2, we can first apply reindexing to get the basis (E2, X1) and then consider Ψ as an operator from (E1, X1) to (E2, X1). (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 iX.

Proof. By properties of reindexation. End of proof.

Proposition. For p1, …, pnX

  • pnp1R(f) = R(f)pnfp1f;
  • pnp1L(f) = R(f)fpnfp1.

Proof. By properties of reindexation:

  • pnp1R(f) = pnp2R(f)p1f = pnp3R(f)p2fp1f = … = R(f)pnfp1f.
  • pnp1L(f) = pnp2L(f)fp1 = pnp3L(f)fp2fp1 = … = L(f)fpnfp1. 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 (E1, X) to a basis (E2, X) is a function Ψ: E1E2 such that ∀iX : Ψi = iΨ.

Proposition. Ψ is a homomorphism iff ∀iS : Ψi = iΨ.

Proof. Reverse implication. Obvious.

Direct implication. Ψpnp0 = pnΨpn-1p1 = … = pnp1Ψp0 = pnp0Ψ. End of proof.

By definition a basis monomorphism is an injective basis homomorphism.

By definition a basis epimorphism is a basis homomorphism such that im Ψ = E2.

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α | iX}.

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

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

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

  1. A is subconstruct closed.
  2. ∀α ∈ A, iX : iα ∈ A.
  3. ∀α ∈ A, iS : iα ∈ A.

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

Let the set HE 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 ∀iX : i0 = 0.

Remark. We could generalize to consider instead a subset ZE (elements of Z are called null or nil constructs) such that ∀iX, 0 ∈ Z : i0 = 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 i0 = 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 iE by the formula i0 = 0.)

I will denote systems of constructs as Sys, Sys1, Sys2, … and the corresponding sets of constructs as E, E1, E2, …, corresponding sets of indices as X, X1, X2, … 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 ∈ HE 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 (E1, X, 0) to a system of constructs (E2, X, 0) a function from E1 to E2 such that f0 = 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 p0 = 0 and so [p]0 = p0 = 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α = 0q[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. [p0]p1pn = p1pn[p0p1pn] for any operators p0, …, pn.

Theorem. [pmp0][pnp0] = [pmax(n,m)p0].

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 Sys1 = (E1, X1, 01) and Sys2 = (E2, X2, 02) be two systems of constructs. Let λ be a reindexation function from the basis (E1, X1) to the basis (E2, X2). Let the basis (E2, X1) be the reindexed (with λ) basis (E2, X2).

Then λ is called reindexation function from the system of constructs Sys1 to the system of constructs Sys2. The system of constructs (E2, X1, 02) = λ-1(E2, X2, 02) is called reindexed (with λ) system of constructs (E2, X2, 02).

To show that (E2, X1, 02) is really a system of constructs we need to prove that i02 = 01 for iX1. We have i02 = (λi)01 = 01.

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: (E1, X, 0) and (E2, 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 01 = 02 = … = 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 E1 is E2 and of 01 is 02. Construct isomorphism is construct homomorphism which is both construct homomorphism and construct epimorphism.

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


Definition. Construct pseudomorphism from Sys1 to Sys2 is such operator from E1 to E2 that ∀iX : Ψi = iΨ[i].

Proposition. An operator Ψ from E1 to E2 is a construct pseudomorphism iff ∀iS : Ψi = iΨ[i].

Proof. Reverse implication. Obvious.

Direct implication. By induction by n for piX:

Ψpnp0 = pnp1Ψ[pnp1]p0 = pnp1Ψp0[pnp0] = pnp0Ψ[p0][pnp0] = pnp0Ψ[pnp0]. 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Ψ1iα = Ψ2iΨ1[i]α = iΨ2[i1[i]α.

Ψ1[i]α ≠ 0 ⇒ Ψ2Ψ1iα = iΨ2Ψ1[i]α; Ψ1[i]α = 0 ⇒ Ψ2Ψ1iα = Ψ1[i]α = iΨ2Ψ1[i]α.

So Ψ2Ψ1iα = iΨ2Ψ1[i]α. End of proof.

Pseudomorphic Image

Definition. Let α ∈ E1, β ∈ E2, Then Pseud(α, β) ⇔ β is a pseudomorphic image of α ⇔ there exists a pseudomorphism Ψ from Sys1 to Sys2 such that β = Ψα.

Proposition. Pseud(α, β) ∧ Pseud(β, γ) ⇒ Pseud(α, γ) for α ∈ E1, β ∈ E2, γ ∈ E3.

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

Theorem. Pseud(α, β) iff ∀i, jS : (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, jS : (iα = jα ≠ 0 ⇒ iβ = jβ). Then ∀iS : (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 jS. We have fiγ = fijα = ijβ[ijα] = ifjα[ijα] = ifγ[iγ] = if[i]γ. End of proof.

Definition. Let Pseud(α, β) where α ∈ E1, β ∈ E2. β/α (factor of β by α) is the operator which is a construct pseudomorphism from Sys1|parts(α) to Sys2|parts(β) such that (β/α)α = β. (Below we will prove that there exist only one factor β/α.)

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

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

Obvious consequence. If Pseud(α, β) then β/α = {(iα, iβ) | iS, 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 ∀iS : fiα = giα. We have iα ≠ 0 ⇒ fiα = iβ = giα. So fiα = giα. End of proof.


  1. Let Pseud(α, β) where α ∈ E1, β ∈ E2. If Ψ is a construct pseudomorphism from Sys2 to Sys3 then Pseud(α, Ψβ) and Ψ(β/α) = (Ψβ)/α.
  2. If α, β ∈ E1 and Pseud(α, β) and Ψ is a construct monomorphism from Sys1 to Sys2 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, jS : (iα = jα ≠ 0 ⇒ iβ = jβ) and need to prove

i, jS : (iΨα = jΨα ≠ 0 ⇒ iΨβ = jΨβ)

what is equivalent to ∀i, jS : (Ψ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


A rebase is a pair of two bases Base1 and Base2 and a relation → (called “can be replaced with”) between E1 and E2.

A reconstruction is a rebase between construct.

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

Rebase homomorphism from a rebase (Base1, Base2, →) to a rebase (Base1‘, Base2‘, →’) is a pair (Ψ1, Ψ2) of construct homomorphisms Ψ1 from Base1 to Base1‘ and Ψ2 from Base2 to Base2‘ such that

∀α, β ∈ E1 : (α → β ⇒ Ψ1α →’ Ψ2β).

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

Rebase and reconstruction monomorphisms 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).

Rebase and reconstruction epimorphisms are such rebase and reconstruction homomorphism that Ψ1, Ψ2 are homomorphisms and

∀α, β ∈ E1 : (α → β ⇔ Ψ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 ∀α, β ∈ E2 : (α →’ β ⇒ Ψ -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 YE. Elements of Y are called symbols (or constant symbols).

Remark. Often ∀ω ∈ Y, iX : 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 Sys1 = Sys2 = (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 “index”, “zero”, “symbol”, not the last alphabet letters.) But why then 0 and 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 (Sys1, Sys2, →) is a pseudomorphism Ψ from Sys1 to Sys2 such that Ψ ⊆ (→) that is ∀α ∈ E1 : α → Ψα.

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 (Sys1, Sys2, →1) and (Sys2, Sys3, →2) correspondingly, then gf is a specialization function on (Sys1, Sys3, (→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.


By definition (for α ∈ E1, β ∈ E2) α ≤ β ⇔ ∀iS : (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 (Sys1, Sys2, →)) of the formula α is the set

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

Remark. α(…) ⊆ E2.

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

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

Theorem. Let α ∈ E1, β ∈ E2. Then (1) ⇒ (2) ⇒ (3):

  1. β ∈ α(…).
  2. Exists a specialization function Ψ on (Sys1|parts(α), Sys2|parts(β), →|parts(α) × parts(β)) such that Ψα = β.
  3. Pseud(α, β) and β/α is a specialization function on (Sys1|parts(α), Sys2|parts(β), →|parts(α) × parts(β)).

If also ∀β ∈ E2 : 0 → β, then the above statements are equivalent.

Proof. (2) ⇒ (3). Pseud(α, β) because a specialization function is a pseudomorphism. Ψ = β/α because β/α is the only pseudomorphism from Sys1|parts(α) to Sys2|parts(β) whose value on α is equal to β.

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

iS : (iα ≠ 0 ⇒ iα → iβ) and ∀i, jS : (iα = jα ≠ 0 ⇒ iβ = jβ).

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

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

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

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

So Ψ is a pseudomorphism from Sys1|parts(α) to Sys2|parts(β).

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

(3) ⇒ (1). (Provided ∀β ∈ E2 : 0 → β) Let ∀i, jS : (iα = jα ≠ 0 ⇒ iβ = jβ) and β/α is a specialization function on (Sys1|parts(α), Sys2|parts(β), →|parts(α) × parts(β)). Because β/α is a specialization function, ∀γ ∈ parts(α) : γ → (β/α)γ.

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

By definition <f>x = fxx ∈ dom f; <f>x = xx ∉ 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 (Sys1|parts(α), Sys2|parts(β), →|parts(α) × parts(β)).

The direct implication of the above is obvious.

Let β/α is a specialization function on (Sys1|parts(α), Sys2|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 (Sys1|parts(α), Sys2|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γ.

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 (Sys1, Sys2, →) to (Sys1‘, Sys2‘, →’), then α ≤ β ⇒ Ψ1α ≤ Ψ2β for α ∈ E1, β ∈ E2.

Proof. Let α ≤ β that is ∀iS : (iα ≠ 01iα → iβ). Let also Ψiα ≠ 0′. We need to prove Ψ1iα →’ Ψ2iβ. We have iα ≠ 0. So iα → iβ; Ψ1iα →’ Ψ2iβ. End of proof.

Proposition. Let Sys1, Sys2, Sys1‘, Sys2‘ be systems of constructs, Ψ1 is construct isomorphism from Sys1 to Sys1‘ and Ψ2 is construct homomorphism from Sys2 to Sys2‘. Then Pseud(α, β) ⇒ Pseud(Ψ1α, Ψ2β).

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

Theorem. If Ψ = (Ψ1, Ψ2) is a reconstruction isomorphism from (Sys1, Sys2, →) to (Sys1‘, Sys2‘, →’), then β ∈ α(…) ⇔ Ψ2β ∈ (Ψ1α)(…) for α ∈ E1, β ∈ E2.

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 (Sys1, Sys’, →1), (Sys2, Sys’, →2), (Sys3, Sys’, →3) be some reconstructions.

The least common specialization LCS(α, β) of constructs α ∈ Sys1 and β ∈ Sys2 is construct γ ∈ Sys3 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 Sys3 = 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). Apparently this algorithm exists only for the concrete representation.]

[TODO: Also greatest common generalization.]

Part 2. Representation Related Properties of Formulas



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 QS of all functions from S to Q.

By definition iα = {(p, α(pi)) | pS} for α ∈ QS.

Tree(Q, X) = (QS, 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 (QS, X, {(i, 0) | iS}).

Constantness of a Construct

Definition. Given a reconstruction (Sys1, Sys2, →) constantness Ωα of a construct α ∈ E1 is

Ωα = {β ∈ E2 | ¬(α → β)}.

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α) | iS}.

Proposition. Form is a construct homomorphism.

Proof. jForm α = {(p, Ωpjα) | pS} = Form jα for jS. End of proof.

Proposition. Form α = Form β ⇔ ∀iS : Ωiα = Ωiβ ⇔ ∀iS, γ ∈ E2 : (iα → γ ⇔ iβ → γ).

Proof. Obvious.

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

  1. Form α = Form β;
  2. iS : (iα ∈ Yiβ ∈ Yiα = iβ);
  3. iS : (iα ≠ iβ ⇒ iα, iβ ∉ Y);
  4. α ≤ β ∧ β ≤ α.

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

α ≤ β ⇔ ∀iS : (iα ∈ Yiβ = iα).

So α ≤ β ∧ β ≤ α ⇔ ∀iS : (iα ∈ Yiβ ∈ Yiβ = iα). End of proof.

Shadow of a Construct. Equivalence of Constructs

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

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

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

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

iS : ((iα, iβ ∉ Yiα = iβ ∈ Y) ∧ iα = 0 ⇔ iβ = 0).

Equivalently transforming the propositional formula under the quantifier, we get

iα, iβ ∉ Yiα = 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β ∈ Yiα, iβ ∉ {0}) ∨ iα = iβ ∈ Y ∩ {0} ⇔

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

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

End of proof.

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

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

Applying Operators to Parts of Formulas

Applying an Operator to a Subformula

I will denote ij iff the sequence i is a start part of the sequence j for i, jS. (Note that i = jij.)

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

If iX then by definition applying f to the i-th (iS) component (or i-th part) of α is

(f@i)α = {(k, Ωkα) | kS, ¬(ik)} ∪ {(ji, Ωjfiα) | jS}.

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


  • ((f@i)α)k = Ωkα ⇐ ¬(ik);
  • ((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: AE is by definition the basis (EA, X) with indices extended onto the set A by the formula iα = ifα for α ∈ A, iX.

iα = i<f

(E, X) ∪ f -1A

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: AB where sets A, BE such that:

  • AB = ∅ ;
  • B is closed.

Let fD = f ∪ (=)|B. (fD is an operator (AB) → B.)

Definition. Recursive applying operator f is the operator Rec(f) = R(fD). [TODO: What if we would replace RbyL 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.iX : iRec(f)α = Rec(f)ifDα.

Proof. iRec(f)α = iR(fD)α = R(fD)ifDα = Rec(f)ifDα. End of proof.

Lemma. For iX

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

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

Theorem. For iS

  1. iRec(f)α = Rec(f)iα ⇐ α ∈ B;
  2. iRec(f)α = Rec(f)ifα ⇐ α ∈ Ai ≠ ().

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

2. pnp1Rec(f)α = pnp2Rec(f)p1fα = Rec(f)pnp2p1. (I used the previous item.) End of proof.

On a System of Formulas

Let we have a system Sys of formulas.

From the above

  • ΩiRec(f)α = Ωiα ⇐ α ∈ B;
  • ΩiRec(f)α = Ωifα ⇐ α ∈ Ai ≠ ().


  • iRec(f)α ~ iα ⇐ α ∈ B;
  • iRec(f)α ~ ifα ⇐ α ∈ Ai ≠ ().

If we will consider equivalent formulas equal, that is will replace ~ by = in the above formulas, we will get exactly the traditional definition (with iX) 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 EE* = ∅ (that is E* is a duplicate of E).

Let X* be a set related to X by a bijective relation ii* for iX, i* ∈ X*. (I also assume XX* = ∅ .) By definition i*α = i*Dα = Diα. So (EE*, 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 (EE*, 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);
  • Y0, Y1, Y2, …, Yn, … be correspondingly nullary, unary, binary, …, n-ary operations.

We will define: Y = Y0Y1Y2 ∪ …; X = ℕ.

E* is recursively defined as the union of:

  • V;
  • all lists of the form (ωn α0 … αn-1) where ωnYn, αiE*.

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 VY ∪ {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 Yi = 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 β: α → β.
  • iS \ {()} : iα = 0 ∉ Y. So ∀iS \ {()} : iα → iβ. Assembling this we have ∀iS : iα → iβ that is β ≥ α.
  • i, jS : (iα = jα ≠ 0 ⇒ iβ = jβ) because iα ≠ 0 ⇒ i = (). So Pseud(α, β). As a result β ∈ α(…).
  • Let α ∈ Y. Then α → β ⇔ α = β.
  • Let α = (ωn α0 … αn-1) where ωnYn, αiE*.
  • α → β ⇔ α = β ∨ (α ∉ 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 ∀iS : iα → iβ.


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))(U2+V3) = U2#V3 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)γ | iS, 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> = fxx ∈ dom f and <f>x = xx ∉ 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 nX.

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), nX. I will denote nGa 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+12 and 2+22.

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.


  • (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 reala+realb = realb+reala.

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.

Leave a Reply

Your email address will not be published. Required fields are marked *