Re: Identity implies logic

>From: "Pat Hayes" <phayes@ai.uwf.edu>
>
>>  >Re: Identity implies logicSeth: It seems to me that if the law of
>identity
>>  >does not hold in a context, then the Law of the Excluded Middle (LEM) and
>>  >the Law of Non Contradiction (LNC) are irrelevant and cannot be used in
>that
>>  >context.
>>  >
>>  >Pat Hayes: What law of identity are you referring to, exactly?
>>  >
>>  >Seth: the formula referred to as 'Identity' on the page:
>>  >http://www.math.psu.edu/simpson/papers/philmath/node9.html
>>
>>  which is, in KIF,
>>
>>  (forall (?x) (iff (A ?x)(A ?x)))
>>
>>  OK.
>
>OK.  But now I see the wisdom of your first question, because there seem to
>be two identities here that we need be concerned with .. the identity of the
>predicates (all triples are unique) and the identity of the nodes (all nodes
>are unique) .  Could the identity of the nodes be expressed as follows?
>
>(forall (?x) (iff (?x) (?x))  .. but that looks weird ... oh well I'm lost
>here.

You probably want the basic law of identity:
(forall (?x)(= ?x ?x))

>  > >Pat Hayes: Why? I don't see the connection. (Presume you mean
>>  >LEM = P or (not P)
>>  >LNC = not (P and (not P))
>>  >right?
>>  >
>>  >Seth: right, didn't I make that clear in my mentograph?
>>
>>  No, that was not clear from the mentograph.
>
>I've relabeled my graph using Suber's terms (which I would now like to stick
>with for the duration of any dialogue on this subject).   Please reload and
>take another look at:
>
>http://robustai.net/mentography/lawsOfLogic.gif
>
>Obviously I haven't defined context in the graph, but outside of that could
>you tell me what is unclear?

What is unclear (to me) is how your graphs express propositions, and 
what propositions they express. I don't understand the rules by which 
the part of the graph are supposed to be combined.

>  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. In fact, the MT shows that things like implications 
*cannot* be represented in RDF graphs (this follows, for example, 
from the subgraph lemma.)

>
>>  >Pat Hayes:  These amount to the same thing in classical logic.)
>>  >
>>  >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.

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

>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

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.

>  .. can
>we ... should we ?

Yes, and yes.

>   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
>
>But I'm not sure that this shouldn't be:
>
>Identity <=> PEM and PNC
>
>Could you help me with that little detail ?

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.

>  > >   But can we rely on such a
>>  >classical  logic on the web ... I'm not at all sure myself whether this
>wild
>>  >west is so tamable ... are you?
>>
>>  Yes, we can rely on it precisely because it is the most reliable
>>  logic around (which is why it is 'classical'). Well, one might make a
>>  case that intuitionistic logic is safer, I guess, but I don't think
>>  that the SW is going to be much concerned with issues that arise in
>>  the foundations of mathematics. (In any case, RDF is intuitionistic,
>>  since it has no negation.)
>
>Well then, sorry,  I use the wrong word when I asked my question with the
>term 'rely'.

Well, what word should you have used?

>....
>It seems to me that the usefulness of multi valued logics is just where we
>cannot use 2 valued logic; and we cannot use two valued logic in a context
>where we are not sure if we are talking about the same things; which, if you
>are talking to guys like me, is most of the time.

We can't use any logic in that context until we discover what we are 
both talking about. 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. (Of course, you may use two different URIs to name the same 
thing, and I may not know that; but that does not involve us in 
multivalued logics, but is simply a reflection of the basic fact that 
if A knows less than B, then A is unable to draw as many conclusions 
as B can.)

>  > >Seth: For example:  If we have two different computers hooked up to the
>>  >semantic web and in one's database an apple is only known as 'apple' and
>the
>>  >other it is only known as 'orange',
>>  >
>>  >Pat Hayes:  Wait. How could you know that? That is, A is talking about
>>  >things called A#apple, and B is talking about things called B#orange. How
>>  >could you (or anyone) know they are supposed to be the same things?
>>  >
>>  >Seth:  Well we humans do this all the time.  I'm relatively sure that
>there
>>  >are stochastic processes that can ascertain after a number of
>interactions
>>  >that two tokens refer to the same thing within a reasonable margin of
>error.
>>
>>  Nonsense. That would require magical powers. Here are two tokens:
>>  AAAA
>>  BBBB
>>  which I am using to refer to some things. Go ahead, figure out
>>  whether they refer to the same thing or not. Use whatever means you
>>  like, stochastic or otherwise.  You can make as many copies of this
>>  message as you want. Give me a call when you know the answer.
>
>You missed the word 'interactions' in my response above.

No, I didn't. You are free to interact with me, or with what I said, 
or with anyone else, as much as you want. Of course you have no way 
to force me to reply, and I choose not to do so when it comes to AAAA 
and BBBB.  Now, what are you going to do?

>
>>Also, all three of these are
>>  elementary theorems in KIF, so its kind of dumb to say in KIF that
>>  they might not be true.
>
>Hmmm ... where can I see those theorems expressed ?

LEM:
(or ?p (not ?p))
LNC:
(not(and ?p (not ?p)))
Identity, see last message.

....

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

Pat Hayes
-- 
---------------------------------------------------------------------
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, 2 October 2001 12:17:44 UTC