Re: SUO: Re: The lattice of theories
Bill,
The partial ordering is defined by ordinary implication:
Theory T1 with axiomatization A1 is a generalization
of theory T2 with axiomatization A2 iff the conjunction
of all axioms in A2 implies the conjunction of all axioms
in A1.
Since we are dealing with first-order theories, implication
is equivalent to entailment, and implication is something
that is more easily computable than entailment.
Chris Menzel noted that if you consider the complete set
of all propositions in a theory (i.e., the deductive closure
of the axioms), then the partial ordering defined by implication
is equivalent to the partial ordering defined by subset:
T1 with axiomatization A1 is a generalization of
T2 with axiomatization A2 iff T1 is a subset of T2.
However, since all of the theories are infinite (even the smallest
one contains all tautologies), we can only store and reason about
the axioms. Therefore, implication is the only operator we can
usefully use for comparing theories in practice.
John