Voevoedski's univalent foundations of mathematics

I found a very nice article about the work of mathematician Voevoedski: he talks about univalent foundations of mathematics. To put in nutshell: the world deals with mathematical proofs and the deep idea is that proofs are like paths in some abstract space. One deals with paths also in homotopy theory. What is remarkable that Voevoedski's work leads to computer programs allowing to check that proof does not contain an error. Something very badly needed when the proofs are getting increasingly complex. I dare to guess that the article is understandable by laymen too.

Russell's problem

The article tells about type theory originated already by Russell, who was led to his paradox with the set consisting of sets which do not contain itself as an element. The fatal question was "Does this set contain itself?".

Russell proposed a solution of the problems by introducing a hierarchy of types. Sets are at the bottom and defined so that they do not contain as set collection of sets. In usual applications of set theory - say in manifold theory - this is always true. Type hierarchy guarantees that you do not put apples and oranges in the same basket.

Voevoedski's idea

Voevoedski's work relates to proof theory and to formalising what mathematical proof does mean.

Consider demonstration that two sets A and B are equivalent. This means simple thing: construct a one-to-one map between them. Usually one is only interested in the existence of this map but one can also get interested on all manners to perform this map. All manners to make this map define in rather abstract sense a collection of paths between A and B regarded as objects. Single path consists of a collection of the arrows connecting element in A with element in B.

More generally, in mathematical proof theory all proofs of theorem define this kind of collection. In topology all paths connecting two points defined this kind of collection. In this framework Goedel's theorem becomes obvious: given axioms define rules for constructing paths and cannot give the paths connecting arbitrarily chosen two truths.

One can again abstract this process. Just as one can make statements about statements about..., one can build paths between paths, and paths between paths between paths.... Voevoedsky studied this problem in his attempts to formalise mathematics and with a practical goal to develop eventually tools for checking by computer that mathematical proofs are correct.

A more rigorous manner to define path is in terms of groupoid. It is more general notion that that of group since the inverse of groupoid element need not exist. For intense open paths between two points form a group but only closed paths can be given a structure of group.

Voevoedski introduced the notion of infinite groupoid containing paths, paths between paths, .... ad infinitum. Voevoedski talks about univalent foundations. The great idea is that homotopy theory becomes a foundation of mathematics: proofs are paths in some abstract structure. This suggests in my non-professional mind that one can talk about continuous deformations of proofs and that one can classify them to homotopy types with proofs of same homotopy type deformable to each other.

How this relates to quantum TGD

What made me fascinated was how closely the basic hierarchies of quantum TGD relate to the objects studies in type theory and Voevoedski's approach.

Let us start with set theory and type theory. TGD provides a non-trivial example about types, which by the way distinguishes TGD from super string models. Imbedding space is set, space-time surface are its subsets. "World of classical worlds" (WCW) is the key abstraction distinguishing TGD from super string models where one still tries to deal by working at space-time level.

What has surprised me against and again that super string modellers have spend decades in the landscape instead of making super string models a real theory by introducing loop space as a key notion although it has very nice mathematics: just the existence of Kähler geometry fixes it uniquely: this observation actually led to the realisation that quantum TGD might be unique just from its mathematical existence.

The points of WCW are 3-surfaces and its sets are collections of 3-surfaces. They are of higher type than the sets of imbedding space. There would be no sense in putting points of WCW and of imbedding space in the same basket. But in the set theory before Russell you could in principle do this. We have got as as birth gift the ability to not put cows and tooth brushes into same set. But the ability to take seriously the existence of more abstract types does not seem to be a birth gift.

Voevoedski and others deal with statements about statements about statements…. What is amusing that this vision has direct counterparts in TGD based quantum physics where various hierarchies have taken key role. Some deep ideas seem to burst out simultaneously in totally different contexts! Voevoedski noticed the same thing in his work but with within the realm of mathematics.

Just a list of examples should be enough. Consider first type theory.

1. The hierarchy of infinite primes (integers, rationals) was the first mathematical discovery inspired by TGD inspired theory of consciousness. Infinite primes are constructed by a process analogous to a repeated second quantisation of arithmetic quantum field theory having interpretation as making statements about statements about..... up to arbitrary high order. Hierarchy of space-time sheets of many-sheeted space-time is the classical counterpart. Physics prediction is that higher level of quantisation are part of generalised quantum physics and allow quantum description of macroscopic and even astrophysical objects. The map of the sheets of many-sheeted space-time to single region of Minkowski space defines the contraction of TGD to GRT and is approximate operation: it maps a hierarchy of types to single type and is a violent procedure meaning a loss of information.
   

   Infinite integers could provide a generalisation of Goedel number numbering in a quantum mathematics based on the replacement of axiomatics with anti-axiomatics: specify what you cannot do instead of what you can do! I wrote about this in earlier posting.
   

   Infinite rationals of unit real norm lead also to a generalisation of the real number. Each real point becomes infinite dimensional space consisting of all infinite rationals of unit norm but well-defined number theoretic anatomy.
   
   

2. There are several very closely related infinite hierarchies. Fractal hierarchy of quantum criticalities ( ball at the top of a hill at the top...) and isomorphic super-symplectic sub-algebras with conformal structure. There is infinite fractal hierarchy of conformal gauge symmetry breakings. This defines infinite hierarchy of dark matters with Planck constant h_eff=n× h. The algebraic extensions of rationals giving rise to evolutionary hierarchy for physics and perhaps explaining biological evolution define a hierarchy. The inclusions of hyper-finite factors realizing finite measurement resolution define a hierarchy. Hierarchy of infinite integers and rationals relates also closely to these hierarchies.
   
   
3. In TGD inspired theory of conscioussness hierarchy of selves having sub-selves (experienced as mental images) having.... This hierarchy relates also very closely to the above hierarchies.
   
   

The notion of mathematical operation sequences as path is second key idea in Voevoedski's work. The idea about paths representing mathematical computations, proofs, etc.. is realised quite concretely in TGD quantum physics. Scattering amplitudes are identified as representations for sequences of algebraic operations of Yangian leading from an initial collection of elements of super-symplectic Yangian (physical states) to a final one. The duality symmetry of old fashioned string models generalises to a statement that any two sequences connecting same collections are equivalent and correspond to same amplitudes. This means extremely powerful predictions and it seems that in twistor programs analogous results are obtained too: very many twistor Grassmann diagrams represent the same scattering amplitude.