My homepage | My math page | My math news | Donate for the research
This article describes the overall concept of future post-axiomatic mathematics, which should replace modern axiomatic mathematics in 21 century. See below for references.
Topic: math logic, mathematical logic, foundations of mathematics, mathematics foundations, math foundations, future of mathematics.
This is a draft. The order of exposition is somehow disordered.
Before 20 century mathematics was disordered. It was simply a set of
different theorems related with each other by the relation of
logical consequences. There were known no systematic structure of
mathematics, an other structural
relation between theorems except of
logical consequence.
Well, the concept of an axiom and of a system of axioms is known even from the time of ancient Greek mathematician Euclid, who formulated a system (with mistakes, BTW) of geometric axioms and has proved some theorems which are consequences of that system of axioms.
But only at about the end of 19 or the beginning of 20 century, there was
established modern axiomatic method (also known as modern mathematics
,
which is however is already coming to the past of the mathematics with
appearance of articles like this).
Probably the main achievement of mathematicians of 20 century was that they have reformulated older pre-axiomatic mathematics in new axiomatic form. (However even now not all pre-20 century mathematics is rewritten in axiomatic form.)
The 20 century axiomatic method is the following principles:
Certainly it is not so simple as is described in the items list above. Mathematicians also studied relations of different axiomatic systems between each other in different ways etc. (So appeared classifications of algebraic systems, category theory etc.)
And surely, in 20 century were also many other trends not only axiomatic method. Notable trends of 20 century mathematics were universal algebra, category theory etc. But even in these trends the above mentioned principles of axiomatic method were used as the foundation. For example, universal algebra can be considered as axiomatic method with additional limitations.
Indeed axiomatic method was remaining the main foundation of mathematics of 20 century. As far as I know in 20 century there were no significant mathematical work which was not founded through all its trend on axiomatic method (not counting pre-axiomatic works).
Axiomatic method has become for many people (including myself in the past) the only way of thinking, as if there would be not possible existence of other methods. We were more or less consciously thinking that axiomatic method and mathematics is the same, that all mathematics is axiomatic method and were not even imagining mathematics without axiomatic method.
Probably the only significant exception of the above paragraph was some specialized automated reasoning algorithms for solving some specialized problems and some graphical methods. If I am not right in this paragraph, please correct me; but as far as I know in 20 century were no non-axiomatic mathematics (not counting continuations of pre-axiomatic research of former centuries).
A theorem from algorithms theory states that there are no algorithm which solves all mathematical problems. So if we want a computer to solve any mathematical problem, the only way to do this is to change the program of the computer over time.
Axiomatic method is defined vaguely (axiomatic method
is a
philosophical term about mathematics, but not an exact mathematical term).
As such how we can say anything precise about axiomatic method?
We indeed can say some exact things about axiomatic method by speaking about common properties of different methods. For example, we can make precise statements about all mathematical methods.
Let us model ourselves (mathematicians) as computers acting by a certain algorithm. (Here is not a place to speak whether it is really so, but it is just a model anyway.) In this case axiomatic method in such the extent as we use it is a part of this algorithm.
A thing we want to do (if we are called mathematicians not mistakenly) is to change our algorithm because otherwise there exists some problem we would never solve. To change an algorithm we may replace some its part.
One of the variants is to replace with something other the axiomatic method. That is we are to lay aside axiomatic method and to not use it anymore (but to use something other in its place).
Now I will make an informal statement, which I think indeed can be
formalized; accordingly my guess that conjecture will be proved true:
If a problem solving algorithms is infinitely modified extending the
set of problems it can solve, so that it solves any problem, then any
old part of this algorithms at some stage becomes superfluous
(not usefully used anymore), that is any part of it goes to the past.
If the above informal conjecture is to be considered true, then at some stage axiomatic method (that it part which we considered as a part of our algorithms) should go to the past.
We modeled the informal concept of axiomatic method as a part of some formal algorithm. Because it is considered as only a model, then like in outside of mathematics (physics etc.) arises the issue not only of whether the model is correct (non-contradictory), but also of whether it is actual (applicable to our real situation, as it is today).
Then the issue is only when to do away with axiomatic method.
As I demonstrate, the issue of axiomatic method passing away from our
mathematical research became very actual in this time, as I demonstrate
you an alternate method, which seems for me better than axiomatic method
by every criterion of comparison of quality
of methods which
I know; and at the same time we have the real possibility to rework all
known mathematics in new methods (including the mean of automatic
converting math formulas to new formats by computers).
In the past mathematics have been researching formulas (or rather to say our mathematics knowledge have been consisting of formulas). On the next level mathematics will research relations between formulas and functions on sets of formulas.
Former mathematics essentially consisted of a set of theorems to which we add new theorems. (Surely there have been trends of different more sophisticated structuring mathematics, but probably all of us continued to consider mathematics as a set of theorems, not switched to a different concept completely.)
The post-axiomatic mathematics will be instead consisting of a set of functions or relations on sets of formulas, to which we add new functions of relations. Definitely these indeed can be formulated in the terms of theorems (see below about substitutions), but in fundamental post-axiomatic mathematics theorems cease to be actual being replaced by becoming more actual concept of transformations of formulas.
We can call this (post-axiomatic) functional (or relational) logic or (post-axiomatic) relational method.
But functional method is only practically useful if we can relate it with the rest of mathematics. A class of functions which is significantly and actually related with all known mathematics are substitutions (A->B). Substitution A->B is a formula which expresses that a subexpression matching the pattern A can be replaced by corresponding value B in formulas.
A well known example of a substitution is (A+B)^2 -> A^2+2AB+B^2 from school algebra.
So a substitution is a relation on a set of formulas. Substitutions is the bridge which connects the world of formulas with the world of relations and functions on the sets of formulas. Namely through this bridge we now can start to move from old mathematics to new post-axiomatic mathematics.
Substitutions are meta-formulas
, formulas expressing relations
between formulas.
Substitutions are not only inherently related with known mathematics but also are well understood intuitively so that we can think and even feel in the terms of substitutions, we people can comprehend the sense of substitutions (not only write formal algebraic formulas with substitutions). This makes the future post-axiomatic mathematics possible for understanding, comprehending, and so developing by us.
In post-axiomatic method we are concentrated on functions on formulas rather than on formulas themselves. So only these formulas which express functions on formulas will remain actual for fundamental mathematics. In practice this may mean that only these formulas which are substitutions will be essential.
As seen from the above for successful development of post-axiomatic mathematics there is needed a theory of formulas.
The answer to this need is my Axiomatic Theory of Formulas (online text) which would be a classical example of an axiomatic theory if it would be not a new theory. (Note that this theory describes not only formulas but also anything what has indexed parts; infinite formulas are also included in the domain of this theory.)
(Boasting) I'd say that this theory supplements the group theory as the second elementary fundamental theory for a foundation of mathematics. (Group theory researches well-organized structures, while the theory of formulas studies messy things.)
Relationization
Certainly relations between formulas are themselves expressed as formulas in mathematics. The issue arises: Could we move even further in this direction and research relations between relations of formulas? The current answer on this issue is that the researched relations between formulas do include relations between formulas expressing relations between formulas. (We can write formulas expressing relations between formulas such as substitution, see below, in our formalistic.) So at the current stage, we do not move further in this direction. We will need to move further when will find these actual (significant, essential) relations which are not expressible in our formalistic.
Personally I have come to the idea of post-axiomatic mathematics through intensive use of definitions and initially formulated ideas of post-axiomatic mathematics in the form of a definitional method. (I use definitions extensively in my Algebraic General Topology research.)
It seems true that post-axiomatic mathematics and a purely definitional
method (by purely
I mean not axiomatic based
) are the same thing
(for the case of finite formulas, see here
about a theory of infinite formulas).
How definitions are related with the above?
A definition can be defined as adding a new term or symbol (or a combination of several terms or symbols) which introduces a new logical formula. A definition must be valid, that is to not contradict to the previous logical formulas.
In the simplest case validity of a definition is checked by ensuring that the new term or symbol is not encountered in any of the previous logical formulas. From this simple case is seen that checking validity of a definition involves all previous logical formulas unlike checking a logical consequence of former formulas (a logical theorem) to check validity of which it is enough to process only one to two previous formulas whose consequence it is.
The need to introduce the concept of a function arises when we consider multiple values. In the simplest case of a relation of a few variables, it may be unneeded to introduce functions into our consideration. For example, to solve this equation a-2a+3b = 2b we do not need to introduce functions f(x,y) = x-2x+3y and g(x,y) = 2y and rewrite the equation in the form f(x,y)=g(x,y).
Likewise there were no strict necessity to introduce functions on the sets of formulas to study traditional math logic consisting of simple logical consequences and no research of definitions.
As every definition is inherently related with many previously written logical formulas, to study definitions the need to introduce some functions on the set of formulas arises.
So, functional logic may be considered as a way to study definitional logic.
When we associate a relation on the set of formulas with each definition, as in the case of definitions which take the form of substitutions (A->B), these two (definitional logic and functional logic) become equivalent.
So post-axiomatic mathematics can be considered as either functional logic or as definitional logic, with functional logic being more abstract than concrete definitional logic.
What I call 21 Century Math Method (21MM) is a kind of a Cartesian product of abstract algebra and specific definitions taking the form of substitutions, a concrete form of post-axiomatic method. An other characteristic of 21MM is that it does not use quantifiers, as these became unneeded being replaced with definitions.
I consider quantifiers a harmful thing for mathematical research (and even for the most aspects of teaching mathematics) as they only mess the mind of a student with too complex formulas. So quantifiers should be eliminated. In 21MM they are eliminated so that all mathematics can be rewritten without quantifiers. (Quantifiers indeed may be useful in specific areas, some particular applications, and engineering like the rest of old mathematics which by the time slowly or quickly passes away from the fundamental science.)
So, in the definitional form of post axiomatic method all important theorems may take the form of substitutions (or equations which can be considered as two reverse substitutions A=B is essentially the same as A->B and B->A). The rest theorems (not substitutions) are supplementary. BTW, this can be a formalization of the informal notion of distinction between propositions (simple theorems) and theorems themselves (more complex); theorems which are not substitutions may be called propositions (in certain logical frameworks).
So writing mathematics in new format, we in fact write algorithms which solve mathematical problems. (I recall that every algorithm can be written as an (ordered) set of substitutions.) When this is formalized we write software. So mathematics and programming coincided in the post axiomatic world.
Post-axiomatic mathematics will be related to the older math as an algorithm related to problems it solves.
Older mathematics was hardly formalizable in practice. But with appearance of 21MM formalization of mathematics becomes quite straight-forward. The future mathematics will be written in formal, computer processable form. Mathematical journals in current form will pass away being replaced by automated electronic repositories of formal knowledge.
Former mathematics also sometimes used algorithms to formulate or to solve problems. The difference is that post axiomatic mathematics will essentially use algorithms everywhere, will consist of algorithms. Former mathematics almost always used algorithms rudely, in an anti-natural way. In post-axiomatic mathematics algorithms will be naturally integrated in the essential structures of the mathematics.
As the reader should understand himself, we do not lose connection with axiomatic method at all and we will indeed have systems of axioms. But what I'm going to do is to do away with axiomatic method by fixing one certain set of axioms (namely rules of inference of a formal system such as 21MM) and using exclusively that system of axioms.
Further development will be in the direction of defining new concepts (inside the formalistic of the formal system) and proving theorems about defined concepts.
The above in short: Now we can and should develop formal post-axiomatic mathematics. In my opinion the main trend of the development of mathematics in 21 century will be complete refuse of axiomatic method in fundamental research.
One more issue: The purpose of axiomatic method was to simplify and generalize mathematics as much as possible. How to formulate the purpose of post-axiomatic methods (such as 21MM)?
Author: Victor Porton - www.mathematics21.org
My homepage | My math page | My math news | Donate for the research