Pólya (1949) gave an example of a proof that is perfectly correct, yet deeply unsatisfying, due to the existence of a “deus ex machina” step. He suggested that deus ex machina steps are problematic because readers cannot grasp their “appropriateness”, i.e., they cannot grasp how such steps are “connected with the purpose” or how they “bring us nearer to the goal” (Pólya 1949, 685). His analysis, however, stopped there. In this talk, I will deepen Pólya’s analysis by investigating the proving activity that corresponds to a proof, that is, by putting the proving agent back into the picture. In particular, I will show how Bratman’s (1987) theory of planning agency can be used to provide a precise account of how a step may be “connected with the purpose” or “bring us nearer to the goal” (Pólya 1949, 685). (This talk is joint work with Yacin Hamami.)
Michael E. Bratman (1987). Intention, Plans, and Practical Reason. Harvard University Press, Cambridge, MA.
Pólya, G. (1949). “With, or without, motivation?”. The American Mathematical Monthly, 56(10), 684-691.