FOM: Proof-theoretic criteria for syntheticity axiomatizations (revised)

[Neil Tennant]

I entirely concede the point that my tentative criterion for decent
axiomatic status, which I advanced only as necessary, couldn't
possibly be sufficient for ruling out the kind of "production of
logical truths by mathematical axioms" that I was trying to avoid. I
said as much when I put the criterion forward; it was only intended as
a necessary condition, not a sufficient one.

Sam's example and Torkel's example show how far one still has to go.
But I'm still interested in seeing how far one could push a
proof-theoretic criterion to rule out these pathological axioms.
Remember that I am trying to avoid mathematical axioms that let
"logical truth drop out of them" when their content is unpacked. It is
(dually) just as important to prevent refutations of logical
falsehoods from dropping out of such axioms.

With this in mind, let us take a closer look at Torkel's ~(T->~A)
where T is a logical truth. I'd like to suggest that one can
re-formulate the criterial complaint by dualizing it as follows: this
axiom can be used to *refute a logical falsehood*, by means of a proof
containing only elimination steps below each assumption occurrence of the
axiom, on any branch running through such occurrence:

       ___(1)
	T        ~T
	___________
	    #
	   ___
	   ~A
	 ________(1) 	
	  T->~A		~(T->~A)
	 ________________________
		    #	

In a normal form proof, it is the use of eliminations *on a branch
below an assumption occurrence* that "unpack the content" of the
assumption. It matters not that there are introductions within the
minor proof for the negation elimination with ~(T->~A) as major
premise.

Part of an amended criterion, then, would be: one should not be able
to construct a proof from a non-empty subset of the set of axioms,
which has a logical truth as its conclusion, and in which at least one
axiom from A has only eliminations below all its assumption
occurrences (on all branches running though them)

To be on the safe side I still put forward my test as a *necessary*
condition only, not a sufficient one, for the "thoroughly synthetic"
status of an axiom for a mathematical theory. It does not stand alone,
however; there is more to come.

Now let us consider the sort of example Sam pointed out. I'll begin
with a trivial case. Suppose we have "nice" axioms C and C->D (so
nice, in fact, that C and D are atomic---it's a rather dull theory).
Sam says we should take some logical truth T (I am not using Sam's
notation here) and doctor the axioms so that they become (T&C) and
(T&C)->(T&D) respectively.

Now the first of these doctored axioms, (T&C), is already ruled out by
the requirement that one not be able to prove a logical truth by means
of a proof with only eliminations on branches below the assumption
occurrence(s) of the axiom. So the doctoring could only turn the
original axioms into

	C, (T&C)->(T&D)

Now consider the following deduction in normal form:

	__
	\/				(triangle=proof of logical truth)
	 T  C
	______
	  T&C      (T&C)->(T&D)
	 _______________________ ->Elim
		 T&D
	         ___ &Elim
		  T

Note that on the branch below the assumption occurrence of
(T&C)->(T&D) there are only eliminations. So now we have ruled out the
doctored implication as well, by the same test.  It does not matter,
either, that we used the other axiom C as an assumption in the minor
proof for the ->Elim; all that matters is that on the branch headed by
the (sole assumption occurrence of the) axiom we are trying to
disqualify, there are only eliminations.

Consider next the minitheory with axioms DvC, D->E, C->F (D, C, E, F
atomic) . Sam's doctoring would yield (T&D)v(T&C), (T&D)->(T&E),
(T&C)->(T&F). The first of these doctored axioms features in the
following normal deduction of the conclusion T:

		_____(1)	______(1)
		T&D		T&C
		____ &Elim	____ &Elim
(T&D)v(T&C)      T               T
____________________________________(1) vElim
	         T

So the doctored axiom (T&D)v(T&C) is ruled out by the test concerning
eliminations on branches. (Remember that in a natural deduction a
branch is defined in such a way that there are branches running from
the major premiss for vElim through the case assumptions of its case
proofs.) 

What about a Sam-style doctoring of an axiom of negated form? Consider
the doctored form ~(T&A). This features as an assumption for the
following normal deduction of the 'synthetic' result ~A:
	__
	\/     __(1)	
	 T     A
	 _______
	   T&A     ~(T&A)
	   ______________
	        #
	       ____(1)
 		~A

This motivates a new test: a set of axioms is no good if, for the
proof of a synthetic (=logically falsifiable) consequence from it, one
needs to have a proof of a logical truth (*as* a logical truth) as a
subproof.

Dually, we should also rule out any set of axioms if, for the proof of
a synthetic consequence from it, one needs to have a reductio subproof
with a single premiss (establishing that sole premise as a logical
falsehood).

The idea we are getting at here is that no 'purely logical' results
should ever be needed as we try to infer synthetic results from
synthetic axioms. This is also a condition on the very results
themselves that we seek to establish; for obviously if P is a genuinely
synthetic theorem of the mathematical theory and T an arbitrary
logical truth, then (T&P) will also count as a synthetic result of the
theory. However, it is intuitively reasonable to ignore the logically
true conjunct and focus only on P as genuinely expressing synthetic
theoretical content. (That's what a mathematician would do, surely?)

To summarize:

In order to theorize synthetically within any branch of mathematics,
one should use only such axiom sets A and seek to prove as theorems
only such results P as meet the following (individually necessary, but
perhaps not jointly sufficient!) conditions:

1. A is independent in the usual sense; i.e. no member P of A follows
logically from A\{P}.

2. There is no natural deduction D in normal form from a non-empty subset
of A with any of the following features:

(a) D contains as a subproof a proof all of whose assumptions have
been discharged;

(b) D contains as a subproof a reductio of a single sentence;

(c) D has a logical truth as its conclusion, and at least one axiom
from A has only eliminations below all its undischarged assumption
occurrences in D (on all branches running though them)

3. There is no natural deduction in normal form from a non-empty set
of the axioms plus a logical falsehood, whose conclusion is absurdity
and in which at least axiom has only eliminations below all its
undischarged assumption occurrences (on all branches running through
them).

I realize now that Sam or Torkel might well show that the conjunction
of these conditions is both too demanding and not demanding enough;
but I feel it worth pushing this line before drawing the pessimistic
conclusion that the intuitions involved are just too vague, misguided
or incoherent to be turned into a decent technical criterion.

Can any mathematician on the list tell me, for example, whether they
have ever had to establish a self-contained logical truth (or refute a
self-contained logical falsehood) in its own right by means of a
subproof of a larger proof of a genuinely synthetic theorem within a
nicely axiomatized theory?

Neil Tennant