[FOM] Animated Proofs

[Jon Awbrey]

Charles Silver wrote:

 > Sorry, can't read *all* the URls, but I haven't seen any
 > displaying his [Peirce's] neat method of using the eraser
 > on circles, etc.  Great on a black (white) board.
 > How about launching some to generate FOM interest?

Maybe you mean the sort of picture that one sees here:

Frithjof Dau's animated Alpha Graph proof of Leibniz's Praeclarum Theorema:

http://web.archive.org/web/20070706192257/http://dr-dau.net/pc.shtml

(I had to use the WebArchive version here, as the current page freezes up.)

Those are nice pictures, but I found early on that the planar embedding imposes
certain limitations on the efficiency and extensibility of the graphical syntax.
Peirce himself experimented with the idea of pasting paper bridges on the plane
of representation, but I gather that he did this mostly just to handle the crossing
"lines of identity" that he used to bind variables in his Beta Graphs for predicate
logic.  Spencer-Brown, in his revival of Peirce's Alpha Graphs, endeavored to escape
the limitations of the plane through the use of worm-hole-like devices to augment the
genus of the medium -- but I can't speak to that.

 > By the bye, Peirce's law is supposedly the only propositional sentence
 > without any negation symbols that requires an indirect proof (in a natural
 > deduction system: MP, MT, C, Reductio, etc.)  Would be nice if someone were
 > to provide another (without using the law itself to create a longer sentence
 > and perhaps using only two propositional letters.   Okay, make it three.

That raises a host of issues that I will have to save for another time.

Jon Awbrey

--

inquiry list: http://stderr.org/pipermail/inquiry/
mwb: http://www.mywikibiz.com/Directory:Jon_Awbrey
knol: http://knol.google.com/k/-/-/3fkwvf69kridz/1
oeiswiki: http://www.oeis.org/wiki/User:Jon_Awbrey