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@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@googlegroups.com <ontology-summit@googlegroups.com> On Behalf Of Jack Park
Sent: Thursday, July 11, 2024 4:11 PM