For all practical purposes, Gödel's theorem is irrelevant. It shows that certain
very complex propositions stated in first-order logic are undecidable. However, the only
people who can state an undecidable proposition are professional logicians who have
studied Gödel's proof.
Gödel stated that theorem about 50 years after Frege and Peirce specified FOL. In those
50 years, no logician had ever written or encountered an undecidable proposition.
For the Cyc system, which uses a superset of FOL, Doug Lenat said that in over a thousand
person-years of developers who wrote knowledge representations in Cyc, nobody had ever
written an undecidable statement.
The designers of OWL made a terrible mistake in restricting its expressive power to avoid
undecidable propositions. That made OWL more complex and more difficult to learn and use.
The people who made that mistake were professional logicians. I have a high regard for
their theoretical knowledge, but very little regard for their practical knowledge.
John
__________________________________________
From: "Wartik, Steven P "Steve"" <swartik(a)ida.org>
Sent: 7/11/24 4:30 PM
Thanks for posting that. It makes me angry my licentious youth didn’t lead to any divine
revelations.
I’m surprised the author didn’t mention Kurt Gödel. He provides the proof a perfect logic
machine isn’t possible, right?
From: ontology-summit(a)googlegroups.com <ontology-summit(a)googlegroups.com> On Behalf
Of Jack Park
Sent: Thursday, July 11, 2024 4:11 PM
----------------------------------------
https://nautil.us/the-perpetual-quest-for-a-truth-machine-702659/ is a decent overview of
this space.