Re: SUO: a silly question about the new modular architecture
Adam,
Theory compilation is trivial. The tools to do it come for free
with every Unix system. (And there are Unix-like tool packages
that can also be run on legacy systems, such as Windows.)
> I don't believe that there are any existing tools that would perform
> this sort of theory compilation nor has anyone volunteered to build them
> but that's another story.
Given the axioms for theory A and the axioms for theory B,
you can create the axioms for the combined theory C
by using the cat (concatenate) command in Unix:
cat A B > C
This creates a new file C, which contains all the axioms for
both A and B.
There are now two more questions one would like to ask:
1. Is the new theory consistent?
2. Are any of the axioms redundant?
Both questions can be answered by running your favorite theorem
prover. To answer #1, try to derive a contradiction (i.e., the
empty clause in resolution theorem provers). That is a test that
should be performed on any theory, especially if it was produced
by hand coding.
To answer #2, use the theorem prover to check whether all the
axioms in C are independent; i.e., none of them can be proved from
the remaining ones. If not, delete the redundant ones, but do so
one at a time to make sure that the deductive closure of the
remaining axioms is still equivalent to the original C.
Now, it is possible that the theory is undecidable. But as I have
said before, that is also true of any theory constructed by hand.
But even at that level, it is easier to prove consistency (if it is
indeed provable) for multiple smaller theories than for one big theory.
John Sowa