This is an attempt to think through some topics from the philosophy of math seminar I’m attending.

One could characterize Frege’s view about the epistemology of mathematics as anti-agentive in the following sense. Frege thinks that the status of a mathematical claim as justified, at least within the areas of logic and arithmetic, do not require the involvement of any agents at all. The argument for this is his recasting of mathematical claims in terms of his Begriffsschrift. Such a recasting is possible in a slightly different form with proof theoretic concepts that were developed following Frege. One starts with a set of axioms and primitive rules of inference. A proof then consists of a sequence (or a tree) generated by a simple inductive definition based on the primitives. An axiom is a proof as is any substitution instance of an axiom. A sequence (or tree) generated by the application of an inference rule to the an existing proof is a proof, with a similar condition on substitution. Closing under these conditions generates a set of proofs. A mathematical claim is then justified if it features as the final sentence in one of the sequences in the set of proofs. 

It is important for the argument that the inferences mentioned above are not understood in psychological terms. That would undermine the thesis entirely. Rather, the rules of inferences can be seen as sets of collections of symbols. Additionally it is important that rule of inference be formally specified. That is to say that the applicability of a rule should be determinable in an entirely mechanical way, e.g. based on the geometry of the symbols in the specification of the rule. 

As long as there is a proof in an appropriate formal system of a proposition it is justified by Frege’s lights. Frege takes his point a bit farther. He thinks that for any mathematical argument, given in a somewhat informal manner, there is already a purely formal proof, entirely  agent-free, in the background corresponding to it or underwriting it. 

To make things a little sharper, the justification of a mathematical claim is given entirely by its proof. This point is made by several philosophers, but I think Benacerraf puts it nicely in “Mathematical Truth.” Proof, following Frege, is formal object, a sequence of symbols or abstract objects, or some such depending on one’s other epistemological and ontological proclivities. (Frege would want to view it not as a sequence of symbols, but as an analog in terms of abstract objects since he thought formalism was a non-starter.) Proof is, consequently, entirely agent-free. Therefore, the justification of a mathematical claim is entirely agent-free. There is simply no space for an agentive contribution to the justification of a mathematical claim on the Fregean view of mathematical justification. This idea, or at least techniques for developing it, has been developed somewhat in Hilbert and proof theoretic researchers following him. 

One of the achievements of Frege and the proof theorists consists in turning proof into a mathematical object in its own right. (Although, I suppose Frege didn’t investigate the mathematical properties of proofs qua objects much, if at all.) This makes salient the distinction made by, I believe, Kreisel between proof theory and the theory of proofs. The former is a completely mathematized approach to proof. The latter is a philosophical investigation into the notion of proof that is found in mathematical practice. Proofs in the sense of the former are rarely given while proofs in the sense attended to by the latter are wide-spread. (I’m not entirely sure I have the distinction or the attribution correct. I’m having some difficulty tracking it down.) Indeed, Frege says that hardly any proof meeting his level of rigor has been offered. The distinction offered seems like one that must be made if one is interested in getting the role of the agent back into the epistemology of math.  

There are two connected issues that I think I need to get clearer on for a better grip on Frege’s views about the epistemology of math. One is how exactly this relates to his anti-psychologism. The other is spelling out how this connects to his project of showing that arithmetic is analytic. 

Also, the above considerations, at least for Frege, only apply to arithmetic and logic. If one holds roughly this view, what does one say about geometry? We can recast geometric questions in terms of Tarski’s axiomatization, but this wasn’t open to Frege.