[FOM] Re. What is a proof?

Michael Detlefsen Detlefsen.1 at nd.edu
Tue Oct 28 13:06:11 EST 2003

```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

```