3 Oct
2024
3 Oct
'24
10:15 p.m.
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(a)igc.org>
Alex. Well stated!
From: ontolog-forum(a)googlegroups.com <ontolog-forum(a)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