FOM: decidability of sets of axioms

[Neil Tennant]

There's something that puzzles me about the orthodox conception of an
axiomatization after the foundational work of the 1930s, and especially since
Church's undecidability theorem for first-order logic.  I'll confine myself
in these remarks to first-order logic and theories.

It's especially important to mathematicians for their set of axioms (in any
given area, such as arithmetic or geometry or set theory) to be decidable
[= recursive, assuming Church's Thesis]. The reason is obvious: one needs
to be able to *tell*, effectively, when a proof establishes a theorem of the
area in question; and for this, one needs to be able to determine, of each
premise of the proof, whether it is a permissible axiom. All this has to be
effective. (By a premise of a proof I mean an undischarged assumption, on
which its conclusion rests.)

But it's equally important (at least, I think it is) to be able to tell when
what has been proved is a genuinely informative, mathematical claim about the
domain in question, and is not simply a logical truth in its own right. So we
want at the very least (1) to avoid using as premises in a mathematical proof so-called `mathematical axioms' that are themselves logical truths.
We also need (2) to be vigilant about inadvertently
`slipping into logical truth' in the middle of a proof. This would happen if
one diligently proved some informative claim P and then inferred (by or-introduction) the claim (P or not-P). Failing to recognize the latter as logically true
would of course be stupid; but this is a degenerate example. One can entertain
the possibility of less glaring `lapses into logical truth' as a proof progresses.

But it's the first requirement (1) that I want to address here. Among the
infinitely many instances of the scheme of mathematical induction

	P(0) --> ( (n)(P(n) --> P(n+1)) --> (m)P(m))

will be infinitely many for which (m)P(m) is logically true anyway. So those
instances do not really tell us anything about the natural numbers. Yet they
sit there within our so-called `axiomatization' of arithmetic, defying us
[by Church's Theorem] to winkle them out.  They cannot be falsified in any
model, so they cannot tell us anything about the intended model N. So why should
they even qualify as members of our list of axioms *for arithmetic*? (After
all, we can get them by logic alone, and do not need any arithmetical axioms
to do so.)

The reason is: Church's undecidability theorem itself! Given any scheme, there
is no effective way of telling whether a given instance of it is or is not
logically true. Hence, so long as we wish to axiomatize mathematics via the use
of uniform axiom schemes, we have to simply put up with this problem.

My question, now, is a very general one for the logicians and mathematicians
on this list. Suppose we insist that the set X of axioms for any given area
be such that:

1) every member of X is true (and hopefully certain or self-evidently so)
when interpreted as a claim about the intended structure (the natural number
system; the real line; the complex numbers; the universe of sets; n-dimensional
Euclidean space; etc.);
2) given any sentence of the language, we can effectively decide whether it is
a member of X (i.e. given Church's Thesis, X is recursive); and
3) every member of X is LOGICALLY FALSIFIABLE (hence genuinely informative).

Requirement (3) is the punchy one.

Clearly, if one had an old-style axiomatization X_0 that failed to meet
condition (3), and a new-style axiomatization X that *did* meet condition (3),
one would want every informative (i.e. logically falsifiable) logical 
consequence of X_0 to be also a logical consequence of X.

Could this be ensured in general? That is, can we prove something like the
following:

Given any consistent decidable set X_0 of sentences true in M, there is
some consistent decidable set X of logically falsifiable sentences true in M
such that all logically falsifiable logical consequences of X_0 are logical
consequences of X  ?

Forgive me if I don't know enough recursion theory to see an obvious answer
right away.

Answers, anyone?

Neil Tennant