Peirce and proof: A view from the trees

Abstract

Using the proof of Peirce’s Law [{(x → y) → x} → x] as an example, I show how bilateral tableau systems (or “2-sided trees”) are not only more economical than rival systems of logical proof, they also better reflect the reasoning Peirce actually gives for securing the law’s acceptance as an axiom. Moreover, bilateral proof trees are readily adapted to Peirce’s own graphical notation, producing a proof system in that notation that is even more efficient and easier to learn than Peirce’s system of permissions. This is in part due to the fact that Peirce’s graphical notation is similarly bilateral. In effect bilateral proof trees in Peirce’s notation can be understood as representing the space of outcomes for a game very much like what Peirce envisions as his endopereutic, and they embody insights of certain expressions of the pragmatic maxim that Peirce offers around 1905. Taken together, this suggests to me that Peirce would have embraced such a system of logic, and so I find it especially unfortunate that he was evidently unaware of Lewis Carroll’s pioneering efforts to develop tree-like proof systems to solve logical puzzles with multiliteral sorites.