Naturalizing Deduction

This project explores how mathematical faculties were understood in new ways through the lens of modern digital computing in the field of automated reasoning. The field developed throughout the second half of the twentieth century with the goal of programming computers to prove mathematical theorems. Some practitioners working in this field imagined that computers and human minds were alike in kind and could therefore be programmed to produce proofs as people do. Others thought that the promise of computing lay in fact in their difference from us—specifically their ability to follow rules further and faster and more accurately than unaided human mathematicians were able. In fact, some practitioners of this field imagined whole new logics, unconstrained by the limitations of human psychology and human practice, that computers could work with to solve problems and prove theorems in new ways. But there were those within the field who thought that human-oriented logics should not be so quickly dismissed. One stronghold of anti-resolution research was the University of Texas at Austin, under the direction of mathematician Woody Bledsoe. Bledsoe believed that computers should not become black boxes carrying out reasoning and problem-solving that people could not read, understand, and unpack. He eschewed computer-oriented methods, in spite of their power, advocating instead for automated systems based on what he called “natural deduction” that would keep human understanding and human reasoning at their core. This project explores what was meant by “natural” in natural deduction and the logical traditions, views of human practice, and of machines that informed it.