FOM: Recursive and independent axiomatizations

[Torkel Franzen]

  Neil says:

  >(1) The 'thin', classical notion of recursiveness, entailed by the
  >mere fact of finitude of the set in question, is not rich enough.

  I agree and in fact would go further, as stated in my original
comments:

     When we actually want to consider stronger conditions on axioms
     than recursive enumerability, recursiveness is too weak, and
     the concept of schemata or some suitable generalization is much the better
     notion.

   >If we *combine* the decidable-membership condition with the communal
   >self-certification condition then (I think) we have something
   >reasonable.

  "Communal self-certification", however, is not a mathematically definable
concept, such as we use in logical reasoning about general theories. In
such a context my suggestion remains that requiring axiom sets to be
recursively enumerable is preferable to requiring them to be recursive.

  About independent axiomatizations:

   >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.

   T&A is equivalent to -(T->-A), from which T is not derivable using
only eliminations.