>It turns out that, aside from their common interest in antagonising Isaac Newton, Hooke and Leibniz also shared an interest in mechanising scientific reasoning through the invention of a universal language for science. Leibniz called his project the "Characteristica Universalis".

I'm surprised it doesn't mention Leibniz's famous "Let us calculate" quote:

>>In a 1679 letter to one of his patrons, Johann Friedrich, he described his project of the universal language as “the great instrument of reason, which will carry the forces of the mind further than the microscope has carried those of sight”. Later he wrote:

>>>The only way to rectify our reasonings is to make them as tangible as those of the Mathematicians, so that we can find our error at a glance, and when there are disputes among persons, we can simply say: Let us calculate, without further ado, to see who is right.[1]

I'm also kind of surprised that Hooke wrote the letter in English, since I assumed all academic communication across language barriers back then would have been in Latin. But ChatGPT tells me Leibniz was unusually multi-lingual.

[1] Sorry, ad-heavy site but I wanted one that gave context: https://publicdomainreview.org/essay/let-us-calculate-leibni...

> The only way to rectify our reasonings is to make them as tangible as those of the Mathematicians, so that we can find our error at a glance, and when there are disputes among persons, we can simply say: Let us calculate, without further ado, to see who is right.

And then Kurt Gödel forever permanently dashed those dreams.

Leibniz invented binary — so he kind of succeeded in his quest.

He based it on the Chinese iching, interestingly enough…

He was ahead of his time, definitely, and binary logic is one critical step in getting there, but we're a long way from having a formal language to represent all claims that would ever arise in human argumentation to the point that it's simply a matter of calculation to resolve them.

Check out metamath.org I can't fathom any valid argument that couldn't be formalized to mathematical statements. There would still be disagreements on axioms and physical postulates, especially where there are conflicts of interest.

The whole project kind of died with Gödel.

He didn’t actually base it on the Yiching, he just noticed that it could be expressed neatly in binary. But he had come up with binary code before that.

Thanks for pointing me to that. Here is some source material.

https://www.historyofinformation.com/detail.php?id=395