My homepage | My math page | My math news | Donate for the research
This article is my own informal philosophical chatting around my formal math research.
This online article by Victor Porton introduces Axiomatic Theory of Formulas (abbreviated ATF, which can be also instead deciphered Algebraic Theory of Formulas).
Like in a humor story about a professor who searched for his glasses long time, and discovered them on his own nose... Mathematicians studied anything but not formulas; algebraic theory of formulas was discovered only in 2005 year. (The analogy is that formulas are like glasses through which mathematicians see, but the glasses themselves were unseen.)
The reason that we have been not discovered it long time ago is our laziness. We was laying aside this issue during centuries hasting to reach a more immediate result with concrete formulas. I myself many times before was thinking about developing an axiomatic theory of formulas, but have been laying this problem aside... until 2005 year.
The main skill of a mathematician is to choose which problems to solve, that is which problems to solve first and which to solve afterwards. (One who knows which problem to solve first and which afterwards can solve any mathematical problem, but we do not know what to solve first.) In this the opposite of a talent was more laziness rather than stupidity. Remove laziness (understood as an irrational desire to lay aside a problem for the future), and a common man would become a genius.
Oh, well, laziness in some issue may be a result of too much efforts
invested
into an other issue. So that is a talent? It is the
ability to invest in a good way. But what is the ability to choose
good investitions? It is a talent. Talent is a victory over laziness,
victory over laziness is a talent.
So what it was a so long time stagnation (unseen glasses
)
in math research, laziness
or stupidity? It is relative, it depends on the viewpoint.
Oh, if you are a causal reader (not a mathematician) and laugh over mathematicians, then think that you yourself also was too lazy to discover formulas theory. Was a big talent needed? I'd say no, just to overcome laziness.
A system of formulas is defined as the system (E, X, Z, Y):
It is essentially equivalent to an abstract algebra (with possibly infinite set of operations) with only unary and nullary operations, namely:
When we exclude Y we get so called system of constructs (E, X, Z). A system of constructs is essentially an universal algebra which has only unary operations (X) and nullary operations (Z).
But except of the case when X contains the identity operation, this is almost obviously equivalent to a semigroup:
So from the viewpoint of universal algebra, the theory of formulas is a case of either algebras with only unary and nullary operations or of semigroups.
So, in its initial variant, ATF is essentially an universal algebra.
It is quite clear that universal algebra is useful for ATF research. (Enough to note that I used the concept of homomorphism from universal algebra as one of the most important concepts in ATF.)
Can ATF be reversely useful of universal algebra research? This question has two different aspects:
Doubtlessly that fact that algebraic equations are formulas will lead to some usages of ATF in algebraic research.
Specifically, any algebraic element, which is a solution of some algebraic equation, corresponds to a formula. So modeling of elements of an algebra can be reduced to modeling finite formulas. Here formulas theory may be useful.
Every algebra can be split into closed subalgebras every element of which is a solution of some algebraic equation. [TODO: Check that this statement is true.] So any algebra can be represented as an union of systems of formulas. But an union of systems of formulas is also a system of formulas. So any algebra can be represented as a system of formulas.
As seen from the above systems of formulas (and systems of constructs) are algebras with only unary and nullary operations with the additional requirement that functions preserve certain sets (the set of null formulas Z, and the set of constant symbols Y).
These particular cases seem to be important cases of universal algebra to which other algebras can be reduces. So research of the theory of formulas seems to be useful for development of universal algebra itself.
See also this news message about algebra of operators (functions) on the set of formulas (at the time of writing this, this is yet not researched).
At the time of writing this, formulas (in the sense of ATF) are not yet researched from the category theory viewpoint. (There are however a call for paper on this topic in Journal of post-Axiomatic Mathematics and Logic.)
As it was noted above, formulas can be considered from the viewpoints of two different kinds of abstract algebra. This makes evident that universal algebra way is not enough general for study of formulas, and these need to be researched from a more general perspective which may be category theory.
Vice verse the category theory model of formulas is likely to be useful result for the category theory itself, because formulas (as in this article) involve interesting uncommon morphisms (pseudomorphisms). Pseudomorphisms should be formalized and researched from category theory viewpoint, if likewise objects were not yet researched in category theory. Anyway we need to find relations between pseudomorphisms and category theory.
Oh, also one note: Every formulas is a category and every category is a formula... Does it give us any hints in either theory?
I initially developed Axiomatic Theory of Formulas for the needs of mathematical logic (particularly for my research which I call 21 Century Math Method). ATF research was initially intended to simplify proofs of math logic theorems (and now it remains to be the main purpose of ATF research).
The idea behind is quite simple: A propositional formula is a formula in the sense of ATF. So we can research propositional formulas using ATF.
ATF makes math logic modular as with ATF math logic research can be generalized for studying general cases which span around several different representations of formulas. So a system of formulas (e.g. binary trees) can be as a module be replaced with an other system of formulas (e.g. lists of lists).
But probably the main archievement of ATF for math logic that we can research transformations of formulas rather than separate formulas.
Also ATF brings math logic to study of infinite formulas, so that we can analyse principles of infinite theorems. It is yet hard to value which results this may bring. But probably we will be able to directly apply logic to study of infinite mathematical objects (functions, topological spaces etc.) This may help to find complex logical relations between mathematical objects. Maybe in the future this will lead to unifying logic with other fields of mathematics.
Above I have said about a professor which sees through glasses but does not see glasses themselves.
How to not remember here common religious (including Christian) notion of
seeing light
,
as we see with light but are used to not see the light itself.
So we can figurativly say that with theory of formulas
we see light that is formulas themselves
(true light
as it progresses to the math logic research).
This is like to foundations of mathematics. We do mathematical research using foundations of mathematics, doing mathematical research we discover any kinds of mathematical structures, as our research progresses we discover among others these structures which are isomorphic to our foundations, we study isomorphisms between strutures and find which of discovered structures are isomorphic, but we may miss that a particular math structure we study is isomorphic to the foundations of math themselves.
This make math foundations research different from other (common) math research: math foundations research is common math research with additional note that the objects which we study are the foundations.
We separate the entire mathematics into two parts: foundations and the rest. (When we have a more elaborate classifications, we can indeed reduce the classification to this simple dichotomy, as any classification can be represented as multiple dichotomies.) An essential aspect of a mathematical research is the choice whether to bring it to the foundations in the classification or to the rest. A common result in non-foundations may be a great discovery in the foundations (consider e.g. the theory of topological spaces, which would be of no significant value if it would be not laid into foundations of other theories, such as theory of metric spaces).
To lay a theory into the foundations of mathematics means to express the intention to rebuild the rest of mathematics on this theory.
So the following statement can be easily formalized and proved in algorithms theory: correctly choosing what to lay into the foundation on the next step, we could solve any mathematical problem.
Formally, we could classify mathematical research by adding additional boolean tag to every math object, whether it is from foundations or from the rest of mathematics.
One mean to add such tags to mathematical objects is to have different terms for foundational and the rest objects even when these are isomorphic. This distinction arises by itself due we tend to not notice that math objects in consideration are isomorphic to other objects. A thing I'd suggest for formal math research is to develop a certain scientific method for such distinction of foundational and non-foundational terms rather to leave this problem to the fate, as we used to do before.
An adequate formal naming scheme seems to name non-foundational objects
accordingly what's specialization they are, and foundational objects
accordingly what's generalization they are. (I named my systems of
formulas
accordingly this principle as they are a generalization for
the foundational concept of formulas (expressions) from math logic and
computer science, rather than a specialization of some essential non-foundational
matb objects.)
The formal naming scheme however can be introduces only when the entire mathematics will be writen in a formal (computer) notation (which becomes possible using 21 Century Math Method). So now it becomes also actual a formal research of the concept of foundation of mathematics and of related naming schemes (that is we are to come to formalizing of things said in this section).
In my opinion, there are two different criteria for a discovery in foundations and in the rest of math:
(If something is both a new foundation and a generalization, it in principle is to be considered as a composition of two separate discoveries, one in the common math and the other in the foundations, rather as one discovery.)
Discoveries in common mathematics (e.g. a proof of Fermat Last Theorem) are hard to accomplish, discoveries in the foundations are simple to accomplish but hard to find.
(Certainly, the above distinction is vague, as there are no exact criteria what is foundations and what isn't.)
During time it changes what we consider as foundations and what
not, as as we discover new foundations they push out
old
foundations to common mathematics, as foundations should be not too many
(as a requirement for mathematics is to not have too much special
things, but to consider all things as common as much as possible).
The above clearly applies to ATF as formulas are clearly classified as a foundation of mathematics. I insist that ATF shall be laid into the foundations.
BTW, I would split math prizes like Abel Prizen into two separate categories: One for the foundations and other for the rest of mathematics as there are different criteria of a discovery.
(Oh, a Freid's misspelling, in a draft of this text two paragraphs preceding this were reversed...)
As formulas (named there expressions) is a key concept for computer science, the theory of formulas is a key theory there.
Algebraic theory of formulas may lead to algebraization of computer science, becoming a branch of abstract mathematics, and as a result computer systems projected accordingly formal algebraic standards.
Among of ease of development, this may lead to much more modular design of computer systems so that components of different companies will be able to interoperate without coordination and standard organization (planned by God).
As computer programs are formulas, algebraic theory of formulas
can be used for algebraization of programming languages what
will make them modular and interchangeable with each other. We will
be able to easily construct a programming language from a set of modules
(several standards on different aspects of programming) rather than
monolitic
programming languages with a fixed standard as now.
So study of this theory is expected to be a positive factor for economy in the field of information technologies, programming, and other related technologies.
Abstract mathematics and certain fields of computer science exchange their roles, computer science becomes a foundation, and abstract math becomes an application. Isn't it a revolution in mathematics? (The top and the bottom levels interchange their places with each other, as in a revolution.)
These things probably even more apply to 21 Century Math Method than to Axiomatic Theory of Formulas.
As Axiomatic Theory of Formulas
describes not only finite but also infinite formulas, naturally arises
the issue of infinite mathematics
, mathematics with infinite
formulas.
Before we were encountered such things as irrational numbers but as far as I know there were no significant systematic research of infinite formulas in general.
Infinite formulas can be considered as continuation of finite formulas, finite formulas being the top of the unseen iceberg of infinite formulas.
Moreover a finite formula can be considered as a shell
(a covering
) which may be filled with infinite formulas. (How to not remember the
religious notion of flesh which may be filled with spirit.)
Now imagine that we have several infinitely fast computers each of which solves a certain class of problems. For example, one of them would solve any problem from group theory etc.
But now imagine that we want to build a network of these computers. To build a reasonable network we need to know the properties of computers that is how they are related with each other.
To know their properties we need to know such things as group theory and other math. Certainly we would ask the computers. But how we would choose which computer to ask which question? For example to ask the group theory solver about any particular math problem we need to know how to rewrite this problem in group theory form.
So even with infinite computers we would be able to operate only when we ourselves know some mathematics.
There are a fantasy literate story about an answer machine
,
a device which answers any question asked. A clever enough person would
guess to ask it Which question is the best to ask you?
, I think
it would reply Which question is the best to ask you?
So he would
be able to get an answer but unable to get an useful answer. Is it simply
to get a good answer? One could then ask What an other question is
the best to ask?
and it would reply What an other question is
the best to ask?
A more clever person would be able to formulate
a more appropriate question, What is the best question to ask you,
which is unrelated with yourself, the answer machine?
What it would
reply? I don't know.
As much as we know which questions to ask and in which order, mathematics is such an answering machine. But in which order to ask? I suggest to ask the mathematics itself by studying properties of formulas themselves.
We can even assume that we have infinite knowledge in any given
part of mathematics, only are unable to relate this knowledge with
other fields of mathematics. (And this is in fact true as having enough
time we can write any theorem.) These philosophical reasoning indeed
give us a useful idea about classification of mathematics: we can
classify mathematics accordingly assumptions of knowing all in certain
field (in the assumption
that we know all algebra
, in the assumption
that we know all group theory
etc.), I would call these
fields of mathematics anti-algebra, anti- group theory, etc.
But now imagine that we are milliards of years researched group theory and other fields of math that can answer practically any question from group theory etc. Then we ourselves would be like these infinite computers.
To operate with our knowledge (practically or almost infinite formulas) we appear to need finite formulas.
Having infinite knowledge, we would be different from having only finite (mathematical) knowledge by being able to answer any e.g. group theory question.
But development of infinite creatures (consider angels which some religions deem to be infinite) would be at every step identical to development of finite creatures, because infinite knowlegde cannot be futher advanced. (If one knows all group theory, he can't further advance in group theory.)
So, as in essential things such as development an infinite creature
appears identical to a finite creature, any creature (or computer)
can be considered as the top of an infinite creature iceberg
.
The purpose to gain infinite knowledge is unreachable for a finite computer, but in regard of issues related to development of new knowledge (study) it can be considered as already reached infinite knowledge.
In mathematics it is a common thing finding answer to a question,
behave in such a way as if we would already know the answer
(remember the school where you were teached Imagine that you already
know X...
) Now I suggest to consider ourselves as knowing all,
and only needing to interrelate our knowledge. In this way the entire mathematics can be
reworked with infinite formulas.
Some religions teach that considering ourselves in such a way (e.g.
in Christ
accordingly Gospel) we can better advance and develop.
Gospel teaches that we progress accordingly as we consider ourselves
being in Christ.
It is also a reason to deem that the progress of mathematics will be related with research of infinite formulas on highest level of abstraction we can reach.
Traditionally mathematicians considered proofs and solutions based on researching the structure of formulas (formal algebra) unbeautiful. Mathematicians striving for purity of abstract mathematics were opposing to this kind of solutions (especially solutions based on computer calculations), instead insisiting on solutions based on pure abstract mathematics (axiomatic method, abstract algebra etc.) which are based on mentally comprehending a problem rather than only pure formalistic.
This was not without a reason, as the solutions arisen from research of structure of formulas were bad in the sense that these have been hardly generalizable for solving a broader class of problems. Nor these solutions were teaching us giving hint for analogous solutions of other problems.
After discovery of axiomatic theory of formulas this changes. Now we have no reason to dislike solutions based on analysing structure of formulas, because now this analysis itself is based on a general abstract theory.
That is now solutions based on pure formalism seem to become of equal scientific value to other kinds of solutions.
We were afraid of formal algebraic, especially algorithmic theories,
computer thinking
as these may while teaching us to solve a particular problem disteach
us to think (to solve broad classes of problems), focusing our
minds on formal aspects of problems and so distracting us from the
essential nature of things behind.
But now we have an abstract theory behind pure formalism and
mathematical formalism is no more separated from abstract mathematics
and the essential nature of things. In the new system formal solutions
become as beautiful as pure
abstract mathematics solutions.
It seems that difference between formal solutions and solutions based
on smart reasoning just vanishes now.
Theoretical computer science became just a part of abstract mathematics equal with all other parts (such as algebra, general topology, etc.), not just an application as before.
In the above mentioned Axiomatic Theory of Formulas article I introduced the concept of Least Common Specialization (LCS) of two formulas (or more generally two constructs).
There are certain conjecture about LCS which I call Least Common Specialization Problem (LCSP). At the time of writing this LCSP is yet unsolved. (LCSP seems being an important problem for the math logic and theoretical computer science.)
I'm not a specialist in the field of number theory. But I deem that solution of LCSP may may probably help to find a shorter proof of Fermat Last Theorem (FLT), as FLT looks like being a special case of LCSP.
LCSP doesn't look like a very hard problem and
I hope that I will solve LCSP in nearest time, but
I remembered FLT when I was trying to sovle the initial variant
of LCSP (for the particular case of lists of lists), as in that
variant LCSP appeared to be a simply looking but a losing solution
,
producing a mess
problem like FLT.
The above however only increases the hope that solution of LCSP will lead to a shorter proof of FLT. (I deem that important math issues are these issues which are not too hard (so that we could not solve them) and are not too simple (as else something similar is already solved). LCSP looks like just such a problem, and being similar in form with FLT, it is likely to be a bridge to a short proof of FLT.)
Axiomatic Theory of Formulas). Victor Porton.
Author: Victor Porton - www.mathematics21.org
Copyright © 2005 Victor Porton. All right reserved.
My homepage | My math page | My math news | Donate for the research