The physicalization of metamathematics and the implications for its foundations

> I never got the "emergent properties have special aesthetic and nearly spiritual significance" or "everything is just an " cognitive confusion that so many mathematicians (especially formalists) seem to have.

People just like spiritual beliefs. There's a reason why a majority of human beings hold non-rational beliefs like religion or money having intrinsic value.

I think that identifying the ruliad with the "logos" makes sense - the idea that there's some underlying abstract shape to the universe that makes rationality possible in the first place.

> In physics there are real tests and relations that have meaning so it makes sense to ask if String Theory is correct or useful. In mathematics there are complex structures built from axioms and sometimes these structures can be related to each other in interesting ways. Will anything important ever come of String Theory? Maybe, but from a mathematical point of view no theory needs to correctly model what is real or have demonstrated application to be worthy of exploration and study.

You say this as if it contradicts some point that the author is trying to make or some key assumption that he holds.

Yet on the contrary, the author himself makes a similar point in the article:

> But the way we’ve modeled mathematics here has been much more about what statements can be derived (or entailed) than about any kind of abstract notion of what statements can be “tagged as true”. In other words, we’ve been more concerned with “structurally deriving” that “” than in saying that “1 + 1 = 2 is true”.

That is, math is not necessarily about truth or usefulness in some (meta)physical sense, it is about entailment from certain axioms via formal rules.

That's certainly a description, but I'm not sure it's terribly useful for anyone who doesn't already know what confluence means in the context of a rewriting system.

For the casual programmer who's seen a lambda calculus at some point and is interested in understanding confluence in some detail, I recommend https://www.cs.cornell.edu/~kozen/Papers/ChurchRosser.pdf

If that work is too dense, all you need to know is the first paragraph. If that's all greek to you, it can be expanded as follows: Suppose you have a program e and an interpreter that executes e by applying a big set of rules that rewrite e until e becomes a value (such as a number, string, function, etc.).

So, for example, (function add(x) { x+x }; add(5)) -> 5+5 -> 6+4 -> 7+3 -> ... -> 10.

Here, "->" is thedefined by a big set of rules that basically pattern match on the syntax of the left-hand term and produce a corresponding right-hand term. So, for example, we have rules like:

(function F(x) { B[x] }; F(y) -> B[y]

and

n+m -> (increment of n) + (decrement of m)

and

n+0 -> n

where n,m are defined to be non-negative natural numbers.

Your interpreter is just a big set of these sorts of rewriting rules, and there's no "ordering" on the rules. Any rule that is applicable to the left-hand side could be used at any point where it's applicable.

Imagine, now, that you define your rewrite rules and then notice that at some points more than one rule might be applicable to the left hand side!

That could be bad if a single program could compute different values depending on which rule was chosen!

In general: Suppose there are some rewrite rules such that that e -> ... -> e1. (Which we sometimes write as e ->^* e1 for readability.) Suppose there are also some rules such that e -> ... -> e2, where e1 and e2 are different and might not be values (ie there's still more rules applicable to e2 and e3).

Your system is confluent -- i.e., not bad in the above sense -- if whenever the above happens there are also some rules such that e1 -> ... -> e3 and e2 -> ... -> e3. Then you know "there are many possible executions of the interpreter but at the end of the day the interpreter always spits out the same value"

It seems to me that 'crackpot' is a bit strong. Even if one thinks Wolfram's foundations of physics project will never bare useful fruit, it's undeniable that he has made progress in other fields that are of interest to many people.

A simple case in point: the study of logic has been a interesting human endeavor for thousands of years, since at least the time of the Greek and Vedic schools. After thousands of years of study, a major breakthrough was made with the first formalization of propositional logic (as Boolean algebra) by George Boole in 1854. Since then, there has been a search for the simplest foundational formal axioms from which all of propositional logic could be derived. This project ended in 2000 with Wolfram's discovery of, and proof that, [1] is the shortest possible single axiom that can be used as a foundation for all of propositional logic.

[1] ((a⁍b)⁍c)⁍(a⁍((a⁍c)⁍a)=c, where ⁍ is NAND