- From: Francois Bry <bry@ifi.lmu.de>
- Date: Wed, 10 May 2006 13:30:04 +0200
- To: W3C RIF WG <public-rif-wg@w3.org>
Sandro Hawke wrote: >> 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. > Sound always refers to something else. A programme generating prime numbers is sound wrt the defr. of prime number. My sentence started with "Sound is used in logic for expressing ...". I made a clrear restriction to logic. Otrher uses are similar yet different. > 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. > In the theorem proving community, sound is said of the theorem prover s.t. what it clainms to be logical consequences (dewfined in a model theory) actually are. Complete is used for a theorem prover that can compute all logical consequences. When used in this community fdor software, it is always used that way. (I am very, very sure of what I say). > 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? > I am saying that usually in logic the concept of soundness is used as I said. I am not excluding it being used by some logicians in another way but this would be quite unusual. > 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. This is exactly what I said. In logics there are two ways to define true consequewnces: 1. through a model theory (like in classical logic or in OWL) 2. only through a proof calculus (like in most constructive logic like Johansen's minimal logic). Validity or soundness isusually used for "connecting" a proof calculus to a model theory in the first case. > An unsound argument either has one or more false > premises or relies upon an invalid inference; its conclusion may be > either true or false. > There again, nothing that wouyld contradict what I said. FRancois
Received on Wednesday, 10 May 2006 11:30:09 UTC