Re: Grist for layering discussion

>On Sat, 2002-01-12 at 05:43, Peter F. Patel-Schneider wrote:
>>  From: Dan Connolly <connolly@w3.org>
>>  Subject: Re: Grist for layering discussion
>>  Date: 11 Jan 2002 20:46:44 -0600
>  >
>>  > On Fri, 2002-01-11 at 19:14, Peter F. Patel-Schneider wrote:
>>  > [...]
>>  > > > So you feel that allowing reification -- or, presumably, allowing
>>  > > > sets of statements as first class objects in the syntax -- 
>>makes the system
>>  > > > such that one can necessarily deduce a contradiction from nothing?
>>  > > > Then I need help understanding how.
>>  > >
>>  > > Look at the spec for KIF at 
>>http://logic.stanford.edu/kif/dpans.html.  The
>>  > > section on Metaknowledge has a nice description of one such problem.
>>  >
>>  > A solved problem, no?
>>
>>  Well, yes, as long as you don't mind the effects of the solution, which are
>>  to, roughly, disallow any ``formula'' that is self-referential.
>
>Is that the case for the KIF v3 version of wtr too?
>
>I know the dpans KIF disallows any occurence of wtr inside wtr...
>but the v3 version didn't have that constraint; it just required
>that the not's be pushed out or something... I guess I should
>look it up...
>
>   Changing Levels of Denotation
>   http://meta2.stanford.edu/kif/Hypertext/node35.html
>
>So it's pushed in, not pushed out.

Right. The pattern that has to be somehow forbidden is (wtr 
....(not....(wtr....)...)...) (being careless about quotation). The 
simple way is to forbid wtr inside wtr. The sexier way is to say that 
inside wtr, (not...(wtr....)...) has to be rewritten (or understood 
as meaning what you would get by rewriting) using deMorgans law to 
get (,,,(not(wtr....),,,) and then replacing that by 
(,,,(wtr(not....)),,,), which is not equivalent but is slightly 
weaker. This is just enough to block the liar-type paradoxes, and it 
leaves most of the wtr assertions alone, and it only weakens the 
others just enough to stop them blowing up. This idea was thought up 
by Don Perlis (a colleague of Jim Hendler's, oddly enough) and 
published about 15 years ago.

>
>>  Unfortunately, there are lots of such situations that are needed.
>>
>>  (In KIF, the problem only occurs with respect to WTR, because that is the
>>  predicate that asks whether a ``list'' represents a true formulae.  In the
>>  DAML+OIL case, however, there is essentially an implicit WTR attached to
>>  every restriction.)
>
>Really? can you elaborate?

The point is that if we are rigorous about quotation and use/mention, 
then every place that a formula is described, but intended to be 
used, is really a place where one ought to write ...(wtr '(...

>
>>  > I've looked at it... several times. It seems to be exactly
>>  > what we need. (Actually, the KIF v3 version is less constraining
>>  > and looks more useful).
>>
>>  One way of translating the KIF solution to DAML+OIL would end up
>>  disallowing classes from belonging to themselves, even indirectly.  I don't
>>  think that you want that.
>
>No..
>
>Er... I meant to say that DAML+OIL/WebOnt could be based on
>KIF modified with the menzel indrection trick. I gather
>PatH is working on making this the standard model theory
>for KIF.

Pat and Chris Menzel. The ISO-KIF committee is moving even more 
slowly than the W3C process moves ;-), but the basic semantics is 
worked out. As far as we can tell, this trick has no significant 
interaction with the Perlis 'wtr' trick, but we havn't done the dirty 
details to be absolutely sure. I'd be willing to put money on it, 
though.

......<snip>

>  > As long as you can't create a contradiction, all this reification stuff
>>  usually works fine.  However, contradictions and reification generally
>>  allow you to create the Liar's paradox, and everything comes tumbling down.
>
>Whenever I write down the Liar's paradox, TimBL usually counters
>with something about the excluded middle not applying...

Well, counter back with the observation that the excluded middle is 
irrelevant. That liar paradox isn't an easy dragon to slay. For a 
mathematical logician, finding a way past Goedel incompleteness while 
still allowing all 'intuitive' reasoning would be like finding the 
holy grail. The best people have tried every way anyone can think of 
for about 40 years, and nobody has managed to find it. The consensus 
is that it doesn't exist. People have tried using multi-valued logics 
(including those with an 'undefined' which kills the excluded middle 
rule), and using intuitionist logic, and all kinds of other logics. 
None of them get rid of the liar-style paradoxes.

>I agree
>that there's not much to talk about there until we figure out
>what we're using in place of the law of the excluded middle.

Its a pretty hard law to avoid. You use it implicitly even when you 
use other rules. For example, if your logic isn't two-valued then you 
don't have LEM, but you also don't have things like being able to 
reason to a negation from a contradiction, or being able to whittle 
down a disjunction to one case by excluding all the other cases. In 
general, its not easy to take one piece of logic and leave others on 
a whim, since they are all connected together. There are genuine 
alternatives in logics, of course, but you need to show how the logic 
you want has some kind of overall coherence.

The only way to completely avoid the EM (in one form or another) is 
to use a 3- (or more)-valued logic which is extremely weak in the 
sense that it is impossible to express truth, only what might be 
called 'true-or-undefined' and 'false-or-undefined'; and this weak 
3-valued logic is so wimpy that almost none of the ordinary reasoning 
processes that are so useful can be expressed in it. (The 
characteristic property of a weak 3-valued logic is that if any 
sub-expression of any propositional formula is undefined, then the 
whole formula is. All the truth-tables have entire rows and columns 
filled with 'U'. That means, in particular, that it is impossible to 
say: 'P is undefined'.)

Pat

PS. This idea of avoiding the excluded middle seems to me to be a 
non-starter, in any case. Can anyone say why they think it is a good 
idea, or what the reasoning is behind it? I see nothing in the web 
world that would suggest that the LEM doesn't apply there as well as 
it does anywhere else.


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

Received on Tuesday, 15 January 2002 13:04:15 UTC