Re: soundness for RIF

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