21 Century Math Method - a Replacement of Axiomatic Method.
Part 1.1: Axiomatic Theory of Formulas

Formulas are an important topic in the science.
Formulas however were 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, axiomatic theory, math logic, mathematical logic, foundation of math, foundation of mathematics, math foundations, variable substitution, morphisms, representation of formulas, representation of expressions, expression representations, algebraic logic, graphs, binary trees, nary trees, n-ary trees, lists of lists, subexpression, subformula, constituent parts, components, indexes, indices, basis, reindexation, coordinate transformation function, coordinate system transformation function, symbolic algebra, constant symbol, mathematical symbol, abstract mathematical theory, abstract theory, abstract math theory, abstract mathematics, abstract math, mathematical abstraction, math abstraction

Preface

See also:

Overview

This article contains the axiomatic theory which can be called either:

• Operator Theory of Formulas ™;

• Operator Theory of Expressions ™;

• Operator Formulas Theory ™;

• Operator Expressions Theory ™.

Draft Status

This is a draft. It was recently updated and there may be not yet found mistakes in the new revision. 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 E1 to E2 an operator from a basis (E1, X1) to a basis (E2, X2). An operator from a basis (E, X) will be called an operator on this basis.

Obvious. Indices are operators on the basis.

By definition S (I call it the set of sequences) is the set of all finite sequences pn...p0 of zero or more indices pi ∈ X. To a sequence of indices corresponds an operator on E: (pn...p0)α = 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 X1 ≠ X2 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 E1 ∪ E2 → E1 ∩ E2).

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

Definition. Let X, λX are sets, λ (called a reindexation function) is an operator X → λX and let (E2, λX) is a basis. For i ∈ X, β ∈ 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) which 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 from 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 i ∈ S!

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) is a basis. Let f is 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 p1, ..., pn ∈ X

• pn...p1R(f) = R(f)pnf...p1f;

• pn...p1L(f) = R(f)fpn...fp1.

Proof. By properties of reindexation:

• pn...p1R(f) = pn...p2R(f)p1f = pn...p3R(f)p2fp1f = ... = R(f)pnf...p1f.

• pn...p1L(f) = pn...p2L(f)fp1= pn...p3L(f)fp2fp1= ... = L(f)fpn...fp1. 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 Ψ:  E1 → E2 such that ∀i ∈ X : Ψi = iΨ.

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

Proof. Reverse implication. Obvious.

Direct implication. Ψpn...p0 = pnΨpn-1...p1 = ... = pn...p1Ψp0 = pn...p0Ψ. 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α | 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 subset Z⊆ E (elements of Z are called null or nil constructs) such that ∀i ∈ X, 0 ∈ Z : i0 = 0.

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. A basis can be considered as a system of constructs with Z = ∅.

Operators on Systems of Constructs

I will call an operator from a system of constructs (E1, X, Z) to a system of constructs (E2, X, Z) a function from E1 to E2 such that ∀0 ∈ Z : 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α ∉ Z ⇒ [p]α = α;    pα ∈ Z ⇒ [p]α = pα.

It is really an operator because p0 = 0 and so [p]0 = p0 = 0 for any 0 ∈ Z.

Obvious. When Z = {0} these formulas take the form [p]α = α ⇐ pα ≠ 0 and [p]α = 0⇐ pα = 0.

Proposition. p[p] = p.

Proof. pα ∉ Z ⇒ p[p]α = pα and pα ∈ Z ⇒ [p]α = ppα = pα. End of proof.

Proposition. pα ∈ Z ⇒ [p]α ∈ Z.

Proof. pα ∈ Z ⇒ [p]α = pα ∈ Z.

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

Proof. pqα ∉ Z ⇒ [pq]α = α; pqα ∈ Z ⇒ [pq]α = pqα;

pqα ∉ Z ⇒ [p]qα = qα; pqα ∈ Z ⇒ [p]qα = pqα;

pqα∉ Z ⇒ q[pq]α = qα; pqα∈ Z ⇒ q[pq]α = qpqα = pqα.

So pqα∉ Z ⇒ q[pq]α = [p]qα and pqα∈ Z ⇒ q[pq]α = [p]qα. ∀α ∈ E : q[pq]α = [p]qα. End of proof.

Obvious consequence. [p0]p1...pn = p1...pn[p0p1...pn] for any operators p0, ..., pn.

Theorem. [pm...p0][pn...p0] = [pmax(n,m)...p0].

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

pα ∈ Z ⇒ [p]α = pα ∈ Z ⇒ [qp][p]α = qp[p]α = qpα; pα ∈ Z ⇒ qpα ∈ Z ⇒ [qp]α = qpα; pα ∈ Z ⇒ [qp][p]α = [qp]α.

pα ∉ Z ⇒ [p]α = α ⇒ [qp][p]α = [qp]α.

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

Construct Morphisms

Reindexation of Constructs

Let Sys1 = (E1, X1, Z1) and Sys2 = (E2, X2, Z2) are two systems of constructs. Let λ is reindexation function from the basis (E1, X1) to the basis (E2, X2). Let the basis (E2, X1) is 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, Z2) = λ-1(E2, X2, Z2) is called reindexed (with λ) system of constructs (E2, X2, Z2).

To show that (E2, X1, Z2) is really a system of constructs we need to prove that i0 = 0 for i ∈ X1, 0 ∈ Z2. 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, Z) of constructs (with additional requirement that ∀0 ∈ Z : Ψ0 = 0.)

Likewise we can make two systems of constructs (considered as universal algebras) to make agree on the same set of unary operations Z. [TODO: Explain in more details about this. Is order of two operations: reindexation and making agreeing on Z significant?]

Homomorphisms and Isomorphisms

By definition construct homomorphism is such basis homomorphism Ψ that ∀0 ∈ Z : Ψ0= 0. (I recall that we have limited our consideration to the case Z1 = Z2 = ... = Z.)

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 Z1 is Z2. 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 Sys1 to Sys2 is such operator from E1 to E2 that ∀i ∈ X : Ψi = iΨ[i].

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

Proof. Reverse implication. Obvious.

Direct implication. By induction by n for pi ∈ X:

Ψpn...p0 = pn...p1Ψ[pn...p1]p0 = pn...p1Ψp0[pn...p0] = pn...p0Ψ[p0][pn...p0] = pn...p0Ψ[pn...p0]. End of proof.

Proposition. Construct homomorphism is a construct pseudomorphism.

Proof. Let Ψi = iΨ. Then iα ∉ Z ⇒ Ψiα = iΨα = iΨ[i]α; iα ∈Z ⇒ Ψ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[i]Ψ1[i]α.

Ψ1[i]α ∉ Z ⇒ Ψ2Ψ1iα =  iΨ2Ψ1[i]α; Ψ1[i]α ∈ Z ⇒ Ψ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, j ∈ S : (iα = jα ∉ Z ⇒ iβ = jβ).

Proof. Direct implication. Let β = Ψα where Ψ is a construct pseudomorphism and iα = jα ∉ Z. Then

iβ = iΨα;    iα ∉ Z ⇒ iβ = iΨ[i]α = Ψiα;    iα = jα ∉ Z ⇒ iβ = Ψiα = Ψjα = jβ.

Reverse implication. Let ∀i, j ∈ S : (iα = jα ∉ Z ⇒ iβ = jβ). Then ∀i ∈ S : (iβ = fiα ⇐ iα ∉ Z) 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α ∉ Z where j ∈ S. 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 ∀i ∈ S : (iα ∉ Z ⇒ (β/α)iα = iβ).

Proof. If iα ∉ Z 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α ∉ Z ⇒ fiα = iβ = giα. So fiα = giα. End of proof.

Theorem. [TODO: Can't this theorem be made stronger?]

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 isomorphism 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, j ∈ S : (iα = jα ∉ Z ⇒ iβ = jβ) and need to prove

∀i, j ∈ S : (iΨα = jΨα ∉ Z ⇒ iΨβ = jΨβ)

what is equivalent to ∀i, j ∈ S : (Ψiα = Ψjα ∉Z ⇒ Ψiβ = Ψjβ).

Taking in account that Ψ is a injection, Ψiα = Ψjα ∉Z ⇒ iα = jα ∉ Z ⇒ iβ = jβ ⇒ Ψiβ = Ψjβ. End of proof.

Reconstructions and Systems of Formulas

Reconstructions

A reconstruction is a pair of two systems of constructs Sys1 and Sys2 and a relation → (called "can be replaced with") between E1 and E2. [TODO: More general case when Sys1 and Sys2 are bases rather than constructs.]

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

Reconstruction homomorphism from a reconstruction (Sys1, Sys2, →) to a reconstruction (Sys1', Sys2', →') is a pair (Ψ1, Ψ2) of construct homomorphisms Ψ1 from Sys1 to Sys1' and Ψ2 from Sys2 to Sys2' such that

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

Reconstructionmonomorphism is such reconstruction homomorphism that both Ψ1 and Ψ2 are injective.

Reconstruction monomorphism has the reverse defined as (Ψ1, Ψ2)-1= (Ψ1-1, Ψ2-1 ).

Reconstructionepimorphism is such reconstruction homomorphism that Ψ1, Ψ2 are construct homomorphisms and

∀α, β ∈ E1 : (α → β ⇔ Ψ1α →' Ψ2β).

Reconstructionisomorphism is reconstruction homomorphism which is both reconstruction monomorphism and reconstruction epimorphism.

Proposition. The reverse of a reconstruction isomorphism is a 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, Z) and a set Y ⊆ E. Elements of Sys are called symbols (or constant symbols).

Remark. Often ∀ω ∈ Y, i ∈ X : iω ∈ Z (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, Z, Y) corresponds a reconstruction with Sys1 = Sys2 = (E, X, Z) and "can be replaced with" relation defined as α → β ⇔ α = β ∨ (α ∉ Y ∧ β ∉ Z).

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

• α → β;

• α = β ∨ (α ∉ Y ∧ β ∉ Z);

• (α ∈ Y ∨ β ∈ Z) ⇒ α = β;

• α ≠ β ⇒ (α ∉ Y ∧ β ∉ Z).

Remark. It seems that it is God who has chosen the letters (X, Z, 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 Z and Y are reversed in the order? Isn't it a hint that we should first define formulas without Z 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 γ ∉ Z, then α → γ is obvious. If α ∈ Y, then α → β ⇔ α = β and so α → β ∧ β → γ ⇒ α = β ∧ β → γ ⇒ α → γ. If γ ∈ Z, 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 ∨ Ψα ∈ Z ⇒ α = Ψα).

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

α ∈ Y ∨ Ψα ∈ Z ⇒ α = Ψα 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.

Specialization

By definition (for α ∈ E1, β ∈ E2) α ≤ β ⇔ ∀i ∈ S : 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 ∀0 ∈ Z, β ∈ 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

∀i ∈ S : iα → iβ and ∀i, j ∈ S : (iα = jα ∉ Z ⇒ iβ = jβ).

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

We have ∀i, j ∈ S : (jiα ∉ Z ⇒ Ψjiα = jΨiα).

That is ∀γ ∈ dom Ψ, j ∈ S : (jγ ∉ Z ⇒ Ψjγ = jΨγ), what is the same as

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

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

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

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

We have ∀i ∈ S : iα → (β/α)iα. But iα ∉ Z ⇒ (β/α)iα = iβ. So ∀i ∈ S : (iα ∉ Z ⇒ 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 (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 ∨ Ψγ ∈ Z ⇒ γ = Ψγ).

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γ = iγ.

If iγ ∈ Z, then Ψiγ = iγ ∈ Z and iΨ[i]γ = iγ. If iγ ∉ Z, 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 ∀i ∈ S : (iα ≠ 01 ⇒ iα → 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' are 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, j ∈ S : (iα = jα ∉ Z ⇒ iβ = jβ). Let iΨ1α = jΨ1α ∉ Z or equivalently Ψ1iα = Ψ1jα ∉ Z. Then because Ψ1 is a bijection, iα = jα and moreover iα = jα ∉ Z. 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) are 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' is 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).]

Postface

References

21 Century Math Method and Operator Theory of Formulas

Misc Math Logic

Legal

About the Primary Author of the Method