Re: soundness for RIF

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