Six levels of the metaverse of mathematics

When I was little, I thought that mathematics was a very formal science. No matter how! When they talk about us, mathematicians, like crackers, this is a lie! (c) 17 moments of spring.

I invite you on a journey through the 6 levels of the universe of mathematics – from the completely formal to the philosophical and poetic, and at the same time we will answer the question of whether Gödel’s theorem is a theorem or a meta-theorem.

Level 1 – first order logic

Let’s start with dry formal theorems – for example, x(y+z) = xy + xz. This simple expression is an arithmetic (and algebraic) theorem and is easily proved in formal arithmetic. This is the simplest case.

However, things are not so simple if we take, for example, Fermat’s Last Theorem, which can be written formally like this:

Of course you know that Fermat’s last theorem proven. in 1994. However, the methods used in this proof go far beyond formal arithmetic. That is, the theorem itself is arithmetic, but the proof is not. Whether it is possible to prove this theorem while remaining inside arithmetic is unknown. But this topic (what is the minimum strength of a theory sufficient to prove this already proven theorem) is the main motive reverse mathematics.

If it is not known for Fermat’s theorem whether it can be proved arithmetically, then for Goodstein’s theorems, also arithmetic, it is reliably known that there is no arithmetic proof. On the other hand, it is quite trivially proved even in very weak versions of set theory.

There are other problems with evidence, for example, proof of the four color theorem was not immediately accepted by all mathematicians because it was computer generated. And the proof abc theorems valid only in Japan. However, there are computer systems for automatic verification of evidence, so at this very first level, everything will be fine.

Level 2 – second-order theories

It is very easy for a programmer to explain the difference between second-order theory: you need to think about what type of variable can be after the quantifier. If this is a number (or another simple object, if the theory is not about numbers, but we are still starting from arithmetic), then this is a first-order theory.

If the variable is of type ‘any expression‘, then this is a second-order theory. When at school they taught us analysis and said ‘for any function…‘, then it was just the second order. The strength of the second order theories is much, much greater than the strength of the first order theories, but their basis, as we shall see, is a little more shaky. In general, the higher we climb, the more everything will shake.

There is also an intermediate level in terms of strength, monadic 2nd order, where expressions in quantifiers cannot be specified, but sets can be specified.

As a rule, expressions are denoted by uppercase:

In this case, X is an expression, and if you learned the principle of mathematical induction in the entry above, then you are a great fellow. Wait a second… But the principle of mathematical induction is also used in formal first-order arithmetic! But how – after all, in its essence, this is a typical second-order rule!

The answer is: regexp. Yes, yes, it is him. In first-order arithmetic, the principle of mathematical induction is expressed by an infinite number of axioms that fit under regexp. A little ugly, but it works.

We haven’t talked about Gödel’s theorem yet, but it doesn’t work for second-order theories. Perhaps there are some analogues. But in general, you need to be more careful with second-order theories – it’s not without reason that second-order arithmetic is called set theory in sheep’s clothing:

Set theory is likened to a “wolf” for a number of paradoxes, an insane number of versions and variants of the theory, which can only be matched by the tree of *Unix variants. However, set theory is a first order theory, and the fact that it can successfully mimic most (not all) aspects of second order theory speaks volumes about its monstrous power.

Level 3 – meta theorems

Here we get to Gödel’s Theorem (there are several), the first of which states that in formal arithmetic there is an expression W, which is true but not provable:

Here PA – Peano Arithmetics. Godel’s meta theorem is proved by giving a second meaning to mathematical expressions, and then using the diagonal method, the expression is formed W, which has additional meaning: “i’m unprovable“

Recording

means that the statement E can be proven in theory T, and it is precisely this moment that brings us to the third level of logic, since the concept “can be proved” is not expressible in logics of either the first or second order (although Gödel’s theorem connects provability with the properties of numbers)

Interestingly, the expression W can be written explicitly (Gödel’s meta theorem is constructive). I saw a picture with a very long formula for Wbut now I can’t find it. Maybe one of the readers can?

I once had an argument with a man who claimed that Godel’s theorem is an arithmetic theorem, because the expression W expressed in arithmetic. However, even in this case, the proof is produced at the meta level and is not expressible in arithmetic. In addition, we call Gödel’s theorem the statement about the existence of unprovable statements in PA, and not a long and, at first glance, devoid of special meaning, a long expression W.

If you are wondering if there are shorter unprovable statements in arithmetic, then yes – tGoodstein’s theoremwhich I have already mentioned.

Level 4 – Theory quantifiers

There are extensions of Gödel’s theorem, which are also sometimes sloppily called Gödel’s theorem. Meanwhile, this is a new, higher meta level. Consider these extensions:

First generalization of Gödel’s theorem: if an unprovable statement W is added to PA as a new axiom, then the resulting new theory (PA+W) still contains a new unprovable statement W1, and so on. That is, this is a system bug, it cannot be fixed by adding new axioms

Have you noticed the quantifier on theories?

Second obobGödel’s theorem: any consistent theory in which formal arithmetic is expressible is incomplete, that is, a variant of Gödel’s theorem applies to it (additionally, it is required that the system of axioms either be finite or all regexp were algorithmically decidable)

Here the quantifier is quite obvious.

At the same meta-meta level, theory about theories, is the theory of models. It studies, and what sets of objects satisfy theories? From the interesting conclusions of this theory:

First-order theories are unable to control the power of their models: if there is an infinite model, then there are other models of any power.

That is, formal arithmetic describes not only natural numbers (their countable number), but other sets of chips (for example, the cardinality of the continuum) that satisfy all the rules of the game of arithmetic! Such models are called non-standard..

It also works the other way: the theory of real numbers (of which there is a continuum) has a countable model (what???). set theory ZFC also has a countable model, although in this model some tokens satisfy the formula ‘this set is uncountable‘. This paradox is called Skolem’s paradox.

Second-order theories, by the way, are able to control the power of their models, so they are not reducible to first-order theories with the help of various tricks.

I was interested in this question: the model of a theory is a set of objects that can satisfy this theory, but what version of set theory do we use at this level? The answers of mathematicians are somewhat confused and contradictory.. In any case, here the building is already staggering very strongly, and you look like you will step on the rake of the contradictory ‘naive’ set theory. And to do this is easier than ever: for example, in alternative set theory New Foundations exists ‘set of all sets‘ without creating a contradiction.

Level 5 – quantifiers in logics

What could be more abstract than quantifiers on theories? Theories, as a rule, still rely on general logical rules. But not always: there is intuitionistic logic, negating excluded middle principle. She is closely associated with constructive mathematics, where it is impossible to prove the existence of something ‘from the contrary’, the object must be ‘presented’. Other logic versions are also possible.

Here is an example of reasoning at this level from here: here it is proved that from AC (the famous axiom of choice) follows the rule of the excluded middle, and hence constructive mathematics and AC incompatible if you are not ready for other sacrifices:

we note that in deriving Excluded Middle from ACL1 essential use was made of the principles of Predicative Comprehension and Extensionality of Functions^[18]. It follows that, in systems of constructive mathematics affirming AC (but not Excluded Middle) either the principle of Predicative Comprehension or the principle of Extensionality of Functions must fail.

The principle of Extensionality can easily be made to fail by considering, for example, the predicates P: rational featherless biped and Q: human being and the function K on predicates which assigns to each predicate the number of words in its description. Then we can agree that P≈Q but KP=3 and KQ=2.

Level 6 – Philosophy

Yes, this is pure philosophy, though mixed with mathematics.

Here’s an example: How to relate to the fact that different mathematical theories can give different, often diametrically opposed conclusions? Mathematicians hold different beliefs: formalists they just say it’s a game. We set different rules and got different results. Why be surprised?

Platonists they see a certain reality behind the formulas, because theories are invented for a reason. For example, set theory NF (New Foundations) is built on completely different principles than the classic ZFC, but for some reason repeats her conclusions about unattainable capacities. V NF, where there is universal set, however, does not work AC, but this also occurs in ZFC for very high powers... Coincidence? Or a hint that there is something behind the formulas?