Schreiber Laws of Type

Algebra and Reality

At times, one may feel a deep miracle in the fact that we write symbols to paper – formulas of laws of physics – and then these symbols carry meaning and information about physical, tangible reality.

It may, at times, almost feel a bit like casting a spell, uttering words and thereby creating reality. As in a quote from theoretical physicist John Archibald Wheeler, which begins as:

Write your equations $[$ for physics $]$ on the tiles of the floor. When you’re done, wave a wand over the equations, tell them to fly. $[$ … $]$

Indeed, model builders in particle physics and cosmology routinely do speak in this vein: for instance they actively “add masses to particles by including SUSY breaking terms” (e.g here) instead of “including SUSY breaking terms in our equations such that they describe massive particles”.

In an age of science, we disregard spells as a figment of our ancestor’s imagination. But mathematics and the exact sciences have realized much of what ancient kabbalists or alchemists were intuitively anticipating: Today we can write symbols on paper, arrange them by esoteric rules, and thereby do make them reflect on the tangible world, notably make them predict the future – say the time when the sun will burn out and shrink away – and the past – say the helium density three minutes after the Urknall. We may forget at times how remarkable that is.

But, still, this is just the physics aspect of it. From there it gets more, say, miraculous even: for, by the unreasonable effectiveness of mathematics we find that many of these spells all follow from a handful of master spells: Einstein's equations and those of Yang-Mills theory. Apart from all the constants of nature in it, the standard model of particle physics is a simple mathematical formula that fits on a few lines. Given all the things that follow from it, this is a rather mighty spell.

Can one go further?

Certainly physicists are trying: in Grand Unified Theory and more generally in the theory of everything known as string theory, physicist try to deduce these “experimentally verified master spells” from even more fundamental physics. But still from physics.

Quantum field theory is argued to be the modern explanation of “creation of a universe from nothing”, namely from a quantum vacuum (see e.g. Carroll 12).

But one participant of the modern and scientifically informed re-staging of this discussion points out that “void” here cannot sensibly mean just quantum vacuum:

Where, for starters, are the laws of quantum mechanics themselves supposed to have come from? (Albert 12).

and then:

What if $[$ somebody $]$ were in a position to announce, for instance, that the truth of the quantum-mechanical laws can be traced back to the fact that the world has some other, deeper property $X$? Wouldn’t we still be in a position to ask why $X$ rather than $Y$? And is there a last such question? Is there some point at which the possibility of asking any further such questions somehow definitively comes to an end? How would that work? What would that be like? (Albert 12)

The particular, eternally persisting, elementary physical stuff of the world, according to the standard presentations of relativistic quantum field theories, consists (unsurprisingly) of relativistic quantum fields. And the fundamental laws of this theory take the form of rules concerning which arrangements of those fields are physically possible and which aren?t, and rules connecting the arrangements of those fields at later times to their arrangements at earlier times, and so on ? and they have nothing whatsoever to say on the subject of where those fields came from, or of why the world should have consisted of the particular kinds of fields it does, or of why it should have consisted of fields at all, or of why there should have been a world in the first place. (Albert)

Algebra and creation myths

This is in fact a modern version of a common idea expressed in various ancient myths of mankind. For instance the Zohar, dating from a few hundred years BC, is quite explicit: the origin of the universe is claimed to proceed out of a primordial void, the Ayn Sof, and by a self-reflecting process, the tzimtzum, that makes non-emptiness appear from just emptiness.

Unlike much of natural philosophy, which has eventually been formalized and made part of the exact sciences, these creation myths seem to have remained immensely vague to date.

Remarkably enough there is the ancient idea that creation rests in manipulating symbols:

Twenty-two letters: God drew them, hewed them, combined them, weighed them, interchanged them, and through them produced the whole creation and everything that is destined to come into being. (Sefer Yetzirah, ii.2)

Can there possibly be an algebra that usefully captures this intuition behind the Ayn Sof? Which symbols could it possibly use?

The Zohar does in parts reflect on this question, when it says:

Before He gave any shape to the world, before He produced any form, He was alone, without form and without resemblance to anything else. Who then can comprehend how He was before the Creation? Hence it is forbidden to lend Him any form or similitude, or even to call Him by His sacred name, or to indicate Him by a single letter or a single point… Zohar, part ii., section “Bo,” 42b

Not by a single letter: it is the empty symbol.

By tzimtzum this void retreats to produce the universe. And it is a symbol that accomplishes this:

After this tzimtzum… He drew down from the Or Ein Sof a single straight line (Etz Chaim, Arizal, Heichal A“K, anaf 2)

and that manifests creation:

$[$…$]$ In the space of that void He emanated, created, formed and made all the worlds. (Etz Chaim, Arizal, Heichal A“K, anaf 2.

In concise paraphrase, the creation myth of the Ayn Sof asserts that:

From the initial void, denoted by the empty symbol, the denotation of a line makes the universe come into existence, whose fine structure is revealed by (further) manipulation of symbols.

Or:

1. the tangible world is exhibited by algebra of symbols;

2. it is created by the severance of the initial empty symbol by a line.

Curiously, this is the statement which in 1969 George Spencer Brown‘s book Laws of Form is suggesting again, but in terms of genuine algebra in the modern mathematical sense.

Laws of Form

While Laws of Form is a text on mathematics, the tone of the prose surrounding the algebra is mystical. And it is not narrative, but imperative, like that of a spell. The author clearly sees his work in a role not entirely unlike that of the creation myth in the Zohar.

The book begins by suggesting that the empty page is to be read as a symbol. The author then draws a single symbol on this empty page and says that this act creates a universe from emptiness:

The theme of this book is that a universe comes into being when a space is severed or taken apart (LoF 72, page v).

Two simple algebraic rules on combinations are imposed on these two symbols. The text suggests that by these algebraic manipulations alone a complex universe emerges from the initial symbol.

This shows a strong believe in that spell called formal mathematics. Much stronger than Wheeler’s, whose quote above instead continues:

$[...]$ Not one [of these equations] will sprout wings and fly. The universe flies, it has a life to it that no equation has.

In fact the claim is bold:

By tracing the way we represent such a severance, we can begin to reconstruct, with an accuracy and coverage that appear almost uncanny, the basic forms underlying linguistic, mathematical, physical, and biological science, and can begin to see how the familiar laws of our own experience follow inexorably from the original act of severance. (LoF 72, page v)

But contrary to this, after its strong poeto-mathematical beginning, Spencer Brown’s text falls short of these bold claims. The algebra presented is really just Boolean algebra in unusual notation (cf. Banaschewski 1977, I am grateful to André Oksas for pointing out this reference):

The empty symbol identifies with the Boolean false, and the severing line with the Boolean negation-operation $\neg$, which sends false to true and true back to false. Indeed, the “severing symbol” of Spencer Brown is a larger variant of the standard symbol “$\neg$”; only that he draws it over the expression being negated, instead of to the left it, as usual. His juxtaposition is the Boolean “or” disjunction, and so his “law of calling” is the logical rule $true \vee true = true$, while his “law of crossing” is the Boolean axiom $\neg \neg = id$.

Boolean algebra is not without interest; it is a basic building block in formal logic. But Boolean algebra alone does not support a universe of mathematical concepts, let alone a physical universe. Boolean algebra is just the logic of a single isolated bit.

And indeed, when the book comes to the promise of deriving “the basic forms underlying linguistic, mathematical, physical, and biological science” supposedly from this algebra, actually presented is only the vague suggestion that writing a paradoxical (one would say: wrong) expression of the form $a = \neg a$ somehow implies a dynamics, suggested by the formal symbol manipulation $a = \neg a = \neg \neg a = \neg\neg \neg a = \cdots$. That suggestion may well appeal to mystical intuition, and it did to many readers – but this degree of vagueness of the intuition of a universe appearing out of a self-reflecting emptiness is already Zohar’s. How does the algebra improve on that state of the art?

In summary, the book Laws of Form makes a noteworthy suggestion; that modern algebra may capture aspects of genuine ontology. But the concrete algebra it promotes is not powerful enough. It only knows that the negation of the initial emptiness is something. But it cannot see any structure in this something.

It is, admittedly, only in 1971, two years after the appearance of Laws of Form, that the first sketch appears of what has become modern formal logic: Per Martin-Löf‘s type theory. This captures both: the elegance of Spencer Brown’s formalization of the creation myth, as well as a complex universe.

Here is how:

Laws of Type

In the context of type theory, the idea of an empty symbol reminds us of the empty type $\varnothing$, whose categorical semantics is the initial object.

And indeed, in the syntactic implementation of type theory in Coq, this is verbatim what happens: the Coq-code that defines the empty type (as an inductive type) is

  Inductive empty : Type :=

with the line ending abruptly after the defining equality sign.

The fundamental construction in type theory is that of function types, denoted $A \to B$. The operation of negation is $(-) \to \varnothing$. And we have the equivalence of types

$$\varnothing \to \varnothing \;\;=\;\; * \,,$$

identifying the negation of the empty type with the unit type.

If we follow Spencer Brown’s notation and suppress the denotation of the empty type, then the above says that the unit type is expressed as

$$\longrightarrow$$

A single line.

In the categorical semantics of type theory in a topos, types identify with the slices over them. In this sense the unit type is the ambient topos itself, hence it is the outermost universe, the limit of the ascending chain of internal universes, in the technical mathematical sense of “universe”.

He drew down from the Or Ein Sof a single straight line

…a universe comes into being when a space is severed or taken apart.

In the notation of type theory with the denotation of the empty type suppressed, we have the “law of crossing”

$$\to \to \;\;=\;\;$$

namely the basic identity in type theory which says that

$$(\varnothing \to \varnothing) \to \varnothing \;\;=\;\; \varnothing \,.$$

So Spencer Brown’s Laws of Form are naturally identified as a small fragment of type theory – the Laws of Type.

In fact, this is precisely just (Boolean) (-1)-type-theory. Most of traditional mathematics is formulated in 0-type-theory. Most natural is the case of ∞-type theory.

Laws of homotopy Type

See at Higher Structures.

Laws of cohesive Type

Continued at Modern Physics formalized in Modal Homotopy Type Theory.

References