Wise words from yesteryear

Peter J. Ross, a notorious poet and a troll, once claimed my posts in Usenet are almost always either enjoyable or informative, and often both. I wouldn't know about such matters, but it is certainly true that Torkel Franzén's contributions, in the news and on various mailing lists, were virtually always enjoyable and informative. I've been scrounging the archives of FOM for nuggets of insight and wisdom, and stumbled upon an old message from Torkel. Neil Tennant repeated the standard line, that in order for a theory to be epistemologically relevant axiomhood must be decidable, which prompted the following reflections from Torkel:

  Although I've said similar things myself often enough, it
only now occurs to me that this isn't really convincing, if
one takes the epistemological motivation seriously.

The basic premise is that we need to able to decide whether
a proposed proof is a proof. I will accept this basic premise,
although it is not an immediate consequence of the necessity
of avoiding an infinite regress in proving theorems. (Merely
being able to verify that a correct proposed proof is a proof,
while coming to no conclusion in the case  when it is not a
proof, would be sufficient to avoid such a regress.)

But then it's not enough that the set of axioms *is* recursive.
To be able to check a proposed proof we also need to know that
the set of axioms is recursive, and in fact we need to have an
algorithm for deciding whether or not a formula is an axiom.
Such  an algorithm, then, is an implicit part or parameter of
the proof,  from an epistemological point of view.

To understand what Torkel's on about, consider the following example, which he himself provided in a later post. Let T be the theory with all arithmetical truths with less than k symbols as axioms. Since there are only finitely many such truths, axiomhood is obviously recursive (and hence decidable). This fact is however of no help whatsoever in deciding whether a given sentence is an axiom or not, and consequently whether a sequence (or a labeled tree or whatever) p is a proof or not -- for sentences with less than k symbols deciding whether it is an axiom or not is equivalent to finding out whether it's true.

The upshot of this is that the usual epistemological argument for requiring theories to be recursively axiomatisable is in fact wanting; by the argument we are only warranted to require recursive enumerability of the axioms. That is, in order to recognise a formal proof p as a proof in a recursively axiomatised theory T, we must have at hand an algorithm for deciding axiomhood (and apply that algorithm to the premises of p, verifying they are indeed axioms) -- the recursiveness of the axioms of T and p in itself are insufficient. Similarly, in order to recognise a formal proof p in a theory T with a recursively enumerable set of axioms, we must have at hand an algorithm for listing the axioms, and a computation that in fact yields the axioms used in p. There is no apparent epistemologically relevant distinction between these cases. As Torkel writes

  If the set of axioms is not recursive, but recursively
enumerable, the property of being a proof will still be
decidable, if we regard as part of the proof the generation,
using an algorithm for enumerating axioms, of the axioms
actually used in the proof. The basic premise, then, is
satisfied even if we only require the axioms to be
recursively enumerable.

I therefore think that what the epistemological argument
supports is only the need for the set of axioms to be
recursively enumerable. A slightly different formal model
of proofs is presupposed - one in which a proof incorporates
an algorithm for generating axioms together with computations
generating the axioms used, rather than just incorporate an
algorithm for deciding axiomhood - but I see no good reason
why the latter model should be preferred.

Of course as everyone knows we can always replace a recursively enumerable set of axioms with a (very unnatural) recursive set with the same deductive closure, by Craig's trick. It is still of independent interest whether epistemological considerations alone justify restricting our attention to recursively axiomatised theories.

Many an interesting observation may be found buried in the archives of FOM and those of Usenet newsgroups. (Alas, it seems Google has decided to utterly wreck its Usenet search function, rendering it almost unusable.)