FOM: on independent axiomatizations: a new requirement

[Neil Tennant]

The desire for a logically independent set of axioms is hard to
translate into a technically watertight requirement. It is necessary,
but not sufficient, to require of such a set A that none of its
members P is derivable from A\{P}. This rules out logical truths P as
members of A, since any logical truth is derivable from the empty set.

To see non-sufficiency of the conventional requirement just stated,
take any axiom set A such that for every P in A, P is not derivable
from A\{P}. Now take any logical truth T. Consider the new axiom set
{P&T|P in A}.  This set meets the conventional requirement; but it is
intuitively objectionable, since the logically true conjunct T within
each axiom does absolutely no work. It can be shorn away in every case
without deductive loss.

Here is a first tentative diagnosis of what was fishy about the axiom
set {P&T|P in A}, stated on the assumption that our proofs are within
a system of natural deduction (a la Gentzen and Prawitz): IT IS
POSSIBLE TO PROVE A LOGICAL TRUTH FROM THE SET OF AXIOMS BY MEANS OF
ELIMINATION RULES ALONE. Thus:

	P&T
	___ &-Elim
	 T

This is a first attempt to explicate the idea that an otherwise
'conventionally independent' set of axioms "unnecessarily harbors
avoidable logical truth". It does so when a logical truth is the
conclusion of a proof from the axioms that uses only elimination
rules.

So here is a new criterion for an independent axiomatization:

Not only must we have, for each P in A, that A\{P} does not imply P;
we must also have that no elimination-proof whose premises are axioms
from A produces a logical truth as its conclusion.

This criterion may itself have to be sharpened; for someone might come
up with an ingenious case satisfying the criterion, but which contains
something that is intuitively objectionable on other grounds. 

What I'd like to know at this point is: do any of the (conventionally)
independent axiomatizations suggested thus far for PA meet this more
demanding criterion?
 
Neil Tennant