ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Triad Logic

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: John F Sowa <sowa@xxxxxxxxxxx>
Date: Tue, 25 Jun 2013 22:04:53 -0400
Message-id: <51CA4C45.4020505@xxxxxxxxxxx>
On 6/25/2013 7:58 PM, Obrst, Leo J. wrote:
> Given his responses on the public-lod list, I think he's blowing smoke.    (01)

I agree.    (02)

Hayes and Guha specified the semantics of RDF as a subset of the CL
model theory.  Pat summarized his suggestions for generalizing RDF
to support full FOL:    (03)

PH
> Give [users] a way to use JSON that makes in, invisibly, into a fairly
> compact notation for RDF is a good start. Tweaking the RDF data model
> so that it becomes a variant of Peirce's existential graph notation
> (see http://www.slideshare.net/PatHayes/blogic-iswc-2009-invited-talk )
> [makes it a complete notation for FOL.]    (04)

I went to Gregg R's site:  http://blog.mobileink.com/    (05)

He uses logical symbols and rewrite rules to make it look impressive,
but he concludes    (06)

GR > If we want our little Triad calculus to reflect RDF, we obviously need
> to support literals.  I'll get to it eventually.    (07)

In other words, he was blowing smoke.  In his talk, Pat showed that the
only addition you need to RDF is an enclosure that negates any graphs
or subgraphs inside.  That was Peirce's addition to his original
relational graphs that created full FOL.    (08)

GR
> Historical note:  this rule is cribbed directly from the great Gerhard 
>Gentzen,
> who first came up with the idea of introduction and elimination rules as
> determining the meanings of the logical constants.    (09)

No.  Peirce came up with the idea about 30 years earlier.  In fact,
Peirce's rules of inference for existential graph are a *simplification*
and *generalization* of Gentzen's system of natural deduction.  Peirce
didn't anticipate Gentzen's system, he *improved* it.    (010)

For Peirce's own tutorial on existential graphs with my commentary and
with a proof that Gentzen's version is a special case of Peirce's, see    (011)

    http://www.jfsowa.com/pubs/egtut.pdf    (012)

In Section 6, I also prove some interesting theorems.  Among them is the
fact that Robinson's rules for resolution are derived rules of inference
from Peirce's.  From that, I show that any proof by resolution can be
converted to a proof by Peirce's version of natural deduction just by
negating each step and reversing the order.    (013)

John    (014)

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (015)

<Prev in Thread] Current Thread [Next in Thread>