On Mar 4, 2010, at 9:05 AM, Gary Berg-Cross wrote:
Ali,
Thank you for the information about and pointers to CALORE. I found them to be a clarifying and progressive contribution to the discussion as a "growing platform (a repository) in which they may be inputted and relations between them explored, identified and formalized." I look forward to updates on progress. The SOCoP group, which I am part of, would be particularly interested in the Geometry ontology.
I also greatly appreciated your exposition on Conservative or Nonconservative extensions of axioms:
From a formal perspective, there are two possible ways of extending axioms, Conservative or Nonconservative. ...
In plain English, a conservative extension means that you are introducing new terms which you didn't have in your vocabulary before and specifically you need these new terms to prove new things based on your axioms.....
In comparison, a non-conservative extension does change the meaning of your primitives.
It's a nice clean distinction that provides useful guidance and helps the discussion on improved ontological models.
To say that an extension T' of a theory T is conservative is to say only that you can't prove anything new about the original primitives in the language of the original theory. Typically, however, the axioms for a set of primitives do not axiomatize those primitives independently. Rather, many axioms lay out the logical connections between primitives. So if you have a theory T with some set of primitives and you introduce a new primitive and axiomatize its connections to your original primitives by means of a conservative extension T' of T, you will likely be able to prove all sorts of new things in T' about your original primitives concerning their connections to the new primitive. All that conservativeness guarantees is that you won't be able to prove anything about the old primitives alone in T' that you couldn't already prove in T.
To illustrate, the basic axioms for zero '0' and successor 's' are:
1. 0≠sx (0 is not the successor of any number.)
2. sx=sy -> x=y (No two distinct numbers have the same successor.)
3. [A(0) & (x)(A(x) -> A(sx))] -> (x)A(x) (Mathematical induction.)
Call this theory T. If we now add the new function symbol '+' to our language and add the axioms
4. x+0=0
5. x+sy=s(x+y)
we have the theory known as Presburger Arithmetic; call it T'. T' is a conservative extension of T; you can't prove anything in T' about zero and the successor function alone that you couldn't already prove in T. But T' does enable us to prove new things about zero and successor that we didn't know before concerning their connections to the addition relation (propositions 4 and 5 themselves, for example).
So the issue here seems to me to boil down to a quibble about what constitutes a change in meaning. Let P be a primitive in a theory T and suppose T' is an extension of T.
Proposal 1: P's meaning changes from T to T' if and only if there are theorems of T' involving P (and, to avoid triviality, requiring at least one nonlogical axiom of T') that are not theorems of T. (As noted, this will typically be the case regardless of whether or not T' is a conservative extension of T.)
Proposal 2: P's meaning changes from T to T' if and only if there are theorems of T' involving P in the language of T that are not theorems of T (and, hence, only if T' is a nonconservative extension of T).
Of these, it seems to me that Proposal 1 is the one that is closest to our intuitive notion of a change in meaning. Even if T' is a conservative extension of T, if you can prove new, nontrivial things about a primitive then you know more about it; its meaning has been refined and extended by relating it to the meanings of new primitives.
But Proposal 2 does not seem entirely unreasonable to me either.
Chris Menzel