21st Century Math Method - a Replacement of Axiomatic Method

- What we have been researching?

- We were researching vectors.

- But what we should research?

- We should research arrows of vectors.

Preface

Overview

Draft Status

Last updated 2005-04-24 08:42 pm.

This is a draft, however it is quite readable. The most important defect of this document is that today the proof of the main theorem is missing. (I'm sure that even if the main theorem is wrong, this article may be corrected to become right, that is that it is correct in the essence. This theorem is expected to be simple to prove.)

Comparison with Traditional Math

The things expressed in traditional math by quantifiers can be expressed in 21MM by defining new concepts.

Not likely to traditional math, 21MM doesn't use nor logics of predicates nor set theory. (However set theories can be expressed as some extensions of systems of axioms in 21MM.) This may have philosophical implication that the reality may be something not set theoretic, and about existence of God.

Any theorem proof in the formal system of logics of predicates can be easily rewritten in 21MM but not vice verse. [TODO: Write the algorithm (it is well known).]

Unlikely traditional math, 21MM does not need a meta-language (such as natural human language) for expressing properties of a system of axioms. This makes 21MM a very good formal system for computer logics. (However a meta-language may probably be needed for expressing relations between several systems of axioms (or a system of axioms with itself).

21MM is more perfect than traditional logics in the sense that it provides us with one (standardized) way to write several modifications of a proof in traditional math. (A problem for the reader to formalize this statement.)

21MM can be considered as a modification of axiomatic method with exclusion of set theory and quantifiers and addition of new kinds of definitional constructs. Note that exclusion of set theory is a kind of a benefit due to very unbeautify of known set theory axiomatics. So, 21MM is a continuation of the idea of the axiomatic method.

We have a way back from 21MM to axiomatic method that is having a (big) system of axioms which includes set theory. 21MM theory with set theoretic axioms is equivalent to an axiomatic theory. (A problem for the reader to show this.)

The Formal System

Symbols

In the current version of 21th century math method there are two kinds of symbols (not counting braces/parentheses):

• constant symbols denoted by small letters, digits 0-9, +, -, /, ∧, ¬ etc. (may denote constants, functions, relations etc.);

• variable symbols denoted by capital letters (used for variable substitution).

The following constant symbols are called primary symbols. [TODO: Exclude the concept of primary symbols...]

• 0 (false);

• ∧ (conjunction);

• ⇒ (implication);

• → (substitution);

• = (equality).

Expressions

I will denote expressions with small Greek letters.

Let's call an expression a list, elements of which are either symbols or (recursively) expressions. (Expressions must be finite.)

Let's call a variable (constant) an expression consisting of one element which is a variable (constant) symbol.

Let's call a variable substitution α(...) in an expression α the the set of expressions resulting from replacing all instances of a variable symbols in this expression (in the top level list and any of its sublists) by any (fixed) expression, also we will count that α∈α(...).

Note that α(...) may be infinite.

Let's call a direct part of an expression an index of an element of this expression (considered as a list).

Let's call the value of a direct part of the expression the element of the expression (considered as a list) with given index.

Let's call a part of an expression, a (finite sequence of zero or more elements such that the first element is a direct part of the expression, the second element is a direct part of the value of this direct part etc.

Let's call the entire expression its part which is an empty sequence of indexes.

Let's call the value of a part of an expression:

• the expression itself if the part is the entire expression;

• (recursively) the value of the direct part of the value of the part of the expression which is the the given part without last index.

Let's call a variable substitution a function from the set of variable symbols into the set of expressions. A variable substitution f(α) applied to an expression α = (α0 ... αn) is by definition recursively (f(α0) ... f(αn)). (In other words, variable substitutions are defined to be distributive over lists.) We will denote the set of results of all variable substitutions applied to expression α as α(...).

Let's call expression α top-matched by expression β iff α ∈ β(...).

Let's call subexpressions of the expression α = (α0 ... αn) the set parts(α) recursively defined as

parts(α) = {α} ∪ {parts(α0), ..., parts(αn)}.

Let's call α matched by β iff γ ∈ β(...) ∃ α ∈ parts(γ).

Proposition. α is matched by β iff γ ∈ parts(β) ∃ α ∈ γ(...).

Proof. If γ ∈ parts(β) and α ∈ γ(...), then exists a variable substitution f such that α = f(γ) ∈ parts(f(β)), but f(β) ∈ β(...).

If γ ∈ β(...) and α ∈ parts(γ), then there exists a variable substitution f such that γ = f(β), α ∈ parts(f(β)). So α ∈ f(δ) for some δ ∈ parts(β). And α ∈ δ(...).

Let's call a match of an expression α a pair consisting of a part P of this expression and a top match β of the value of P. Let's call β the value of the match and P the place of the match.

Example. The expression (a+(B*c)^2)^3 is top-matched by the expression (A+B)^3 and matched by the expression (A*B)^2.

Let's call the replacement of the part P of expression α by expression β:

• the expression β if P is the entire expression;

• the list resulting from (recursively) replacing i-th element of α (considered as a list) by the replacement of the part P', where i is the first index of the sequence P and P' is the rest indexes.

I will use expressions like (α ∧ β) to denote conjunction, (α = β) to denote implication etc. I will also (for readability) sometimes omit parentheses. The symbols ∧, = etc. in such expressions are called heads of expressions. [TODO: More formally about heads.]

Substitutions

Let's call a substitution an expression matching A→B (pronounced as substitution of A by B).

Let's call the substitution α→β applied to the expression γ (or an expression γ with α substituted by β) and denote as (α→β)γ the set of replacements of the values of all matches of γ by α with β.

Note: It is trivial that applied substitution is always a finite set.

The Base Formal System

Remark. Base formal system is our formal system without axioms. Axioms are to be "loaded" over the base formal system later. The base formal system can be supplemented with different sets of axioms (e.g. of classical logic or intuitionistic logic etc.)

I will call a formal system a sequence of expressions every of which is either (see below):

• an axiom;

• a theorem;

• an equality definition;

• a backward axiom.

Some expressions at the start of a formal system may be chosen arbitrarily, these expressions are called axioms. However every 21MM formal system must contain the substitution axioms (see below).

I will call old theorems all expressions before a given expression (not only theorems but also axioms, equality definitions, and backward axioms).

A theorem (by definition) is either:

• the result of a variable substitution in an old theorem (variable substitution rule);

• conjunction of an old theorem with an other (or the same) old theorem (conjunction rule);

• either left or right part of an old theorem which is a conjunction (conjunction operand rule);

• applying an old theorem which is a substitution (that is top-matches to the pattern A→B) to an other (or the same) old theorem (substitution rule).

Potential theorems. New Expressions

Definition. Potential theorems are:

• any subexpressions of axioms, [TODO: Shouldn't we limit only to conjuncts?]

• (already written) equality definitions,

• right parts of backward axioms.

A new expression is an expression which no potential theorem matches and whose head is not a primary symbol. [TODO: Prove that it is enough to check only axioms, definitions, and backward axioms rather than all expressions.]

Proposition. Any theorem (in absence of additional equality definitions and backward axioms) is a result of variable substitution in a conjunct in the conjunction of all potential theorems.

Substitution Axioms

I call the following the substitution axioms and recommend to always use them together with the base formal system:

• (A→B)∧(B→C) ⇒ (A→C)

• (A→B)∧(B→A) → (A=B) (This axiom seems not necessary)

• (A=B) →  (A→B)

• (A=B) →  (B→A)

[TODO: Do we need at all any except of the first of these axioms?]

These axioms are not contradictory (nor to the base formal system, nor to the classical propositional logic, nor to their combination) because to → can be assigned the semantics of equality. [TODO: More detailed proof of this almost obvious statement.]

To these axioms can be also added any axioms of the classical propositional logic or its part e.g. the set of the axioms of the intuitinistic logic.

Theorem. The base formal system with main axioms and a full [TODO] set of axioms of the classical propositional logic allows to prove any expression which is a true statement in the classical propositional logic.

Proof. [TODO]

Remark. A→A is not an axiom (nor a theorem), and A=A is also not a theorem! It is to exclude nonsenses like (positive -1)=(positive -1) or (whole 0.5)=(whole 0.5). In the informal method description below you normally should also introduce a class of self-equal objects with the axiom:

(self_equal A) → (self_equal A) or (self_equal A) = (self_equal A)

and derive all normal object classes from self_equal adding axioms like this:

number → self_equal or (number A)=(number A).

We as well can operate with not self-equal classes. E.g., ¬((changing A)=(changing A)) may be an axiom, but is (god A)=(god A) a theorem for properly defined "god"?

Some Consequences

• (A=B) →  (B=A)

Equality Definitions

A new expression is such an expression to which does not match any subexpression of the previously written expressions and whose head is not a primary symbol. [TODO: Prove that it is enough to check only axioms, definitions, and backward axioms rather than all expressions.]

An equality definition is any expression of the form α = β, where α is a new expression and α is not a substitution.

Remark. If one wants to declare that a new expression α is true, he could write equality definition like this: α = 1 (provided that we have some system of axioms and definitions such that (1) is a theorem).

Proposition. Adding an equality definition to a noncontradictory formal system does not make it contradictory.

Proof. Suppose we added equality definition  α = β. Substitute α→β in every expression after the definition. This will not break the proof because α is a new expression and so the only what we know about α is that α = β what is also true when α is substituted by β (β = β). (W have taken into account that α isn't a substiotution and so cannot be used for a substitution rule) The resulting formal system is non-contradictory and so the original formal system will be also non-contradictory (we have taken in account that α cannot be the expression (0) because 0 is a primary symbol.)

[TODO: Formalize "our knowledge about expression α", "the only what we know".]

Because α is a new expression, α = β may top-match only to expressions like A = γ (that is with a variable at the left side). Any consequences produced will be the result of replacing in consequences of γ = γ (provable expressions) some instances of γ with α  

Backward Axioms

A backward axiom (Note: backward axioms are not axioms!) is a new expression α→β such that for every potential theorem δ∈β(...), exists old theorem γ such that δ is a result of variable substitution in (α→β)(γ) (α→β)(γ) ∩ δ(...) ≠ ø.

[TODO: The above seems be a case of a limit in a topological space...]

Informally, a backward axiom is such a substitution that from it follows every relevant axiom. [TODO: Define the word "relevant" and make it a formal saying, if possible.]

Proposition. For every provable theorem δ∈β(...) which is not a conjunction and a backward axiom α→β exists an old theorem γ such that δ is a result of variable substitution in (α→β)(γ).

Proof. From the proposition about potential theorems.

It is called backward axiom because it forms an axiomatic loop, that is axioms are consequences of theorems. [TODO: Rules of transformation between variants of an axiomatic system using axiomatic loops.]

Remark. Backward axioms make 21st Century Math Method different from axiomatic method, because they are related with analyzing the axiom set as a whole (rather than simply finding consequences from axioms), form axiom loops, and can be regarded as adding new axioms to the axiom set.

[TODO: Consider this: After every backward axiom, all old axioms can be eliminated replacing them with the backward axiom and the theorems from which the axioms follow. I suspect that we should systematically "forget" the axioms replacing them with theorems in some canonical way.]

?? Let's replace in the formal system every (higher level) subexpression matching α by the rule α→β.

The Main Theorem

Theorem. Adding a backward axiom to a formal system, which is not contradictory [clarify] and does not contain any axioms except of the substitution axioms matching to A→B, does not make it contradictory.

Proof [TODO]. Applying the substitution α→β to old theorems can produce only theorems provable without this substitution. (We have proven this above.)

As a substitution α→β is equivalent to the set of substitutions

{ω→β | ω ∈ α(...) ∧ ω does not contain variable symbols}

We will exclude from this set all substitutions which are new expressions. (It can be done by replacing all instances of such symbols.) So, by the substitution rule they do not produce anything except of consequences of old theorems.

The only left to prove is that consequences of old theorems which are substitutions applied to α→β nor to conjunction of α→β with a provable theorem do not produce wrong results. But it is so because α→β is a new expression (and as such has no more sense than a new constant).

Conditional Expressions

Conditional expressions can be written this way: (A ∧ B) ∨ (¬A ∧ C). The trick here is that (in assumption of classical logic axioms) it will be equal to B or C dependently on A being 0 or 1 even if B and C are not boolean expressions.

[TODO: Write the proof.]

Having conditional expressions we can write an equality definition like (f X) = (((cX) ∧ (g X)) ∨ (¬(cX) ∧ (h X))).

Remark. This definition can be used instead of the axiom x∃(g(x)∨h(x)) ⇔ x∃g(x) ∨ x∃h(x) of the classical predicate logic. This makes quantifiers not necessary in our formal system. [TODO: Detailed method how to transform any predicate formula into a sequence of expressions in our formal system and how to transform any proof in the classical predicate logic into a proof in 21th Century Math Method.]

Using the Formal System for Math Research

21 Century Math Method

21 Century Math Method is a more advanced replacement of axiomatic method.

The following is the current version of the method (how to use the formal system described in this article for mathematical research):

1. Write a set of axioms (that is any universal algebra), if the axioms contain quantifiers you must [TODO] to eliminate quantifiers from the axiom system.

2. Reasonably split the set of all math symbols used in the axiom system into classes of different symbols (e.g. different classes of symbols for points, vectors, sets, and functions).

3. For every group of symbols introduce a new constant symbol t (type mark) which will specify a class of symbols, and in the axioms replace every subexpression α of this class with (t α). Note that you should mark every (significant) subexpression, not only variable and constant symbols (not only leaf nodes of an expression but also its complex subexpressions).

4. Study the properties of the formal system by writing:

• theorems;

• equality definitions;

• backward axioms of the form p→q where p and q are type marks. (Currently I suggest to write backward axioms every time when you reasonably could do this. However now even I myself do not have big experience in 21 Century Math Method and cannot tell how to do it in a good way. I also do not yet know whether we should limit ourselves only to backward axioms whose left and right parts are simple constants or should use also more complex backward axioms.)

Remark. With the conventional math notation accents (such as arrows over vectors) or special parentheses (e.g. [x], 〈x〉, {x}) can be used as a notation for (t α). An another practically convenient (with modern computer technologies) possibility is to mark different types of subexpressions with different background colors.

Remark. In practice it is often more convenient to imply type marks in formulas than to write them explicitly [TODO: Formalize the concept of implied type mark.]

Classes

[A class is a set of equal expressions denoted by a type mark.]

[TODO]

Examples

Suppose we already have the axioms of natural numbers. Let's define negative numbers.

First, this is an example of an axiom (or theorem) for natural numbers ("natural" is a type mark):

• ((natural A) + (natural B)) = ((natural B) + (natural A)).

We will introduce a new constant symbol "number" to denote both positive and negative numbers.

The following could be a definition because no former expression matched the pattern ((number X) + (whole Y)) (as we use the constant "number" the first time):

• (number (- (whole A))) + (whole A) = 0

After a little further analysis we could write the backward axiom:

• (number (whole X)) → (whole X)

[TODO: Write this example in details.]

Postface

Further Research Plans

Completeness Conjectures

Conjecture. Any true expression can be proved. (I'm not sure whether the Godel theorems are applicable to 21 Century Math Method because the set of inference rules is not fixed. We need to look into the exact formulation of the Godel's theorems to check whether they require a fixed set of inference rules.)

A more strong conjecture:

Conjecture. Every expression which does not contradict to the classic logic and main axioms can be written as a theorem in 21MM formal system.

Other

The History of Discovery of 21MM

The Problem with Axiomatic Method and Principle of Simplicity

[TODO]  

Following the principle of infinite development as contained in the Christian concept of children of God (to which I believe to pertain myself), I found that the main principle of my thinking which was axiomatic method is a wrong path leading away from God to void infinite decrease of perfection, I believed in existence of an other better method which can be the next stage of development of thinking.

I mean that if we limit ourselves only to simple axioms systems, then generalizing axioms system following axiomatic method, we necessarily will go by circles due a limited number of simple axioms. Alternatively we go to the more and more complex systems that is to the direct opposite to the stated purpose of axiomatic method that is writing math in simple axioms systems. So axiomatic method is a dead end.

These thoughts were called when I (probably) rediscovered real numbers giving them an AGT-based (see below) definition and realized that I'm going to make a big circle possibly returning back to old pre axiomatic method math that is to study of real numbers.

I set before myself to find a method which does not leads to going by circles being limited by the principle of simplicity. I'm not yet sure whether 21MM is such a method but anyway it is a step forward in math.    

Algebraic General Topology

I found a way to write certain general topology statements as equations and called this new field of math Algebraic General Topology™. It is yet unpublished.

I generalized and wrote algebraically some of general topology structures but later I thought that it is of limited usefulness for practical tasks as we had no general way to rewrite a problem from math analysis in the form of AGT™ equations where it is simply solvable, nor a way to extend AGT further except of using intuition.

So I started to think about an algorithm which would transform math analysis theorems into AGT equations and more generally to transform traditional math into quantifiers-free math. 21MM provides us with an algorithm to free ourselves from quantifiers. That is I searched for a way back from old less general theories to new theories. (BTW, it would be a kind of formalization of History of Mathematics, a self-teaching algorithm.)

Historically 21MM was constructed to be a formal system where it is possible to write certain basic definitions of Algebraic General Topology.

Before invention of 21MM I developed AGT in axiomatic method which appeared to be inappropriate for this new theory as in axiomatic method it appears hard (or impossible) to write the most general cases of AGT axioms and the systems of axioms appear to be somehow antinatural and hard to catch in mind for some people. (I thought about these general cases long time and was unable to fix such a system in axiomatic method.) So I'm going to re-develop AGT in 21MM possibly extending 21MM by the way as needed.

Extension-Definition Method, an Old Version

References

21st Century Math Method

Misc Math Logic