> 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 :)
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.