KIF: What's our goal?

[pat hayes]

>Pat,
>
>At 05:42 PM 7/5/2001 -0700, pat hayes wrote:
>>Adam:
>>
>>>Pat,
>>>I agree.  I don't think that our efforts on a new version of KIF 
>>>should be aimed at just one project, merely that SUO can be a 
>>>driving force, and as I see it, if it doesn't meet the needs of 
>>>SUO it will be deficient in important respects on other efforts.
>>
>>OK, but then while this kind of criterion can make a reasonable 
>>argument for including a feature (because SUO needs it, eg typing), 
>>it is not a good basis for *excluding* a feature because SUO 
>>*doesn't* need it. You re-opened this debate by arguing that a very 
>>useful and harmless feature ( (and) and (or) ) be excluded from the 
>>syntax, thereby making it universally unavailable to all users no 
>>matter what their goals or intentions, because you didn't want to 
>>use it in the SUO.
>
>I'm afraid this is not true.  I do want empty connective expressions 
>excluded from the syntax, but not just because I don't want it in 
>the SUO.  I think it's bad to allow vacuous statements.

(and) and (or) are not vacuous. They are, in fact, the truthvalues. 
Now, if one is only considering *assertions*, then indeed there is 
little point in asserting True or False. But if one is considering 
*sentences*, then being able to infer True or False can be essential. 
Resolution works by deriving (or) , ie False, from a set of clauses, 
thereby demonstrating that the set is unsatisfiable. Many natural 
deduction systems have inference rules that refer explicitly to the 
truthvalues, eg not-introduction is often phrased: From (p |- False) 
Infer (not p). More generally, one may want to regard (implies true 
q) |- q as a special case of modus ponens, for example. All of these 
and many other similar examples are found in real textbooks written 
by real logicians, believe it or not. If we make these expressions 
illegal in the syntax, all these very natural and sometimes useful 
inference systems will be excluded; and for no rational reason, since 
there is absolutely no way to legislate away the possiblity of some 
user asserting a truthvalue: they can always write a tautology, after 
all, and they can always negate a tautology. And tautologies can get 
arbitrarily complicated in their syntax. So it is, literally, 
impossible to not allow 'vacuous' statements.

Pat

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes at ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes