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.
The tricky bit is that "simplest" has no formal definition. Here Wolfram claims to simplicity is having the least number of axiom, even if that axiom is very complicated.
Unfortunately, that is a perversion of the idea of axiom. An axiom should be as simple as it can be and ideally self-evident. Being self-evident is a strong requirement because axioms are not proven but accepted as true.
Clearly, no-one would say that Wolfram's axiom is self-evident. As a matter of fact, even Wolfram does not find it self-evident: that it is equivalent and sufficient as a basis needed to be proven, via proving it can generate all other set of axioms.
Basically, once a field has matured enough and we found a simple set of axioms, one can come up with a new set. All set of axioms must encode the same information, so you can either have multiple simple one or a single complex one. The quantity of information that is encoded must be constant.
So having a single axiom is not simpler, except by the very naive measurement of count.
> 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.
This is true, I'm sure, in Physics. But I don't think it's true in logic. Did anyone working in logic at the time care about this question? Does it have any practical significance? If experts at the time didn't care and it has no useful purpose, then why should this impress me? Doing novel work is really easy -- just work on stuff other people don't care about.
Workers in the field of logic made steady progress in shortening the axioms throughout the 20th century, after Alfred N. Whitehead's axiomatization in 1898. Edward Huntington reduced it to three axioms using fourteen instances of two operators (OR and NOT) in 1933. Herbert Robbins conjectured it could be reduced to thirteen instances of those operator but could not prove it. Alfred Tarski also investigated and could not prove it. In 1967, Carew Meredith proved the axiomatization could be reduced twelve instances of OR and NOT (with only two axioms). Later, Meredith shows it could be reduced to two axioms with ten instances of a single operator (NAND). Several single-axioms systems were later found, but they were very long axioms. William McCune proved the Robbins conjection in 1996. And finally Wolfram and McCune apparently independently discovered and proved that the shortest possible single-axiom has only six instances of a single operator (NAND).
That this list of workers includes names like Whitehead and Tarski suggests that this was in fact something that (some) significant people did care about. I'm not sure how much value to give to this heuristic, but every name on the list of workers above is an 'important enough person' to have their own Wikipedia article. Certainly when I look discrete math classes in university, this was discussed as if it was an interesting topic (and I personally was interested).
I wonder if this is related to the shortest one combinator basis being λx λy λz. x z (y (λ_. z)), whose type is
(a -> b -> c) -> ((d -> a) -> b) -> a -> c.
He made novel contributions to computability theory. The first person to show that one-dimensional cellular automata could be turing-complete.
That being said, he’s very much a crackpot nowadays. Being sane in the past does not imply you will be sane in the future, no matter how significant your list of accomplishments.
His results on cellular automata are clearly solid contributions. Any academic would be proud to open a whole line of inquiry. I understand that he's also done good work in Physics.
I was just surprised to see this particular result about propositional logic in particular highlighted because, as a logician, I really don't care :)
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