[FOM] Re. What is a proof?

[Michael Detlefsen]

Continuing the discussion with John Baldwin concerning what a proof 
is, Steve Simpson wrote:

"To spell it out, what I am proposing is that we make your vague
distinction precise, as follows:

   Definition.  Let T be a theorem of second order arithmetic, Z_2.
   Let P be a formal proof of T within the formal system Z_2.  We say
   that P is *explanatory* if the conjunction of the fintely many Z_2
   axioms used in P is logically equivalent to T, over RCA_0.

This rigorous notion of *explanatory proof* may not do everything you
want it to do, but it is good enough to make some useful distinctions."

I don't deny that this may be enough to provide some useful 
distinctions, but it also seems to leave some important questions 
unanswered. Here are a few:

1. Using this characterization, does every theorem T of Z_2 have an 
explanatory proof (i.e. is every theorem of Z_2 such that there is a 
set of axioms A_T of Z_2 such that A_T is equivalent over RCA_0 to 
T)? Or are there theorems T of Z_2 all of whose proofs require sets 
of axioms of Z_2 that are strictly stronger (over RCA_0) than T? If 
the latter, do these theorems then have NO explanatory proofs? Is 
that an acceptable consequence for you? (I am not thinking, of 
course, that your view is that every theorem of Z_2 has an 
explanatory proof. I would assume, for example, that you would not 
take the axioms to have explanatory proofs. My question, then, is 
whether there are non-axiom theorems T of Z_2 such that there are no 
explanatory proofs of T, and whether this is an acceptable 
consequence for you?)

1a. Relatedly, consider a system Z_2* such that Z_2 and Z_2* have 
exactly the same theorems, but have different sets of axioms. 
Assuming your general reverse mathematical approach (to characterize 
the notion of an explanatory proof in terms of a proof that uses 
axioms that are equivalent over some appropriate base theory to the 
theorem to be proved), how do I decide whether to identify an 
explanatory proof of a theorem T of Z_2 with the axioms of Z_2 or the 
axioms of Z_2*? On your view do I even HAVE to decide such a thing? 
(If you allow that each different axiomatization of a theory has its 
own explanatory proofs, then it seems you don't think the axioms used 
play much of a role in making a proof explanatory. If, on the other 
hand, you think some axiomatizations are "privileged", how would you 
justify this?)

2. What are the characteristics of RCA_0 that make it the right 
reductive base for explanatory proofs in Z_2? Is RCA_0 unique in this 
respect, or is it one of possibly more than one such base?

3. Consider proofs of theorems of Z_2 that make use of axioms (e.g. 
second-order induction or comprehension) which at the first-order 
level would be axiom schemata. Is the explanatory quality, content or 
characteristic of a proof always completely attached to the 
particular instance of the axiom that is used? Or should we take part 
of the explanatory quality, content or characteristic of a proof, at 
least in some cases, to attach simply to the fact that the instance 
of the axiom used is an instance of INDUCTION, say, or of 
COMPREHENSION?

I have other questions, but these will do for now.

 From a cloudy and chilly South Bend,

Mic Detlefsen