Alex and Chuck,
That claim is FALSE in general, and determining the error bounds is essential.
It is true that you can write a formal statement that seems to state something similar to what is stated in English or other natural languages. But that does not imply that the two statements are equivalent.
A vague statement may express a continuous range of possibilities, but the translation to a statement in logic is limited to a very precise and very limited range of possibilities. Sometimes that is an advantage, but sometimes it can be horribly false or misleading or disastrous.
Engineers know this point very well. I quoted their motto in my previous note: "All theories are false, but some are useful." This point is absolutely TRUE. And I would apply it to your claim about formalization.
The critical issue is to determine what range of values in a translation is acceptable or useful. Unless you emphasize that range of options, your formalization is an invitation to DISASTER.
Re Leibniz: He had many good ideas, but he oversimplified issues about precision. He did not emphasize the importance of vagueness and the dangers of ignoring the error bounds.
John
From: "Chuck Woolery" <chuck@igc.org>
Alex. Well stated!
From: ontolog-forum@googlegroups.com <ontolog-forum@googlegroups.com> On Behalf Of Alex Shkotin
John,
Any verbal knowledge can be formalized, at least for the English language🦉 How precisely this knowledge is a topic for scientists and practitioners working in a particular area of reality. We simply formalize knowledge to use the power of a computer. But you are right, we need a reason for formalization as it's hard. In some cases, formalization can reveal some unclear areas in informal knowledge. And sometimes, in very rare cases, formalization can find errors in a mathematical text. There is a report of this kind from the Isabelle research group.
Just to make it clear: even wrong, inaccurate, vague knowledge may be formalized. If we need to.
And after
that we can run the verification algorithm and it will say that this knowledge is incorrect, inaccurate, or vague.
The first person to put forward this idea as a project was G. Leibniz, who was 25 years old. He hoped to obtain a formal language in 2-3 years🏋️
Alex