I've looked at Godel's ontological proof of the existence of God (based on Leibniz). My puny brain is incapable of critiquing his reasoning, but I understand that some people point out errors or fallacies in his argument.
For me (English major) the significance of Leibniz (beyond mathematics) was his existence as an object of ridicule by Voltaire.
So your explanation of Leibniz here was very helpful.
I'm wondering about his creation of a universal language ("Characteristica Universalis"). It seems problematic to me because even though Leibniz eventually reaches a language based on numbers, he arrives at that Universal from a specific natural language (German in his case).
Now natural languages are not mappable on a 1-1 basis of synonomy. You can look up "blue" in an English-Chinese dictionary, for example, but the term you get will not necessarily reflect the same position on a color spectrum as will the English word "blue." And of course language-based syntax can influence the meaning of a word.
So the "Characteristica Universalis" that a German speaker effects will not NECESSARILY be identical to a "Characteristica Universalis" that a speaker of Navajo effects (which of course was why the U.S. used code talkers in WW2).
But it seems to me to be telling that speakers of German (Leibniz, Godel) would be attracted to the notion of a universal mode of communication / proof. Paradoxically, the proponents of uncertainty, relativity, and language games are also German. Go figure.