[Top] [All Lists]

Re: [ontolog-forum] Fwd: Breaking News: Google supports GoodRelations

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Alex Shkotin <alex.shkotin@xxxxxxxxx>
Date: Wed, 10 Nov 2010 11:04:40 +0300
Message-id: <AANLkTikTLg_GGVV5oxR4xuFbKRgWNLjK1qkdii_TC9j7@xxxxxxxxxxxxxx>
JS: "Bottom line:  God made FOL, and Peirce was his prophet."

Under bottom line: And people prove theorem that the tower of Babel may be build. And begin they. And God punish them by NLs.


2010/11/10 John F. Sowa <sowa@xxxxxxxxxxx>

That paper isn't available on the WWW:

> Well, but for a non-burning bush origin for FOL, see: Ferreirós, José
> (2001), "The Road to Modern Logic-An Interpretation", Bulletin of
> Symbolic Logic 7 (4): 441–484, doi:10.2307/2687794,
> http://jstor.org/stable/2687794 .

But as Kronecker said in 1886, "Die ganzen Zahlen hat der liebe Gott
gemacht, alles andere ist Menschenwerk". [The dear God made the
whole numbers, everything else is the work of man.]

I believe that one can make a very strong case that FOL can be
considered the equivalent for logic as the natural numbers for
mathematics.  It is a subset of every natural language, and it
is simpler to specify than any of its subsets.

In any case, the paper you cited is not available on the WWW.  But the
abstract seems to discuss the work that Peirce did in the years from
1897 to 1906, but everybody else ignored:

> Among the latter, one may emphasize the spirit of modern axiomatics,
> the situation of foundational insecurity in the 1920s, the resulting
> desire to find systems well-behaved from a proof-theoretical point
> of view, and the metatheoretical results of the 1930s. Not surprisingly,
> the mathematical and, more specifically, the foundational context in
> which Firs-Order-Logic matured will be seen to have played a primary
> role in its shaping.

First of all, FOL was born mature in the versions by Frege and Peirce.
It is true that Frege had a better formalized axiomatization in 1879
than Peirce had in 1885.  But their versions are equivalent to every
version invented since then.

I certainly agree that the axiomatization by Frege, a version of
which Whitehead and Russell adopted for PM, was not bad for 1879,
but it was horribly cumbersome.  And the version presented in PM
probably made more people hate logic than any other system ever
inflicted on poor, innocent students.

But in 1897, Peirce developed the existential graphs, which have
the simplest axiomatization, proof procedure, and model theory
ever discovered:

 1. The only axiom for EGs is a blank sheet of paper, and Peirce's
    rules of inference are a streamlined version of natural deduction,
    which Gentzen invented over 30 years later.

 2. Peirce also invented a very simple and elegant model theory for
    EGs, which he called _endoporeutic_ (for outside-in evaluation).
    Nobody understood Peirce's endorporeutic until Hintikka's
    student Pietarinen showed that it was a version of Game
    Theoretical Semantics.

 3. Every other common axiomatization and proof procedure invented
    for FOL can be shown to be derived theorems or derived rules
    of inference from Peirce's system.

 4. But as Frithjof Dau showed, Peirce's rules are strictly more
    powerful than the other common proof procedures: certain proofs
    that take exponential time with those methods can be proved
    in polynomial time with Peirce's rules.  (The case he showed
    was for cut-free proofs with Gentzen's clauses, but there
    would be similar kinds of proofs for other cases as well.)

For a brief summary of Peirce's system, see his own tutorial:


Bottom line:  God made FOL, and Peirce was his prophet.


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
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (01)

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