21 Century Math Method - a Replacement of Axiomatic Method.
Part 2: Patterns of Usage and Examples

Preface

[This second part of the article, ulike the first part, is a complete mess, being a rough draft.]

Important Axioms, Theorems, and Definitional Constructs

[This chapter is a very mess in this draft version!]

This section describes several useful constructs and theorems, which are somehow more concerned with features and usage of our formalism itself rather than with particular math applications.

By analogy with an operating system or a programming language these constructs may be called "system" theorems and definitions as apposed to mathematical applications. (There are however no exact border between system and application definitions and theorems, for example a definition of natural numbers can be considered either as system or as an application definition.)

Values and Classes

Values and classes are defined by the axioms:

• value ∈ class ⇒ value → classvalue;

• classvalue → value.

Remark. It is similar to subclassing with adding additional data fields in object oriented programming languages.

Remark. Classes (represented by "class") are to be thought as a kinda extensible sets (sets to which new elements may be possibly added). [TODO: Formalize and attempt to prove: semantics of classes is extensible sets.]

[TODO: Could we also add the axiom (class → value)?]

Variables

Variables are defined by the substitution (var → value) (a variable can be replaced with a value).

Additionally we will accept the axiom (var → class).

This allows to define x as a variable: x ∈ var. Then we can use variables like this: realx + realy = realy + realx.

Using following axioms we can arbitrarily rename variables in formulas:

• name → name1

• name → name2

• varname1 name2 → varname2

Note that varname2 → varname1 name2 is a theorem by specialization rule.

Using this we add to a variable a new name modifier and then remove then old one.

Remark. Oh, well, it is similar to renaming a city: it receives a new name temporarily preserving the old one, and afterwards the old name is removed.

Humor. How the teachers teached us to substitute variables in the low school? We were writing new names near old ones, an only after this in the second stage we erases old names from the desk, like this: a+b → ac+bd →  ac+bd → c+d. Now we know that it was the right approach, the super technology of 21st century with object oriented variables...

Preaching. Now I understand what means biblical "Lord is our teacher" [TODO: Check exactness of the quote.] Our teacher teached rightly, only we were not teached this... (A man who teached us was not only teacher, he was many other things also, but who is the exactly one who teaches in a teacher is the Lord, we are teached by presence of the Lord, the teacher, in a teacher, that is the invariant teacher in different teachers.)

Definite Expressions. Symmetric Equality

The substitution operation → is not symmetric:

Example. One could write (whole → real) meaning that a whole number is a real number, but the reverse would be wrong.

We will introduce the special class (denoted by type mark "definite") of objects for which substitution is symmetric.

For this type mark we will introduce the following axiom: [TODO: Define "definite" using definitional constructs instead of using axioms]

• definite → class;

• value → definite ⇒ definite → value.

As a consequence: value ∈ definite ⇒ value → definitevalue ∧ definitevalue → value

Remark. The type mark "definite" serves to denote definite objects (e.g. the number (1+2) having the definite value 3) as opposed to indefinite objects which may be undefined (e.g. (positive A) could be not definite because it does not make sense for A=-1).

Remark. The constant symbol "definite" is somehow similar to the definite article "the" in English.

Then we can define some type marks to be declarations 8 → value, 8 ∈ definite.

After this we could write constructs such as (in supposition that (number z) is a new expression):

1. Z → 8 (an analogy)

2. Z → definite8 (a theorem using substitution rules)

3. definite8 → Z

4. 8 → Z

So in this case the operation → is symmetric. Also we can prove that Z → Z and 8 → 8, that is in our case it is also reflexive.

We can consider → to mean equality (commonly denoted as "=") in this case. [TODO: Formally introduce equality symbol using definitional constructs.]

So Z → 8 was in fact an equality definition. We defined Z to be equal to 8.

Self Identity

Self equality is defined by the axiom (self_equal → self_equal).

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

Most "normal" classes are derived from self_equal, as in this example: (number → self_equal).

We as well can operate with not self-equal classes. E.g., (changing ≠ changing) may be an axiom (the changing from the left part of the formula has changed until we readed the right part), but is (God = God) a theorem for properly defined "God"?

Substitution Axioms

Let A ∈ var, B ∈ var, C ∈ var.

I call the following the main substitution axiom: (A→B)∧(B→C) ⇒ (A→C)

These axioms are not contradictory (nor to the base formalism, 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.]

Boolean Expressions

With boolean expressions we have two choices, illustrated with the below examples:

We can write boolean logic axioms like this:

• X → boolean, Y → boolean, Z → boolean;

• X ∨ Y = Y ∨ X;

• etc.

We optionally can also add the axiom (var → boolean) which would essentially make all values boolean (but not necessarily definite).

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.]

[TODO: Correct this for the new variant of the formalism without equality definitions]

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 formalism. [TODO: Detailed method how to transform any predicate formula into a sequence of expressions in our formalism and how to transform any proof in the classical predicate logic into a proof in 21th Century Math Method.]

Using our Formalism for Mathematical Research

21 Century Math Method

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

Remark. 21MM is not a variant of axiomatic method because axiomatic method does not contain formal generalizations nor analogys. Combining formal generalizations and analogys we can get certain principally new things missing in axiomatic method. [TODO: More with examples.] Surely, these constructs are indeed have been used by mathematicians working with axiomatic method, but in a non-systematic way. 21MM is a systematic method of using these constructs in addition of some common constructs from axiomatic and pre-axiomatic mathematics. 21MM was developed with the purpose to replace axiomatic method rather than just to ammend to it.

Examples

[FIXME]

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

References

21st Century Math Method

Misc Math Logic

Legal

This article is licensed under the same conditions as the Part 1 ("The Formalism"), as it would be its part.