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, +₁ (+ 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¹ 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₁ to E₂ an operator from a basis Base₁ to a basis Base₂. An operator from a basis to itself will be called an operator on this basis.

I will denote bases as Base, Base₁, Base₂, …

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₀ of zero or more indices p_i ∈ X. To a sequence of indices corresponds an operator on E: (p_n…p₀)α = p_n(p_{n – 1}…(p₀α)…).

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₁ = X₂ = … = X.

The case of two bases (E₁, X₁) and (E₂, X₂) such that X₁ ≠ X₂ 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₁ and E₂ some f can be operator on both E₁ and E₂ (for example if f is a function E₁ ∪ E₂ → E₁ ∩ E₂).

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

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

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

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

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

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

When we have two bases (E₁, X₁), (E₂, X₂) and a pair (Ψ, λ) of an operator Ψ from E₁ to E₂ and a reindexation function λ from X₁ to X₂, we can first apply reindexing to get the basis (E₂, X₁) and then consider Ψ as an operator from (E₁, X₁) to (E₂, X₁). (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₁, …, p_n ∈ X

• p_n…p₁R(f) = R(f)p_nf…p₁f;
• p_n…p₁L(f) = R(f)fp_n…fp₁.

Proof. By properties of reindexation:

• p_n…p₁R(f) = p_n…p₂R(f)p₁f = p_n…p₃R(f)p₂fp₁f = … = R(f)p_nf…p₁f.
• p_n…p₁L(f) = p_n…p₂L(f)fp₁ = p_n…p₃L(f)fp₂fp₁ = … = L(f)fp_n…fp₁. 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₁, X) to a basis (E₂, X) is a function Ψ: E₁ → E₂ such that ∀i ∈ X : Ψi = iΨ.

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

Proof. Reverse implication. Obvious.

Direct implication. Ψp_n…p₀ = p_nΨp_n-1…p₁ = … = p_n…p₁Ψp₀ = p_n…p₀Ψ. 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 Ψ = E₂.

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:

1. A is subconstruct closed.
2. ∀α ∈ A, i ∈ X : iα ∈ A.
3. ∀α ∈ 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 : i0 = 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 : 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 i ∈ E by the formula i0 = 0.)

I will denote systems of constructs as Sys, Sys₁, Sys₂, … and the corresponding sets of constructs as E, E₁, E₂, …, corresponding sets of indices as X, X₁, X₂, … 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₁, X, 0) to a system of constructs (E₂, X, 0) a function from E₁ to E₂ 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α = 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₀]p₁…p_n = p₁…p_n[p₀p₁…p_n] for any operators p₀, …, p_n.

Theorem. [p_m…p₀][p_n…p₀] = [p_max(n,m)…p₀].

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₁ = (E₁, X₁, 0₁) and Sys₂ = (E₂, X₂, 0₂) be two systems of constructs. Let λ be a reindexation function from the basis (E₁, X₁) to the basis (E₂, X₂). Let the basis (E₂, X₁) be the reindexed (with λ) basis (E₂, X₂).

Then λ is called reindexation function from the system of constructs Sys₁ to the system of constructs Sys₂. The system of constructs (E₂, X₁, 0₂) = λ^-1(E₂, X₂, 0₂) is called reindexed (with λ) system of constructs (E₂, X₂, 0₂).

To show that (E₂, X₁, 0₂) is really a system of constructs we need to prove that i0₂ = 0₁ for i ∈ X₁. We have i0₂ = (λi)0₁ = 0₁.

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₁, X, 0) and (E₂, 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₁ = 0₂ = … = 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₁ is E₂ and of 0₁ is 0₂. 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₁ to Sys₂ is such operator from E₁ to E₂ that ∀i ∈ X : Ψi = iΨ[i].

Proposition. An operator Ψ from E₁ to E₂ 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₀ = p_n…p₁Ψ[p_n…p₁]p₀ = p_n…p₁Ψp₀[p_n…p₀] = p_n…p₀Ψ[p₀][p_n…p₀] = p_n…p₀Ψ[p_n…p₀]. 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 Ψ₁ and Ψ₂ are construct pseudomorphisms. We have Ψ₂Ψ₁iα = Ψ₂iΨ₁[i]α = iΨ₂[i]Ψ₁[i]α.

Ψ₁[i]α ≠ 0 ⇒ Ψ₂Ψ₁iα = iΨ₂Ψ₁[i]α; Ψ₁[i]α = 0 ⇒ Ψ₂Ψ₁iα = Ψ₁[i]α = iΨ₂Ψ₁[i]α.

So Ψ₂Ψ₁iα = iΨ₂Ψ₁[i]α. End of proof.

Pseudomorphic Image

Definition. Let α ∈ E₁, β ∈ E₂, Then Pseud(α, β) ⇔ β is a pseudomorphic image of α ⇔ there exists a pseudomorphism Ψ from Sys₁ to Sys₂ such that β = Ψα.

Proposition. Pseud(α, β) ∧ Pseud(β, γ) ⇒ Pseud(α, γ) for α ∈ E₁, β ∈ E₂, γ ∈ E₃.

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.

Definition. Let Pseud(α, β) where α ∈ E₁, β ∈ E₂. β/α (factor of β by α) is the operator which is a construct pseudomorphism from Sys₁|_parts(α) to Sys₂|_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.

1. Let Pseud(α, β) where α ∈ E₁, β ∈ E₂. If Ψ is a construct pseudomorphism from Sys₂ to Sys₃ then Pseud(α, Ψβ) and Ψ(β/α) = (Ψβ)/α.
2. If α, β ∈ E₁ and Pseud(α, β) and Ψ is a construct monomorphism from Sys₁ to Sys₂ 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 rebase is a pair of two bases Base₁ and Base₂ and a relation → (called “can be replaced with”) between E₁ and E₂.

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 (Base₁, Base₂, →) to a rebase (Base₁‘, Base₂‘, →’) is a pair (Ψ₁, Ψ₂) of construct homomorphisms Ψ₁ from Base₁ to Base₁‘ and Ψ₂ from Base₂ to Base₂‘ such that

∀α, β ∈ E₁ : (α → β ⇒ Ψ₁α →’ Ψ₂β).

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

Rebase and reconstruction monomorphisms are such rebase and reconstruction homomorphism that both Ψ₁ and Ψ₂ are injective.

These monomorphisms have the reverse defined as (Ψ₁, Ψ₂) ^-1 = (Ψ₁^-1, Ψ₂^-1).

Rebase and reconstruction epimorphisms are such rebase and reconstruction homomorphism that Ψ₁, Ψ₂ are homomorphisms and

∀α, β ∈ E₁ : (α → β ⇔ Ψ₁α →’ Ψ₂β).

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. Ψ₁ and Ψ₂ are construct isomorphisms; consequently Ψ₁^-1 and Ψ₂^-1 are also construct isomorphisms. We have left to prove that ∀α, β ∈ E₂ : (α →’ β ⇒ Ψ ^-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₁ = Sys₂ = (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 (Sys₁, Sys₂, →) is a pseudomorphism Ψ from Sys₁ to Sys₂ such that Ψ ⊆ (→) that is ∀α ∈ E₁ : α → Ψα.

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₁, Sys₂, →₁) and (Sys₂, Sys₃, →₂) correspondingly, then gf is a specialization function on (Sys₁, Sys₃, (→₂)◦(→₁)).

Proof. That gf is a pseudomorphism is proved above. We have left to prove that gf ⊆ (→₂)◦(→₁). It follows from that f ⊆ (→₁), g ⊆ (→₂). 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₁, β ∈ E₂) α ≤ β ⇔ ∀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₁, Sys₂, →)) of the formula α is the set

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

Remark. α(…) ⊆ E₂.

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₁, β ∈ E₂. Then (1) ⇒ (2) ⇒ (3):

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

If also ∀β ∈ E₂ : 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₁|_parts(α) to Sys₂|_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₁|_parts(α) to Sys₂|_parts(β).

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

(3) ⇒ (1). (Provided ∀β ∈ E₂ : 0 → β) Let ∀i, j ∈ S : (iα = jα ≠ 0 ⇒ iβ = jβ) and β/α is a specialization function on (Sys₁|_parts(α), Sys₂|_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₁|_parts(α), Sys₂|_parts(β), →|_{parts(α) × parts(β)}).

The direct implication of the above is obvious.

Let β/α is a specialization function on (Sys₁|_parts(α), Sys₂|_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₁|_parts(α), Sys₂|_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 Ψ = (Ψ₁, Ψ₂) is a reconstruction homomorphism from (Sys₁, Sys₂, →) to (Sys₁‘, Sys₂‘, →’), then α ≤ β ⇒ Ψ₁α ≤ Ψ₂β for α ∈ E₁, β ∈ E₂.

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

Proposition. Let Sys₁, Sys₂, Sys₁‘, Sys₂‘ be systems of constructs, Ψ₁ is construct isomorphism from Sys₁ to Sys₁‘ and Ψ₂ is construct homomorphism from Sys₂ to Sys₂‘. Then Pseud(α, β) ⇒ Pseud(Ψ₁α, Ψ₂β).

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

Theorem. If Ψ = (Ψ₁, Ψ₂) is a reconstruction isomorphism from (Sys₁, Sys₂, →) to (Sys₁‘, Sys₂‘, →’), then β ∈ α(…) ⇔ Ψ₂β ∈ (Ψ₁α)(…) for α ∈ E₁, β ∈ E₂.

Proof. β ∈ α(…) ⇒ Ψ₂β ∈ (Ψ₁α)(…) directly follows from two previous statements. Because Ψ₁, Ψ₂ are bijections, then also analogously Ψ₂β ∈ (Ψ₁α)(…) ⇒ β ∈ α(…). End of proof.

Least Common Specialization

Let (Sys₁, Sys’, →₁), (Sys₂, Sys’, →₂), (Sys₃, Sys’, →₃) be some reconstructions.

The least common specialization LCS(α, β) of constructs α ∈ Sys₁ and β ∈ Sys₂ is construct γ ∈ Sys₃ 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₃ = Sys’ be a system of formulas and →₃ 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

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₁, Sys₂, →) constantness Ωα of a construct α ∈ E₁ is

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

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. jForm α = {(p, Ωpjα) | p ∈ S} = Form jα for j ∈ S. End of proof.

Proposition. Form α = Form β ⇔ ∀i ∈ S : Ωiα = Ωiβ ⇔ ∀i ∈ S, γ ∈ E₂ : (iα → γ ⇔ iβ → γ).

Proof. Obvious.

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

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

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).²

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 ^-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: 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 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. ∀i ∈ X : iRec(f)α = Rec(f)if_Dα.

Proof. iRec(f)α = iR(f_D)α = R(f_D)if_Dα = Rec(f)if_Dα. End of proof.

Lemma. For i ∈ X

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

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

Theorem. For i ∈ S

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

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

2. p_n…p₁Rec(f)α = p_n…p₂Rec(f)p₁fα = Rec(f)p_n…p₂p₁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

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

So

• iRec(f)α ~ iα ⇐ α ∈ B;
• iRec(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₀, Y₁, Y₂, …, Y_n, … be correspondingly nullary, unary, binary, …, n-ary operations.

We will define: Y = Y₀ ∪ Y₁ ∪ Y₂ ∪ …; X = ℕ.

E* is recursively defined as the union of:

• V;
• all lists of the form (ω_n α₀ … α_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 α₀ … α_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²+V³) = U²#V³ 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 ω(α₀ … α_n) instead of (ω α₀ … α_n).

By definition H(ω(α₀ … α_n)) = ω for n ≥ 0. (H is called the head of the formula ω(α₀ … α_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}.³

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_Ga 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 +₁ and +₂. It can be formalized in our system as the constant symbol “+” with a modifier: 2+₁2 and 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)₁ ∈ (a + b)(…) or ((a|) (+|) (b|) | 1) ∈ ((a|) (+|) (b|) |)(…);
• (a +₁ 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.