Re: Identity implies logic

From: "Pat Hayes" <phayes@ai.uwf.edu>

> >http://robustai.net/mentography/lawsOfLogic.gif
>
> What is unclear (to me) is how your graphs express propositions, and
> what propositions they express.

Every triple is a proposition with the proviso that in some cases it takes
multiple triples to express one proposition.  For example if we say in N3
syntax { :s :and :x, :y }, that translates into two triples {:s :and :x}{:s
:and :y}  ... but I would not consider each of those triples separately to
be a proposition.  In KIF I think that would be the single proposition (and
x y).  I don't know how to name propositions in KIF, so I don't know where
to put the ':s'.   In most other cases the propositions of KIF translate
directly to triples as you yourself have stated elsewhere actually giving
the translation formula.  Does that help?

> I don't understand the rules by which
> the part of the graph are supposed to be combined.

Well let's just resort to N-Triples as defined by
http://www.w3.org/2001/sw/RDFCore/ntriples/

Then, hopefully, we both can agree what a labeled directed graph (LDG) is
... it has nodes and directed arcs, each of which is labeled ... in a RDF
LDGs the arcs are labeled with property nodes.  A mentograph is just a LDG.
There is a one to one mapping between RDF N-Triples and the arcs in a
mentograph.   There is a one to one mapping between each node in the
mentograph and every unique subject in the N-Triples.   The name of the node
is placed inside the box of the node in the mentograph for human
readability, however it is not part of the mathematical construction.   The
names inside the box would correspond with your V  in the Model Theory [1] .
Does that help ?

[1] http://www.w3.org/TR/2001/WD-rdf-mt-20010925/

Occasionally my mentographs include the shorthand  shortcuts which are
described at:
http://robustai.net/mentography/MentographySemenglish.gif
The only substantive difference that I know of between a mentograph and a
RDF graph, is that the arcs of a mentograph can have an optional sequence
attribute associated with them.  If this (seq) attribute is present in the
arc, it means that all arcs with the same subject and property must be
considered to exist in the order specified by the integer in the seq.

> >  Especially since it just represents an
> >instance of the kind of graphs that your MT has supposedly given meaning
to.
>
> No, the MT applies to RDF graphs. Your mentographs do not appear to
> be RDF graphs.

Apart from the difference I mentioned above about sequence, what other
difference do you see?

>In fact, the MT shows that things like implications
> *cannot* be represented in RDF graphs

Well would you agree that if we can represent an implication in N-Triples,
then we can represent it in a RDF graph?

>(this follows, for example,
> from the subgraph lemma.)

I'll need to noodle on that before I say anything stupid.

>>>>Seth: Well, ok, (though i'd like to see a proof that LEM can be derived
>>>>from LNC just to close the gap in my education).
> >>
> >>  By deMorgan's law:
> >>  not (P and (not P))  =  (not P) or (not (not P))
> >>  By double negation:
> >>  (not P) or (not (not P))  =  (not P) or P
> >>  and then permute the 'or'
> >
> >Woops, maybe we better back up here ... let me quote from Suber at:
> >http://www.earlham.edu/~peters/courses/logsys/pnc-pem.htm
> >
> >      "Under De Morgan's theorem, the PNC can be transformed
> >       into the PEM and vice versa, but this only shows that
> >       De Morgan's Theorem presupposes the PEDC.
> >       (Logics that deny the PEM must deny some forms
> >       of De Morgan's theorem.)
> >
> >       "The PNC and PEM need not be equivalent in n-valued
> >       logics when n > 2"  ...
> >
> >      "If we use a standard two-valued logic, the three principles
> >      are already present even if they do not appear as axioms.
> >      The three principles can be proved in such a logic, but
> >      any such proof would be viciously circular."
>
> For the record, I disagree with that last claim. Obviously Suber
> takes a formalist position in mathematical philosophy, which I do
> not. The proof of these principles can be given on semantic grounds
> in the metatheory, and they are then by no means circular, even
> mildly so.

Well I'd like to be a fly on the wall were you and Suber to discuss that.  I
cc'd him just in case such a discussion is in the cards.

> But this is an arcane debate in foundations of mathematics, and has
> no significant bearing on the semantic web.

Perhaps, perhaps not ... it depends on the political ramifications of the
MT.

> Well, for everyone who proposes to use RDF, DAML+OIL, etc., we can
> make that commitment, and indeed do. You (or anyone) are free to
> invent a multivalued version of RDF, of course, if you prefer it.

Nope, I don't need to invent anything.   RDF already exists and is
compatible with multivalued logics, AFAIK.   That no model theory has been
written for such deviant logics does not mean that some program can't
respond to a set of RDF triples according to whatever brand of entailment
the author (or owner) of the program intends.

> >So I take it that we need to keep PNC and PEM separate until we commit to
> >classical binary logic and committing to binary logic is not something we
> >can just do willy nilly for everybody with a single stroke of the pen
> >  .. can we
> Yes,

Agree ... because you have done it :)

>>... should we ?
> and yes.

Well I think this depends on the political ramifications of  this binary
logic Model Theory.  The Internet has thrived on there being no authority
that can say something like:  "your file is meaningless" ...  the way you
just said "RDF cannot represent implications".  The Model Theory provides
the liturgy for Priests of logic to stamp an RDF file as kosher or not.
That is something that rubs me the wrong way.

Now  let me ask a technical question:  .. correct me where I go wrong
because this leads me to an absorb conclusion:   The MT assigns an
entailment (True or False) for every possible triple based upon a Vocabulary
... right?   If the set of triples of the graph does not entail a triple,
then that triple is called False in the interpretation of the graph ...
right?   So here is my problem ... I assert a single triple in my graph ....
something like {:Mary :loves :John}.  The MT seems to say that my assertion
means that {:John :loves :Mary} is False.   But that is absurd, my triple
said no such thing ... help me .. where did I go wrong?

> >   Let me ask you a straight question:  Does the MT commit
> >us to (classical?) binary logic ?
>
> To two-valued logic; yes, of course. That is obvious from the
> semantic conditions: an interpretation always assigns one of the
> values true or false to any RDF graph.
>
> >  > Now, what was the connection between LEM/LNC and Identity, again?
> >
> >Identity => PEM and PNC
> >
> The trouble with any assertions like this is, that one needs to know
> what logic the proof of the implication is going to use. Since you
> and Suber are rejecting two-valued logic, I'm not sure what would
> count for y'all as a demonstration. Since all three of these (LEM,
> LNC and Identity) are all tautologies in normal logic, its kind of
> hard for me to know how to set about showing which of them follows
> from which others.

[...snip...]

> We can't use any logic in that context until we discover what we are
> both talking about.

I couldn't agree more :))   ... see my closing note below.

>RDF and DAML+OIL make a basic assumption that
> URIs are a universal naming convention; if you and I both use the
> same URI, then we are referring to one thing, whether we like it or
> not.

Were that true, we would be living in a much different world.  Even in
standards land, what a URI refers to,  is not a cut a dried thing ... there
is much confusion as you well know.  When people bookmark a URI and then
describe that bookmark with RDF are you quite sure they will all be talking
about the same thing?

> > I see you have nicely excised the bug-a-boo of time from the MT.  But
> >time is not the only problem, Identity is a problem too .... isn't it ?
>
> Actually, no, I don't think it is.

Well using your own words above:  "We can't use any logic in that context
until we discover what we are both talking about." .... That and only that
is all I am saying too.  Thing is, we certainly *can* send each other useful
RDF statements regardless of that contingency.   You, and all logicians I
have ever known, always assume that you are in a logical space where
identity holds before you roll up you sleeves and start doing logic ... but
that assumption does not hold on the semantic web ... nor will it hold by
edict ... nor would that be a good thing ... well at least I don't think it
would be a good thing.  I am simply lobbying to eliminate that assumption
from the model theory of RDF.  In order for us to do that,  I think we need
to be able to identify sets of statements and to specify what kind of logic
holds within those sets... but that is not in the Model Theory.

Seth Russell

Received on Tuesday, 2 October 2001 21:01:57 UTC