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.
>Formalisation of mathematics
>is certainly a major issue; modularity, and preferences for different
>formalisations and theories are others. Yes, we could all go off tomorrow
>and use/build systems which have hardwired support for our own preferences.
>This is the `Tower of Babel' approach, and is what we're trying to escape
>from, rather than what we seek.
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?