My homepage | My math page | My math news | Donate for the research

This is an old draft. See new version instead.

Introduction to Extension-Definition Method,
the Next Math Method after Axiomatic Method

Victor Porton

[[TODO: ToC]]

WARNING: This is a VERY DRAFT with MANY mistakes and COMPLETE DISORDER. Please comment and suggest how to make it better.

[[How to name it: Extension-Definition^TM method or Definitive Method^TM?]]

Note that this text contains some problems for readers. If you'll solve these and write detailed solutions, please send me the solutions to be included in the next edition of this text.

Overview

Axiomatic method was a new method of 20nd century math. In this articles I describe a new method recently found by me which is expected to become the 21st century math method^TM. It is a definitional method like back to the time of Socrates.

The essence of EDM^TM is writing a system of logical (that is without quantifiers and set theory) axioms (normally we need to check that the system of axioms is non-contradictory) and then extending it by adding additional axioms (also in pure logic without quantifiers and set theory).

When adding axioms, one need to ensure that these do not contradict to already present axioms. New axioms are normally added introducing one new concept (that is a new functional or relational symbol). So adding new axioms are definitions of new symbols.

Notwithstanding of that we do not use quantifiers (EDM does not use quantifiers at all.), we can have different kinds of symbols for systems of axioms. We also can introduce new kinds of symbols when adding new axioms/definitions. If we find that a kind of symbols fits to all axioms for an other kind of symbols, we can declare these kinds of symbols equal.

Comparison with Traditional Math

The things expressed in traditional math by quantifiers can be expressed in EDM by defining new concepts. (A definition correspond to the existence quantifier as we must accompany a definition with proof of non-contradictory).

Not likely to traditional math, EDM doesn't use nor logics of predicates nor set theory. (However set theories can be expressed as extensions of a systems of axioms in EDM.) This may have philosophical implication that the World may be something not set theoretic.

Any theorem proof in the formal system of logics of predicates can be easily rewritten in EDM (a problem for the reader to find an algorithm.)

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

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

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

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

Formal system of EDM

Symbols

Logical symbols

OR, and, NOT, implies, LEQUAL (some symbols can be excluded, see any math logics studybook).

Equality

= (note that ≠ is not a primary symbol, this is importain for correctness of definitions, see below).

Classes (used to represent kinds of defined symbols)

CLASS (class of classes), IS (like subset relation)

Constants (used to denote constants, functions, relations)

small letters, digits 0-9, +, -, / etc.

Variables (can be substituted)

capital letters

Note that to have an infinite set of symbols, I may use constants and variables names of several letters, e.g. natural, GAMMA. Furtherly the conventional math symbols may be used instead for clarity, which kind of symbols it is should be clear from context).

Expressions

Expressions are either symbols or finite sequences of subexpressions. (Every expression contains a finite number of symbols.)

Example: arithmetic expression a+bc from traditional math may be formalized as the following sequence (a, +, (b, *, c)). Furtherly I will skip commas and outward parentheses, so this expression is written as a+(b*c).

This form of expressions does not differenciate between functional and other symbols. This is useful to use complex expressions (not only symbols) as functions or relations. Example of a complex expression as a function name: (f^2)x=f(fx).

Also we are free to use either traditional (a+b), prefix (+ab) or postfix (ab+) notation. This doesn't matter as the order of parts of expression is choosen arbitrarily by a human.

The following rule applies to all situations except of in left parts of definitions: no (sub)expression must be of an undefined class. Furtherly this rule will be applied implicitly. (For primary symbols some class is implied.)

The expression CX, where C is an expression denoting a class and X is any expression is conventionally used to denote that X belongs to the class C. (Alternatively one could use the notation X in C (that is the sequence (X, in, C)) like traditional math, but our notation is more concise.

Every variable must be declared to be of some class before being used.

Definition: class A matches class B iff there was written a statement to which expression A is B matches.

Definition: expression A matches expression B iff every B can be transformed into A by replacing variable with subexpressions of matching classes or other variable symbols of matching classes.

Note that in this article I follow the convention to write expression denoting the value of function F at the point X in this form: FX; relations may be written like so: a=b or so: Rab.

Axioms systems

[[TODO: can't the concept of an axiom be excluded entirely replacing these with definitions? The complexity is that we need to ensure that every non-contradictory axioms system can be written.]]

An axioms system is a finite sequence of expressions conforming to these rules:

• for every variable or constant symbol used there are exactly one definition of it being belonging to a class that is an expression of the form CX where C is defined to be a class (by expression CLASS C which also must be present in the axioms system);
• being non-contradictory accordingly to the traditional boolean logic and properties of equality (that is the axioms A=A, A=B LEQUAL B=A, (A=B and B=C) implies A=C are added implicitly).

Additionally implicitly add axioms C is C, (A is B and B is C) implies A is C?

Note that quantifiers must be not used in axioms. (They really cannot as we don't have the notion of bound variables.)

[[TODO: it seems that the rule of classifying every symbol can be excluded. One could write X of C every time in an expression to denote that X is to be considered as a value of class C.]]

Kinds of Expressions

Any expression matching any subexpression of an axiom or the expression at the left side of a previously written definition is called an old expression, all other expressions are called new.

New expressions must be used nowhere except of the special places in definitions as explicitly described below.

The system

Our formal system is a (finite) sequence of:

1. axioms system;
2. any number of theorems, definitions, or class equivalences in any order (provided that these are correct).

Theorems

A theorem is any logical expression. Correct theorem is either:

• a theorem which is a logical consequence (that is a consequence in the traditional boolean logic) of previously written axioms, definitions, and theorems (taking into account only properties of boolean operations, but not properties of equality);
• a result of substitution of a subexpression X in a previosly written axiom, definition, or theorem with some expression Y provided that we have previously written axiom, definition, or theorem of the form X=Y, probably written in other symbols but of the same (or denoted equivalent) symbol classes.
• a result a previously written axiom, definition, or theorem some user symbol with a matching expression.

Note that the above implies that a correct theorem is always written only in previously defined symbols.

Definitions

Definitions are the heart of EDM.

There are several kinds of definitions:

Equality Definitions

[[TODO: Can't equality definitions be excluded?]]

def X = Y, where X is a symbol and Y is an expression (with only already defined symbols).

Equality definition adds X = Y to the list of the axioms.

Equality definition declares X to be of the same class as Y.

Equality definition is correct iff X is a new expression and doesn't contain any logical symbols??

Slot Definitions

X: C def R(X)

Correctness requirements:

• statement to which CLASS C matches was written previously;
• X is a new expression;
• R(X) isn't a part of an axiom (or right-side of a prior slot definiton) written in disjunctive normal form (taking in account that equality is symmetric and not counting expressions of the form A=A which normally should be not present in axioms) [[Shouldn't we add the rule: always write axioms systems in disjunctive normal form?]]
• R must contain X as a subexpression;
• R must be of the form R = A0 or A1 or ... or An or not(B0) or not(B1) or ... or not(Bn), where Ai, Bi do not contain logical operations nor directly nor indirectly through equality definitions containing logical operations. [[indirectly through equality definitions are very crude words, how to do this without a curse? Also it seems that we can allow not]]

X is defined to be of class C. R(X) is added to the list of axioms.

Lemma: From a disunctive normal form follows nothing non-trivial (not containing this form) without adding new symbols even if we take in account properties of equality.

Proof: We already have taken into account that equality is symmetric. So the only axioms of equality left are: A=A, (A=B and B=C) implies A=C. A=A is excluded as said above. All what can follow from the second axiom A≠C |- A≠B or B≠C, that is this adds new symbol B.

Lemma: from R doesn't follow any non-trivial (like A=A) old expression (where by old understood before this definition).

Proof: R does not match any part of an axiom from the old system. So, no logical consequence rule can be applied to R, except of trivial consequences. But of R has no trivial consequences not containing R (as a dijunctive normal form).

Main lemma: Adding right part of a correct slot definitions to an axioms system does not make it contradictory.

Proof: Assign to new symbols and to X some values distinct from all other values. Assign every expression with X some distinct value. Let E be the set of old expressions. Define the set T (of true expressions) by induction:

• any expression mathing old axioms;
• R(X);
• any consequence thereof (taking in account properties of equality);

As follows from the lemma, (T inters E) is exactly the set of the consequences of old axioms which can be written in old expressions. So, we have extended the boolean logic of true expressions.

The only thing left to prove is that the logic T does not contradict with properties of equality with X, which is imposible because nothing is known about X except of that X was not encountered in the axioms and that X is distinct from all other relevant values.

Example: (-x): number def (((-x)+x)=0)

• Because - is a new symbol, (-x) is a new expression.
• Analogously ((-x)+x)=0 doesn't match any previous subexpressions.
• and ((-x)+x)=0 doesn't match any logical theorem nor a theorem about equality.

So it is a correct definition.

Math Induction [[Move this to an appendix as it is non-normative]]

We can deal with math induction this way: Let induct be a constant symbol.

Add axioms [[TODO: they should be some way implicit]]:

• CLASS(F induct Z);
• (F induct Z)Z
• ((F induct Z)X) implies ((F induct Z)(FX))
• (DZ and (DX implies DFX)) implies (D is (F induct Z))

Example: axioms of natural numbers ([[are these all axioms?]]):

natural 0, (inc induct 0)natural, (inc X)>X, (A>B) implies (A≠B), (A>B) implies not(B>A).

The Main EDM Theorem

Theorem: adding a correct definition to a system of axioms doesn't make it contradictory.

Proof: For slot definitions it was already proven. For the rest it is obvious??

Class Equivalences

A class equivalence is a statement of the form C is D.

A correct class equivalence is such class equivalence that for every already written axiom or definition containing a variable from C, there was already written axiom, definition, or theorem resulting from substituting it with a variable from D.

What to do with constants? (The simplest way is to disallow constants of C before C is D declaration at all. The more hard way is to introduce definitions of homomorphisms.)

After a class equivalence definition every theorem containing a symbol from C is (implicitly) duplicated with a symbol from D.

Example of an Axiomatic System

This example defines axiomatic system for strict partial order:

order, rels in class;
A, B, C in order; < in rels;
not(A < A); not(A < B and B < A); A < B and B < C implies A < C.

Possible Plans for Future Research

• algorithms and software for EDM (I'm going to use Ada95 programming language):
  • algorithms of simplifications of equations in EDM;
  • EDM based automatic provers of 2nd-predicates theorems;
• theory of relations between axiomatic systems and classification of axiomatic systems (Isn't it already developed? Isn't so the entire math concluded in something like group theory?);
• variations of set theory in EDM, possible corresponding relations of EDM with traditional axiomatic method, whether the old axiomatic method preserves its scientific value after discovery of EDM;
• philosophy of EDM, particularly regarding the principle of simplicity;
• effective reformalizing known math in EDM (see also about Algebraic General Topology below);
• algorithmical methods for effective reformalizing known math in EDM;
• a map of of all published math knowledge formalized in EDM, studying the properties of the map and its development;
• about fullness of systems of axioms;
• about partial definitions (e.g. X is a real number) with later concretization (e.g. X=5);
• adding operations on classes (such as intersection or union);
• isn't math splitted into three separate sciences: formal algebra, theory of definitions, and theory of math induction? how these relate with each other?
• EDM in pedagogy;
• the next math method?

The History of Discovery of EDM

The Problem with Axiomatic Method and Principle of Simplicity

My Religious Thoughts

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 necesarily 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 EDM 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^TM. 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^TM equations where it is simply solvable, nor a way to extend AGT furtherly 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. EDM 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 Math.)

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

Before invention of EDM 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 EDM possibly extending EDM by the way as needed.

My homepage | My math page | My math news | Donate for the research