21 Century Math Method - a Replacement of Axiomatic Method.
Part 1.2: Representation Related Properties of Formulas

Formulas are an important topic in the science.
This topic however was probably almost not researched by mathematicians until 2005 year.

Keywords: theory of formulas, theory of expressions, expressions theory, formulas theory, mathematical theory of formulas, mathematical theory of expressions, theory of mathematical formulas, mathematical formulas theory, formulae, representation of formulas, representation of expressions, expression representations, binary trees, nary trees, n-ary trees, lists of lists, directed graphs, directed multigraphs, data structures representation, representation of data structures, data structures theory, theory of data structures, axiomatic theory, math logic, mathematical logic, foundation of math, foundation of mathematics, math foundations, variable substitution, constituent parts, components, indexes, indices, pattern substitution, substitution of patterns, symbolic algebra, recursion, recursive applying function

Preface

Overview

Draft Status

This is a draft. Some sections are yet missing. However this is already a quite useful text.

WARNING. The current version of this document is based on a wrong definition of reconstruction on system of formulas from an old version of the first part of this article. (This will be corrected.)

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)) | p ∈ S} 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) | i ∈ S}).

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 with 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, γ ∈ E2 : (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.]

[XXX] 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 fD = f ∪ (=)|B. (fD is an operator (A ∪ B) → B.)

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

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

Let α ∈ E.

Lemma. ∀i ∈ X : iRec(f)α = Rec(f)ifDα.

Proof. iRec(f)α = iR(fD)α = R(fD)ifDα = Rec(f)ifDα. 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. pn...p1Rec(f)α = pn...p2Rec(f)p1fα = Rec(f)pn...p2p1fα. (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 ~ with = 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) is a basis and f is a function from a subset of E to E. We will define Rec(f) in this general case.

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

Let X* is a set related with X by 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 with 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.]

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, ... are correspondingly nullary, unary, binary, ..., n-ary operations.

We will define: Z = {0}; Y = Y0 ∪ Y1 ∪ Y2 ∪ ...; X = ℕ.

E* is recursively defined as union of:

• V;

• all lists of the form (ωn α0 ... αn-1) where ωn ∈ Yn, α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 ∪ Z is always 0.

(E, X, Z, 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, β ∉ Z. Then α ∉ Z ∧ α ∉ 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α ∉ Z ⇒ iβ = jβ) because iα ∉ Z ⇒ i = (). So Pseud(α, β). As a result β ∈ α(...).

•  

• Let α ∈ Y. Then α → β ⇔ α = β.

•  

• Let α = (ωn α0 ... αn-1) where ωn ∈ Yn, αi ∈ E*.

•  

• α → β ⇔ α = β ∨ (α ∉ Y ∧ β ∉ Z).

•  

• 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))(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→ β)γ ∈ β(...).??

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:

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 is 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 with ω 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 is 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 is a DMGWIE, a ∈ vertices(G), n ∈ X. I will denote nGa such b ∈ vertices(G) that (a, b, n) ∈ edges(G).

Let G is 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.

Example.

• (a + b)1 ∈ (a + b)(...) or ((a|) (+|) (b|) | 1) ∈ ((a|) (+|) (b|) |)(...);

• (a +1 b) ∈ (a + b)(...) or ((a|) (+|1) (b|) |) ∈ ((a|) (+|) (b|) |)(...).

Example. We could denote real number variables as the constant symbol "real" with indexes (specializations of "real"). Then the school algebra equation a+b = b+a could be formalized as reala+realb = realb+reala.

Postface

References

21 Century Math Method and Operator Theory of Formulas

Misc Math Logic

Legal

About the Primary Author of the Method