- From: Sandro Hawke <sandro@w3.org>
- Date: Tue, 09 May 2006 15:29:26 -0400
- To: Francois Bry <bry@ifi.lmu.de>
- Cc: public-rif-wg@w3.org
Francois Bry writes: > Sandro Hawke wrote: > > I believe this use of the word "sound" is normal and correct for logic. > > > Sound is used in logic for expressing that what can be proven using a > proof calculus is a logical consequence, ie corresponds to a model theory. > > If the logic has no model theory, like many constructive logics, > especially Johansen's Minimal Logic, then there is no notion of > soundness for this logic. Really? I often hear the term "sound" used somewhat more loosely to cover all kinds of reasoning procedures and systems, including software. For instance, the OWL spec says: An OWL consistency checker takes a document as input, and returns one word being Consistent, Inconsistent, or Unknown. An OWL consistency checker SHOULD report network errors occurring during the computation of the imports closure. ... An OWL consistency checker MUST be sound: it MUST return Consistent only when the input document is consistent and Inconsistent only when the input document is not consistent, with respect to the datatype map of the checker. -- http://www.w3.org/TR/owl-test/#consistencyChecker (Jeremy Carroll and Jos De Roo, Editors) Google for "sound" "theorem prover" and you'll see lots of people say their theorem provers are sound and complete -- they are talking about running code. While I know OWL has a model theory, you're claiming that these theorem provers must be for logics with model theories because they are claiming soundness? Or dictionaries: sound / unsound Distinction among deductive arguments. A sound argument both has true premises and employs a valid inference; its conclusion must therefore be true. An unsound argument either has one or more false premises or relies upon an invalid inference; its conclusion may be either true or false. -- http://www.philosophypages.com/dy/s7.htm#sound Perhaps there are nuances of usage in some communities that are lost on me. Do you see something misleading in my use of the word "sound" in the use case I described? I think of soundness and completeness as just splitting apart an obvious notion of correctness. "Sound" means you get no incorrect answers; "complete" means every correct answer will be returned. -- Sandro
Received on Tuesday, 9 May 2006 19:29:41 UTC