Re: More Approaches to Avoiding Paradox with Asserted Reifications

Hi Sandro,

I am glad you is addressing this issue.
I tried to raise early on this email list
and at the first DAML PI meetings January last year,
but apart from Pat Hayes nobody seemed to bite.

The problem affacts not only negation,
but also "syntactic modality"
which is how I imagine modality (beliefs knowledge etc)
would be handled in RDF, ie by first order predicates
over reified formulae.

I believe that RDF is more of aculprit than you think.
In languages with linear syntax you need
a fixpoint operator in order to construct a cyclic
reified sentence and hence a paradox.
Such power usually comes from recursive arithmetic
or the lambda calculus.
RDF seems to give you cyclic sentences essentially for free.

Of the approaches you suggest
Stratification and paraconsistent logic are the most promissing.
[I think you have covered all the plausible options,
only note that the main variant of paraconsistent logic
is relevant logic as studied by Anderson and Blenap in "Entailment"
and of which linear logic an instance]
Standard intuitionistic logic does not help,
since the problem is not excluded middle
but reductio ad absurdum, which is a valid principle
of intuitionistic logic.
However it is precisely the principle
rjected by paraconsistent/relevant logics.
There are of course relevant intuitionistic logics
but it is the relevance bit that address the issue you are dealing
with.

I think you a are right to be concerned about the viability
of moving negation to the meta-level somehow (ie option 4).
I think this this will suffer from the same problems
as syntactic modality.
The general scope of this problem
was discussed by Montague.
There is also a very detailed discusion of the issues in
Raymond Turner's "Truth and Modality for Knowledge Representation"
book. The upshot is that only fairly weak operators
can be handled consistently using predicates
over reified sentences.

Quine's stratified approach is called NF,
and although it has never been proved consistent,
a fairly powerfull variant called NFU has.
The web resource for NF/NFU related systems is

http://math.boisestate.edu/~holmes/holmes/nf.html

Note that in NF/NFU the stratification
is with respect to the use of the set abstraction algorithm,
not negation or reification.
That, however, does not change the fact that
stratification is a good idea here.

Good luck

D

Sandro Hawke writes:
 > 
 > 
 > I've done some more reading on the paradoxes of self-reference.  I've
 > learned a few things, and unlearned a few things.  I'll be somewhat
 > self-referential and annotate my own message.
 > 
 > The short form: If we're going to do a same-syntax semantic-extension
 > of RDF to include negation, we will need to limit negating
 > self-reference.  We can do that in the semantics of our
 > reification/extension vocabulary.  So far, I know of three ways to do
 > it: (1) as in KIF98 [11], (2) stratification, and (3) as in KIF3 [9].
 > (I talk about these more below.)  The choice among these seems to
 > involve a tradeoff between implementation complexity and language
 > expressiveness. 
 > 
 > Thanks to Dan Connolly, Tim Berners-Lee, and Lynn Andrea Stein for
 > help with these ideas; any mistakes are almost certainly mine.
 > 
 > 
 > > In sketching out a vocabulary (ontology) for reifying logical
 > > statements in RDF [1], I've come across a few different approaches for
 > > avoiding the self-reference paradoxes that arise in a naive approach.
 > > 
 > > To stumble across a Liar Paradox [2] [3] we need only introduce a
 > > class naive:FalseStatement, which includes all the rdf:Statement
 > > objects which are not true.  Then we can say
 > > 
 > >   _:x rdf:subject _:x.
 > >   _:x rdf:predicate rdf:type.
 > >   _:x rdf:object naive:FalseStatement.
 > > 
 > > which says that there exists an rdf:Statement which says that it is
 > > false.  The truth value of that statement is now ill-defined.  If we
 > > were to suppose it was true, we'd learn it was false.  If we were to
 > > suppose it was false, we'd learn it was true -- at least following
 > > classical notions of logic.
 > >
 > > How can we avoid this situation?
 > > 
 > > 0.  Avoid RDF.   :-)    
 > 
 > Actually, this doesn't help at all.  These issues arise in all systems
 > allowing self-reference, not just in RDF.  The web is full of
 > references (links), so it's only natural that the SemWeb would be full
 > of references, and that some of them would loop.  People want to
 > publish information about other people's information.  The webized
 > liar paradox might be a web page with the text, "The information on
 > this page is false."  People are going to want to use the SemWeb to
 > rate the veracity of web pages; what should agents make of ring of
 > page ratings?
 > 
 > > 1.  Instead of naive:FalseStatement, use nonlooping:FalseStatement,
 > > the class of all rdf:Statements which are at once both (1) not true
 > > and (2) non-looping.
 > > 
 > > To define "non-looping", let's use a stratification approach, where
 > > statements are "first-order" if none of their elements (subject,
 > > predicate, or object) is a statement; they are second-order if they
 > > are first-order or if one or more of their elements is a first-order
 > > statement; ... they are Nth order if each of their elements are of
 > > order N-1 or less.  Nonlooping statements must be of some finite
 > > order.
 > 
 > I understand this kind of approach is how W.V. Quine approached
 > Russell's paradox, in contrast to Russell's approach of using types
 > for classes. [6]   I also understand that Quine's approach has not
 > been proven consistent [6], which worries me.  
 > 
 > > This is the approach I feel most confident in.   With this approach
 > > the triples
 > > 
 > >   _:x rdf:subject _:x.
 > >   _:x rdf:predicate rdf:type.
 > >   _:x rdf:object nonlooping:FalseStatement.
 > > 
 > > are simply false.  A document which asserts those three triples is
 > > false.  They say that such a rdf:Statement exists, but it does not. 
 > 
 > Ooops, I said that wrong.    The "rdf" namespace should be the
 > "nonlooping" namespace.   But I'm going to call it "strat" instead of
 > non-looping, to keep it distinct from the KIF approaches to preventing
 > loops. 
 > 
 >      _:x rdf:type strat:Statement.         # implied by RDFS
 >      _:x strat:subject _:x.
 >      _:x strat:predicate rdf:type.
 >      _:x strat:object strat:FalseStatement.
 > 
 > These four statements say that there exists a stratified statement
 > which has a subject which is itself.  (The second triple alone
 > actually does this.)  And that's not true -- there can be no
 > stratified statements which have themselves as a subject.  The second
 > triple above is false.
 > 
 > Suber [7] would argue, I think, that I am making the liar paradox a
 > veridical paradox (much like Russell's), so that I can dispatch it
 > more easily as a simple contradiction.  It is not what he calls a
 > "genuine paradox", although in other situations the liar paradox is
 > one. 
 > 
 > Does this work in the open, distributed world of the semantic web?  I
 > think so.  An agent making inferences does so on the basis of
 > knowledge it holds; only when it knows that a sentences is higher
 > order than all its parts will it be free to process an assertion of
 > that statement.  If the relative ordering of the sentence to its parts
 > is not known, the statement will not be known to be stratified, and so
 > cannot be asserted.  (Not that this does not require ever knowing the
 > absolute order of anything -- we don't need to know which object are
 > not sentences -- we just need to know that sentences which assert a
 > loop exists in a stratified sentence are false.)
 > 
 > > I wouldn't expect most RDF software to recognize this fact -- it would
 > > handle documents with these triples like any other documents, unless
 > > it happened to understand nonlooping:FalseStatement.  Then it would
 > > probably do some different processing, but without an RDF processing
 > > model defined, it's hard to say what that might be.   
 > > 
 > > Occasionally there are versions of RDF(S) floated (by the WG) which do
 > > specify a way to have RDF graphs with no models; this graph would be
 > > free to have models at the RDF(S) level, but would not have any models
 > > for an observer who happens to know the meaning of nonlooping:FalseStatement.
 > > 
 > > 2.  Use safe:FalseStatement, the class of all rdf:Statements which are
 > > both (1) not true, and (2) will not lead to a paradox.
 > > 
 > > This sounds fine, but I'm not sure how to formalize (2).  I heard there
 > > was some such approach in one version of KIF's wtr predicate, but I
 > > can't find it.   If (1) starts to pan out, then more work on (2) would
 > > probably be worthwhile.
 > 
 > I found it.  I was confused because it's in the earlier KIF
 > documentation, called simply "true" [kif3, 9], before they decided
 > [10] to turn it into "weakly-true" (wtr) in the draft proposed ANSI
 > standard [kif98, 11].  I haven't followed the references given in
 > [9], but I imagine the theory is sound, even if it is hard to
 > implement (as claimed).
 > 
 > This gives us three possible approaches.  Reified sentences in a logic
 > with negation could
 >    1.  exclude sentences which refer to sentences (kif98)
 >    2.  exclude sentences which have reference loops (via
 >        stratification) 
 >    3.  exclude sentences with non-atomic negation, or whatever
 >        KIF3 is saying.
 > 
 > > 3.  Avoid negation.  Stick to a positive logic, as N3 does.  Fine, but
 > > I'd like more.  This is kind of a non-answer.  (I did some work in
 > > this direction, calling it Positive Triples Logic, before I decided
 > > option (1) was feasible.)
 > > 
 > > 4.  Put negation at a higher level.  Have your base logic be positive
 > > as in (3), but suggest people who want negation define it and the rules
 > > for it.  As with TimBL's N3-based partial DAML-validator [4], the
 > > rules can not make the system inconsistent; instead, they lead to a
 > > triple which is used as an indicator of inconsistency by some agent or
 > > user.
 > > 
 > > My sense is that this doesn't help.  The rules (like modus tollens)
 > > for doing inference based on negation information will either land us
 > > back in the land of ill-defined truth values (at their level), or will
 > > have to address the problem in some other way (such as requiring
 > > non-looping statements).
 > > 
 > > 5.  Use intuitionist logic [5].  I've heard this one, but I don't
 > > understand it well enough to see how it helps.  I can almost see
 > > constructivism giving the same kind of stratification as I defined in
 > > (1), but I'm a long way from seeing the details.  Anybody care to
 > > explain?
 > 
 > As I understand it, intuitionistic logic, not having the Law of the
 > Excluded Middle (LEM) does not fall prey to the liar paradox.  So at
 > first this looks promising, but it turns out there are other
 > self-reference paradoxes, such as Curry's paradox, which demonstrate
 > that self-reference is a problem even without LEM.
 > 
 > 6.  Paraconsistent logics, and other non-classical logics also promise
 > to help, but I think we're a long way from settled here.  Restall [8]
 > seems to cover the issues fairly thoroughly, and the results don't
 > look good.  (This approach is a broadening of approach #5 above.)
 > 
 > > [1] http://www.w3.org/2002/08/LX/RDF/layering
 > > [2] http://www.google.com/search?q=liar%20paradox
 > > [3] amusing variation: http://muhu.cs.helsinki.fi/mailing_lists/humor/msg76.h
 > > tml
 > > [4] http://lists.w3.org/Archives/Public/www-rdf-interest/2002May/0034.html
 > > [5] http://plato.stanford.edu/entries/logic-intuitionistic/
 > 
 >     yours, for a paradox-free world,
 >     -- sandro
 > 
 > [6] http://www.utm.edu/research/iep/p/par-russ.htm
 > [7] http://www.earlham.edu/~peters/writing/psa/sec01.htm
 > [8] http://citeseer.nj.nec.com/restall98costing.html
 > [9] http://meta2.stanford.edu/kif/Hypertext/node35.html
 > [10] http://logic.stanford.edu/kif/decisions.html
 > [11] http://logic.stanford.edu/kif/dpans.html
 >

Received on Thursday, 12 September 2002 17:12:01 UTC