Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: