FOM: pathologically recursive axiomatizations

[Neil Tennant]

In an entirely accurate response to an earlier question of mine, Torkel
suggests the following recursively axiomatized theory:

Choose k sufficiently large. Take all true sentences in the language
of PA of length < k. 

He says this should solve my favourite open problem. So what we have
here is a recursive (but only because finite) set of axioms for a
fragment of Th(N). This is intended to show that the usual requirement
that one's set of axioms be recursive is somehow misguided.

OK, my favourite open problem is Goldbach's Conjecture (GC). I choose
k=length(GC)+1. My finite (hence, for the classical logician,
recursive) set of axioms is

	A =df {P|P is true in N and length(P) < k}.

I believe that GC is true in N. 
Am I then allowed the following proof of GC?:

	GC	(Assumption---available axiom)
    So, GC	(Conclusion)

Presumably not, since even if my belief is correct, the proof of GC
just given "from" this classically recursive set of axioms
(containing, ex hypothesi, GC) will fail to convince any person who
does not share my belief that GC is true.  Indeed, the proof will fail
to convince *me*, since I am still seeking suasive *grounds* for my
belief in GC.

There are, then, two objectionable things going on here in Torkel's example.  

(1) The 'thin', classical notion of recursiveness, entailed by the
mere fact of finitude of the set in question, is not rich enough. In
order to establish genuine recursiveness of the set A of axioms it must
be possible to exhibit an algorithm for deciding membership in A. It
is not enough simply to know that there is a finite upper bound on the
size of A.  Rather, one should be able to define A by means of some
*decidable* condition F on its members:

	A =df {P|F(P)}

The would-be condition "length(P) < n & P is true in N" will not do,
since truth in N is not decidable.

(2) Whatever happened, anyway, to the venerable idea that one's axioms
should be self-evident, or certain? (I do not mean this
solipsistically. What is obvious for one person may be highly
non-obvious for another. The self-evidence or certainty must be
communally agreed upon---as is indeed the case with all well-known
axiomatizations of major branches of mathematics, such as geometry,
arithmetic, the theory of real closed fields, etc.) If we add the
requirement of 'self-certification' then (even if we do not strengthen
the recursiveness requirement along the lines just suggested) we
clearly rule out Torkel's pathologically 'recursive' (only because
finite) axiomatization.

If we *combine* the decidable-membership condition with the communal
self-certification condition then (I think) we have something
reasonable. For then one can reasonably guarantee that any proof (from
such axioms) settling one's favourite open question will not only
provide oneself with the justification sought for one's conjecture,
but will also persuade any other member of the relevant community
(for all of whose members the axioms are self-certifying) that the
proof's conclusion is true.

Neil Tennant