Re: soundness for RIF

On May 10, 2006, at 12:30 PM, Francois Bry wrote:

> Sandro Hawke wrote:
[snip]
>>
>> Really?  I often hear the term "sound" used somewhat more loosely to

No need to perpetuate slop in a context where precise communication  
is very highly desirable.

[snip]

>> Google for "sound" "theorem prover"

Google for "sound foundation" and you'll see lots of people say that  
stone construction leads to sound foundations. And if you google for  
"sound system" you'll see lots of people say that their sound system  
has high fidelity. So?

>> and you'll see lots of people say
>> their theorem provers are sound and complete -- they are talking  
>> about
>> running code.

This is a simple contraction for "my code, by and large, correctly  
implements a sound and complete proof procedure".

(Frankly, this appeal to google is absurd and, in my opinion,  
counterproductive. It is *crazy* to try to fly in  face the plain and  
well understood central meaning of a term with regard to a particular  
subject matter by appeal to general and loose talk, especially when  
said term has a *precise* formal definition. It's even crazier to do  
so by appeal to the thinnest of empirical linguistic evidence. What  
purpose does this serve?)

> 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.

I wouldn't think so, at least not all the time, since I think a FOL  
prover can be said to implement a complete procedure, but of course  
it cannot 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?

Soundness is about the relation between a proof theory and a  
semantics, where, in general, the semantics are not proof theoretic.  
I don't think that restricts you to model theoretic semantics --  
algebraic semantics could be fine.

> 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

Since we are trying to be a bit nice with our terminology, let me say  
that it's not the happiest (even granting the possibility of  
inferential *semantics* acknowledged; or, for example, in the case of  
default logic, the lack of an *alternative* to a proof theoretic  
characterization) to use the word "true" here. It's exactly the fact  
that the derivations of a proof theory *might not be sound* that  
helps differentiate semantics from proof theory.

There are definitely at least two notions of "semantics" floating  
about: the first where the notion of meaning is connected to the  
notion of truth, falsity, etc., and the other where the meaning of a  
construct is connected to it's (computational) *behavior* (which may  
connect back up to something more like the first). I don't want to  
denigrate either approach (I *like* formal operational semantics for  
programming languages), but if we are going to use semantics in this  
ambiguous way, we should be extra careful with our use of certain  
semantic terminology, e.g., truth.

[snip]

Cheers,
Bijan.

Received on Thursday, 11 May 2006 12:23:42 UTC