The Epistemology of Computer-Mediated Proofs

Abstract

Epistemology includes in large part investigation of the conditions by which rational human knowledge and belief, of the propositional variety, can be secured. Our particular instance of this investigation arises from the stipulation that a human (a) receives a partial or complete formal argument/proof (A ) for/of a conclusion ϕ, where some computing machine ℳ “stands between” or mediates a’s receiving A and ϕ. The mediation can take any number of forms, ranging from the simple and mundane (e.g., a is a teacher who types in to a text-editing system a proof of some easy theorem for a math class, and then prints out the proof for subsequent study and presentation to the class) to the exotic and famous (e.g., a receives a too-big-to-survey printout of a computer-generated proof of the four-color theorem). Under what conditions is it rational for a to believe ϕ? Once we have erected at least a reasonably precise framework for understanding the structure of arguments and proofs, classifying computing machines, ranking strength of knowledge and belief, and distinguishing at least roughly between types of computer mediation, this result, as we indicated, is a framework in which this pair of questions (and other, related ones) can eventually be answered.