MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

3 Improved grammar

First of all, I suspect that whenever a formal system has such an "isomorphism inference rule," all proofs using that rule can be converted to proofs not using it. (I don't know the details of Bourbaki's set theory, though.)

So what could an "isomorphism rule" look like? First of all, you need a metamathematical characterization of what constitutes an "isomorphism" between arbitrary "structures." I guess category theory can answer this question, but only if you encode your specific class of structures as a category. So that does not really define isomorphism on a metamathematical level. (Unless, apparently, one works within fully categorial foundations: http://cs.nyu.edu/pipermail/fom/2003-July/007064.html)

However, there is indeed a comparatively simple way to characterize isomorphisms. This is actually part of a formal system I have developed for a proof assistant, but you can apply the same principle in naive set theory if you don't mind a little vagueness. (Don't try to apply it to first-order axiomatic set theory, though.)

There is one rule of this system that matters here: Roughly speaking, for given x and S, you may not ask whether x is a member of S unless x was introduced as a member of some superset of S. The introduction of a variable as a member of a given set is considered primitive, so the rule is purely syntactical. An example:

We want to say: "Let S be the intersection of the set of primes with the set of even integers, and n be a member of S. Then n is in N." Surely, the set of primes is defined as some subset of N, which in turn is a subset of Z, and the set of even integers is also defined as a subset of Z. So n is syntactically known to be a member of Z, and we can ask whether it is also in N. However, we cannot ask whether it is e.g. in the set of finite graphs. Or whatever else. Formally, this amounts to a type system.

Another aspect of the formal system is that when you want to define what a "group" is, you need to specify when two "groups" are considered equal. So suppose you are given two sets S and T, as well as group operations on each. There is no syntactically "known" superset, so you cannot ask whether S=T because that would involve taking an element of S and asking whether it is in T. Now convince yourself that the most you can do is ask whether the two groups are isomorphic. That is, no other formula you can come up with will ever distinguish two groups that are isomorphic groups. (It is required to be reflexive, symmetrical, and transitive, of course.)

To conclude, it is possible to construct a system in which you cannot even talk about structures except up to isomorphism, for arbitrary structures. (That does not mean you cannot take their concrete sets into account in special cases. For example, if you have a group with two isomorphic subgroups, these will be considered equal as groups, but the sets can be different. Note how it makes sense to ask whether they are equal or different because we know a common superset.)

Now here is my equivalent of your "isomorphism inference rule": Since two isomorphic groups are in fact equal in this system, any property you can specify about one of them will be considered true of the other.

2 removed a "not" I had inserted mistakenly

First of all, I suspect that whenever a formal system has such an "isomorphism inference rule," all proofs using that rule can be converted to proofs not using it. (I don't know the details of Bourbaki's set theory, though.)

So what could an "isomorphism rule" look like? First of all, you need a metamathematical characterization of what constitutes an "isomorphism" between arbitrary "structures." I guess category theory can answer this question, but only if you encode your specific class of structures as a category. So that does not really define isomorphism on a metamathematical level. (Unless, apparently, one works within fully categorial foundations: http://cs.nyu.edu/pipermail/fom/2003-July/007064.html)

However, there is indeed a comparatively simple way to characterize isomorphisms. This is actually part of a formal system I have developed for a proof assistant, but you can apply the same principle in naive set theory if you don't mind a little vagueness. (Don't try to apply it to first-order axiomatic set theory, though.)

There is one rule of this system that matters here: Roughly speaking, for given x and S, you may not ask whether x is a member of S unless x was introduced as a member of some superset of S. The introduction of a variable as a member of a given set is considered primitive, so the rule is purely syntactical. An example:

We want to say: "Let S be the intersection of the set of primes with the set of even integers, and n be a member of S. Then n is in N." Surely, the set of primes is defined as some subset of N, which in turn is a subset of Z, and the set of even integers is also defined as a subset of Z. So n is syntactically known to be a member of Z, and we can ask whether it is also in N. However, we cannot ask whether it is e.g. in the set of finite graphs. Or whatever else. Formally, this amounts to a type system.

Another aspect of the formal system is that when you want to define what a "group" is, you need to specify when two "groups" are considered equal. So suppose you are given two sets S and T, as well as group operations on each. There is no syntactically "known" superset, so you cannot ask whether S=T because that would involve taking an element of S and asking whether it is in T. Now convince yourself that the most you can do is ask whether the two groups are isomorphic. That is, no other formula you can come up with will ever distinguish two groups that are not isomorphic. (It is required to be reflexive, symmetrical, and transitive, of course.)

To conclude, it is possible to construct a system in which you cannot even talk about structures except up to isomorphism, for arbitrary structures. (That does not mean you cannot take their concrete sets into account in special cases. For example, if you have a group with two isomorphic subgroups, these will be considered equal as groups, but the sets can be different. Note how it makes sense to ask whether they are equal or different because we know a common superset.)

Now here is my equivalent of your "isomorphism inference rule": Since two isomorphic groups are in fact equal in this system, any property you can specify about one of them will be considered true of the other.

1

First of all, I suspect that whenever a formal system has such an "isomorphism inference rule," all proofs using that rule can be converted to proofs not using it. (I don't know the details of Bourbaki's set theory, though.)

So what could an "isomorphism rule" look like? First of all, you need a metamathematical characterization of what constitutes an "isomorphism" between arbitrary "structures." I guess category theory can answer this question, but only if you encode your specific class of structures as a category. So that does not really define isomorphism on a metamathematical level. (Unless, apparently, one works within fully categorial foundations: http://cs.nyu.edu/pipermail/fom/2003-July/007064.html)

However, there is indeed a comparatively simple way to characterize isomorphisms. This is actually part of a formal system I have developed for a proof assistant, but you can apply the same principle in naive set theory if you don't mind a little vagueness. (Don't try to apply it to first-order axiomatic set theory, though.)

There is one rule of this system that matters here: Roughly speaking, for given x and S, you may not ask whether x is a member of S unless x was introduced as a member of some superset of S. The introduction of a variable as a member of a given set is considered primitive, so the rule is purely syntactical. An example:

We want to say: "Let S be the intersection of the set of primes with the set of even integers, and n be a member of S. Then n is in N." Surely, the set of primes is defined as some subset of N, which in turn is a subset of Z, and the set of even integers is also defined as a subset of Z. So n is syntactically known to be a member of Z, and we can ask whether it is also in N. However, we cannot ask whether it is e.g. in the set of finite graphs. Or whatever else. Formally, this amounts to a type system.

Another aspect of the formal system is that when you want to define what a "group" is, you need to specify when two "groups" are considered equal. So suppose you are given two sets S and T, as well as group operations on each. There is no syntactically "known" superset, so you cannot ask whether S=T because that would involve taking an element of S and asking whether it is in T. Now convince yourself that the most you can do is ask whether the two groups are isomorphic. That is, no other formula you can come up with will ever distinguish two groups that are not isomorphic. (It is required to be reflexive, symmetrical, and transitive, of course.)

To conclude, it is possible to construct a system in which you cannot even talk about structures except up to isomorphism, for arbitrary structures. (That does not mean you cannot take their concrete sets into account in special cases. For example, if you have a group with two isomorphic subgroups, these will be considered equal as groups, but the sets can be different. Note how it makes sense to ask whether they are equal or different because we know a common superset.)

Now here is my equivalent of your "isomorphism inference rule": Since two isomorphic groups are in fact equal in this system, any property you can specify about one of them will be considered true of the other.