[FOM] Question on axiomatizations

[Michael Sheard]

I have been working on a problem in which I can describe a particular 
theory in first-order logic abstractly, as a computably enumerable set 
of formulas, but it is not obvious if there is a natural 
axiomatization.  This situation raises two general questions:

1)  Typically a theory in f.o.l. is described by presenting a decidable 
set of axioms, but an alternative approach is to supplement the axioms 
with one or more extra rules of inference:  if A_n is a theorem, then so 
is B_n, for some decidable set of pairs (A_n, B_n).  A theory described 
in this way does have a decidable axiomatization by Craig's trick, but 
the resulting axiomatization is far from natural, even if the rule of 
inference itself is very simple.  Does anyone know if any work has been 
done comparing these two approaches on any measure of "naturalness", 
complexity, etc.?

2) From a philosophical standpoint, it could be argued that the standard 
requirement that an axiomatization be decidable (or even primitive 
recursive) is too general, because it leaves undecidable questions about 
the axioms which in practice are easy to answer for any actual theory in 
common use in mathematics: for example, given formula A, is there a 
formula B such that "if A then B" is an axiom?  Has anyone argued for a 
more restrictive definition for what should count as an acceptable set 
of axioms for a theory?

With thanks,
Mike Sheard

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/fom/attachments/20071105/938e8942/attachment.html