The isomorphism inference rule

Question

Suppose we are writing very detailed proofs, absolutely without any gaps (for example, for checking proofs by computer).

In such formal proofs every step (even a trivial one) must be justified.

For example, when we have proved that A = B and A is a prime number, we can infer that B is also a prime number.

We can justify this step by Leibniz Law (which may be represented by an axiom of Predicate Calculus with Equality).

When a group A is isomorphic to a group B and the group A is simple, then we can infer that the group B is also simple.

We can say , that "the isomorphism inference rule" was used in that case.

To justify such inferences, Bourbaki developed a general theory of isomorphism (see their book "Theory of Sets").

Because the Bourbaki theory is rather complicated, my questions are:

1) Are there other approaches for justification of "the isomorphism inference rule"?

2) Or maybe there are more simple expositions of Bourbaki approach?

Answer 1

Well, if you prove a predicate P respects any equivalence relation R, you can then use a similar inference from one member of an equivalence class to another. So you can deduce P(y) from P(x) under those circumstances from x R y. Now are you objecting to the complexity of the isomorphism concept (R), or the fact that certain concepts P are in some a priori way known to depend only on the isomorphism class? I suspect the latter. Bourbaki likes "transport of structure" as a concept; I suppose the point may be that "structure" in this sense is by no means confined to first-order logic.

Answer 2

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 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.

Answer 3

Dealing with this question is one of the goals behind Voevodsky's equivalence axiom for type theory.

In ordinary Martin-Löf dependent type theory, an equality A=B is represented by a term in an identity type, $p:Id_T(A,B)$ where T is the type of A and B. The term p is regarded as a "proof" that A=B, under the "propositions as types" paradigm. The fact that any property of A then transfers to a property of B is implemented by the elimination rule for identity types. For example, if P(X) is the property "X is prime" and we have a proof of P(A), i.e. a term $q:P(A)$ (under propositions-as-types), then from p and q we can construct a new term $J(q;A,B,p): P(B)$ which "proves" that B is also prime. This is the type-theoretic incarnation of "Leibniz' law," but since it applies to terms of arbitrary types (not just proofs of propositions) it is more powerful.

The equivalence axiom says, roughly, that If A and B are types and $Type$ is a type-theoretic universe containing them, then terms of the identity type $Id_{Type}(A,B)$ are the same as isomorphisms between A and B. In particular, this means that given an isomorphism between A and B, we can apply the equivalence axiom to obtain a term $p:Id_{Type}(A,B)$, and then use the elimination rule for identity types, as above, to show that any property of A is also possessed by B.

The equivalence axiom greatly restricts the class of models of type theory. Notably it excludes all "extensional" approaches which model types by sets and identity types by equality. Models of the equivalence axiom tend to be categorial or homotopical, in which the models of types are higher categories or homotopy types containing internal structure with which to record isomorphisms. The ur-example models types by homotopy-types, a.k.a. ∞-groupoids, and the universe $Type$ by the ∞-groupoid of all small ∞-groupoids.

Answer 4

This approach is related to my other answer, but simpler.

Note that if we define groups and so on in terms of classical membership-based set theory, then it is not true that all properties transfer along isomorphisms. For instance, the property "the identity element of this group is the empty set" is not preserved under passage to an isomorphic group. So if we want an "isomorphism inference rule," we need to somehow restrict the allowable statements. A very natural way to do this is by using a category-theoretic foundation of mathematics. If we write the axioms of a category in dependent type theory in a way which excludes the notion of "equality between objects" (which reflects how we usually reason about objects of a category anyway), then any fact about objects or morphisms in a category which can be expressed in this language will automatically be invariant under isomorphisms of objects, and under equivalences of categories. This was first shown by Peter Freyd in the paper "Properties invariant within equivalence types of categories" and by Georges Blanc in the paper "Équivalence naturelle et formules logiques en théorie des catégories," and more recently it has been explored in much more depth and generality by Michael Makkai in the theory of FOLDS.

Answer 5

There is more than one kind of isomorphism, because isomorphism preserves structure, and there is more than one kind of structure.

• Set isomorphisms preserve cardinality.
• Group isomorphisms preserve the way the group may be generated.

and so on. They are meant to show that two instances are merely 're-presentations' of a common structure. An 'isomorphism inference rule' would simply be the observation that any property P which is phrased directly in terms of the properties preserved by isomorphisms, will also be preserved by isomorphisms.

Whether an integer number is prime does not depend on whether it is expressed in decimal or binary, but on e.g. the Peano Axioms used to define the integers and the particular integer in question; whether a group is simple does not depend on anything but the group axioms and the way in which the group is generated. If you prove isomorphisms of the two instances, the preservation of properties defined in terms of those structures follow ipso facto.

Leibnitz's law is the same principle as this, except applied to an equivalence relation which preserves "all" structures. (Leibnitz's law is tantamount to the declaration that such an equivalence relation exists.)

Answer 6

I don't see why a special rule should be introduced to make inferences about properties preserved by isomorphisms: if a property P is preserved by isomorphisms then it should hopefully be possible to prove this preservation using only the axioms and the standard logic inference rules.

Answer 7

The "isomorphism inference rule" can be understood in terms of the concept of elementary equivalence in model theory: http://en.wikipedia.org/wiki/Elementary_equivalence

The wikipedia article above discusses elementary equivalence for first order logic, but it may be generalised to higher order logic. Given a language $\mathcal{L}$ with semantics $\models$, two structures $\mathbb{M}$ and $\mathbb{N}$ are elementarily equivalent whenever for all $\phi \in \mathcal{L}$, $\mathbb{M} \models \phi$ holds if and only if $\mathbb{N} \models \phi$.

One can prove for first-order, second-order and higher order logic the following theorem:

if two structures are isomorphic, then they are elementarily equivalent

The proof almost always employs structural induction on the composition of formulae, making use of the fact that the semantics for various logics are usually defined compositionally using recursion. The converse of the above statement is not true in general.

Here is how we can apply the concept of elementary equivalence to the example provided. We can express in second order logic a formula $\phi$ such that $\mathbb{M} \models \phi$ if and only if $\mathbb{M}$ is a simple group. We then know that if $\mathbb{M} \cong \mathbb{N}$, then $\mathbb{M} \models \phi$ if and only if $\mathbb{N} \models \phi$. This means that if $\mathbb{M}$ and $\mathbb{N}$ are isomorphic, $\mathbb{M}$ is a simple group if and only if $\mathbb{N}$ is a simple group.

TL;DR: The "isomorphism inference rule" can be understood model theoretically in terms of elementary equivalence, and is a consequence of the compositionality of semantics.