> What about an a-theoretic vocabulary? From algebra and arithmetic
> a logical theory is just a set of elements (formulae) and a collection
> of operators on the elements.
and
> My question is whether we need to "formalize" in the sense of logicians
> at all. To make the discussion a little more concrete, suppose that
> we were to extend Mathematica with a collection of deductive systems
> and proof checking operators. You wish to work within pure FO Peano
> arithmetic, I want to restrict myself to Yessenin-Volpin's realm
> (assuming I could understand it at all) and an engineer wants to
> prove theorems about some differential equations and doesn't care
> how its done. It should be possible to load the appropriate libraries
> and use deductive operators and syntax checkers for each of these
> three choices. Is there a reason why there should be a formal meta-theory
> behaind each of these systems? Is there an advantage if we require
> that all three types of systems be translatable into some ur-logic?
I agree that a naive user should be able to get on with deductive
reasoning in a particular theory, without being aware of any metatheory.
Explicit use of metatheory is important for power users (e.g. appreciating
whether results available in another theory or logic could be applied,
and then prescribing how) and for system implementors (for whom it is
a large part of their conceptual framework).
The three users you mention are almost certainly not interested
in exchanging the results of their labours, so that the other two can
reuse them. I believe exchange and reuse are major goals of QED however.
If we all agreed on one object theory - and stuck to it forever - then we
could have exchange and reuse without explicit metatheory. Even then,
explicit metatheory could improve the quality of the common object theory,
e.g. by providing a way of specifying and justifying derived rules of
inference so as to increase the productivity of proof-checking; but that's
another story.
John