# Theorems and isomorphisms

1. Sep 11, 2010

### Fredrik

Staff Emeritus
If G and H are groups, and f:G→H is a group isomorphism, then every theorem that holds for G can be translated to a theorem that holds for H, by changing the domain of discourse for the logical quantifiers $\forall$ and $\exists$ from G to H (or simply changing G to H, if the domain of discourse is taken to be the class of all sets) and replacing each free variable x in the theorem with f(x) (and each constant y with f(y)).

Is the statement above accurate? Would it also be accurate to say that it can't be proved as a theorem in ZFC or even in mathematics, since theorems aren't sets (or categories, or whatever we choose to think of as the foundation of mathematics)? They are strings of text in the formal language of mathematics, so any "theorem" about them would be metamathematics, not mathematics.

Last edited: Sep 11, 2010
2. Sep 11, 2010

### Newtime

Why can't we simply avoid this question by noting that any theorem which applies to $$G$$ applies to $$H$$ without any need for "translation," but just by applying the isomorphism to any element in question since $$G \backsimeq H$$. I know this is in effect what you've said, but why isn't it trivially correct?

Note: it is clear from this post and others you've far more knowledge and experience in the subject than I do, so I realize my post may come across as silly, but since my level of knowledge is where it is, this is how I interpret your question.

3. Sep 11, 2010

### Fredrik

Staff Emeritus
I agree that the claim is "obviously true", but to know that it can be proved and to actually prove it are two different things. Consider e.g. the claim that since addition of real numbers is associative, you can drop all parentheses from all sums without introducing any ambiguities. This is also "obvious", but to really prove it you would have to write down a recursive definition of "sum" and prove the claim by induction. Similarly, a proof of the claim I'm talking about would have to use a formal definition of "theorem". Actually, we need such a definition just to state the claim in a way that makes it meaningful to ask if it can be proved.

Last edited: Sep 11, 2010
4. Sep 11, 2010

### farleyknight

I do not have a lot of experience with the subject you are describing, but from what little I do know: Some areas of proof theory and meta-mathematics take proofs as functions, where the domain, say A, is of the type specified by the hypothesis and the range, say B, is the type specified by the conclusion.

In this way, we may be able to describe a proof that is general enough for your G where the "proof function" acts polymorphically on both G and H. So you may not have to translate anything at all.

I'm actually curious: What is the motivation behind your question?

5. Sep 11, 2010

### Fredrik

Staff Emeritus
I want to be able to explain why "isomorphism" is such a useful concept. Isomorphic structures are supposed to be interchangable for all all practical purposes, but without a (meta)theorem like this, I don't think we have really justified that. I also think it's fascinating that this very important result isn't even "mathematics".

6. Sep 11, 2010

### Hurkyl

Staff Emeritus
A string of text in a formal language is a finite sequence of elements in a set (the alphabet). Metamathematics is, roughly speaking, the hypothesis that formal logic adequately describes "real world" mathematics.

7. Sep 11, 2010

### farleyknight

Yeah, I think polymorphism is probably what you're looking for. At least it seems that way to me. If two objects are isomorphic on some set of properties, then we can define a new type T based on that set of properties. I think model theory calls this a structure.

Anyways, once you have the type T, you can begin considering the class of all objects that fit T as a new kind of object. And often times, since you had to do the work to show these objects are isomorphic, you're probably a little familiar with them both. And a fair amount of methods or formulas or what-not will fit both "naturally".

So, in a sense, isomorphism can give you a lot of "new" results for "free".

You mention categories briefly in your OP. A lot of this kind of stuff can be found in the Category Theory literature, although they assume a fair amount of prior knowledge (at least graduate level mathematics). But some of it is suitable for undergrads.

8. Sep 11, 2010

### yossell

I think so - I'm a little hesitant because you've not specified the languages. I presume the language in question contains only predicates for the group operations plus identity? Translation I normally understand as a mapping from sentences to sentences. But your talk of change of domain of discourse' suggests you have a reinterpretation rather than a translation in mind?

Provided you allow the set-theorist his usual trick of coding mathematical objects in terms of sets, I can't see why the set-theorist can't do this. Symbols are identified or modelled by certain sets; concatenation of symbols is modelled by a set-theoretic construction on these other sets; well-formed-formulas are then defined as certain sets along familiar lines. In effect, this is even doable in number theory via a Godel numbering. Then various semantic notions of satisfaction and the like are similarly coded up in set-theory. There are limitations due to the need to avoid paradoxes when you try to do anything too ambitious - such as coding up the semantics of set-theory itself - but group theory should be easy enough.

9. Sep 11, 2010

### Fredrik

Staff Emeritus
I'm not sure how to avoid circularity here. "Finite" means "has n members, for some natural number n", but natural numbers are defined using sets, and set theory itself is expressed in a formal language. Hm, I suppose we can use the set-theoretic definitions of such terms when we're talking about other languages than the language of set theory. And we can also identify the symbols of the alphabet with the members of a finite set...if we're not talking about the language of set theory. This is OK I guess*. In that case, the theorem I'm concerned about is a theorem in ZFC, and not a metamathematical theorem. Is that what you had in mind?

*) It seems to imply that when we're dealing with the formal language of set theory, we have to appeal to intuition. The specification of the formal language of set theory only works because we already have an intuitive understanding of natural numbers. This would also mean that "natural number" is a more fundamental concept than "set", even though it's often claimed that natural numbers are defined in ZFC.

10. Sep 11, 2010

### Fredrik

Staff Emeritus
That's what I had in mind.

Consider the groups G={0,1} with addition modulo 2 and H={-1,1} with multiplication. I was thinking that if I specify that the domain of discourse is G, $\forall x\ x+x=0$ is a theorem, but if I don't, I would have to write it as $\forall x\ (x\in G\rightarrow x+x=0)$. But that was probably the wrong way to think. If I say that G satisfies the first sentence, I always mean that the domain of discourse is G, so there's no need to specify it explicitly.

The corresponding theorem for H would of course be $\forall x\ x\cdot x=1$, so what I meant by a "translation" here is simply what you get by the substitutions $+\rightarrow\cdot$, $0\rightarrow 1$, $1\rightarrow -1$. (No need for $x\rightarrow f(x)$ here, since there are no free variables).

I think I was a bit confused by the fact that this doesn't make sense for the formal language of set theory. See my reply to Hurkyl above.

11. Sep 11, 2010

### yossell

Hi Fredrik,

it probably makes no serious mathematical difference, it's probably a matter of terminology (and I don't mean this negatively at all), but from my point of view, your way of describing things mixes up model theoretic notions and linguistic notions. You present two groups {0 1} and {-1 1}. But it also seems you're considering a language L that contains symbols 0', 1', -1' for all these objects, and which also has predicates for different operations + and . Is this right? I guess that these terms and predicates are all definable in set theory - from this point of view, your question becomes a question about whether certain equivalences are provable in set-theory. But this is a different perspective from one which involves coding up a first order language of group theory in set-theory, and then coding up a certain amount of model theory.

I'm not sure what's worrying you in your response to Hurkyl. In set-theory, and without appealing to semantic or linguistic notions or appealing to numbers, one defines the special set omega. In terms of this set, and without appealing to semantic or linguistic notions or appealing to numbers, one defines finite sequences. One defines one's alphabet as certain sets. Then, one can define finite sequences of letters to form strings of symbols. I don't see a circularity here.

The one worry with all this, perhaps it's the one you had in mind, is the trouble that the first order theorist has with non-standard models - there are those who think the existence of such models means he cannot, as he had hoped, properly define a finite sequence. But I don't see this as a circularity worry.

12. Sep 11, 2010

### JSuarez

My apologies if someone already said it (I couldn't find it), but the isomorphism statement is a basic result in classical model theory: if you have two isomorphic structures, then any first-order formula (that is closed, or with free variables replaced by parameters) is true (or false) in both. The only inacuraccy is in saying that open expressions (the ones with free variables) have a truth-value; they don't until you replace those variables with concrete objects from the structure's domain.

The proof of this statement is simple: just apply induction on the complexity of the expressions.

In fact, you don't need isomorphism for two distinct structures to satisfy the same class of first-order expressions: there are non-isomorphic strucutures that have this property; they are called, in Model Theory, elementarily equivalent structures.

Last edited: Sep 12, 2010
13. Sep 11, 2010

### Fredrik

Staff Emeritus
Hm, you have a point there. The language should consist of the symbols that all first-order languages have in common, and in addition to that, a binary operation symbol, a unary operation symbol and a constant symbol. Let's choose those to be $\{\star,i,e\}$. Now each structure with signature $\{\star,i,e\}$ associates a binary operation with $\star$, a unary operation with i, and a member of the underlying set with e. What I should have said is that the complete definition of the first group I specified (incompletely), associates + with $\star$, $x\mapsto x$ with i and 0 with e. The second group associates · with $\star$, $x\mapsto x$ with i and 1 with e.

Edit: Another thing became clear to me when I wrote this sentence in the reply to JSuarez below: "if X and Y are isomorphic, any theorem that is satisfied by X is satisfied by Y too." When I gave an example of a theorem about a group G that corresponds to a theorem about another group H, I shouldn't have written $\forall x\ x+x=0$ and $\forall x\ x\cdot x=1$. The theorem is one sentence that's satisfied by both structures, and it's neither of the two above, it's $\forall x\ x\star x=e$. This discussion is clearly good for me, since I'm making exactly the sort of mistakes you'd expect from someone who has read a third of the book and not done any exercises.

Mainly the problem of how to define "finite" before "natural number". It seems like we even have to have an intuitive understanding of sets before we define the formal language of set theory, because a specification of a language involves a specification of an alphabet, which is a set of symbols.

Can you tell me how?

Yes, I remember seeing a theorem that appeared to be saying something very similar in a book a few months ago. I haven't studied the proof yet, but I will. My concern here isn't so much "does such a theorem exist?". It's more like "is it a theorem in mathematics or metamathematics?". I was thinking that since it's a theorem about theorems, rather than a theorem about sets, maybe it's not a theorem in ZFC or any other set theory. But it seems that I should be thinking about variables, logical symbols, sentences etc, as sets. I can see how that makes sense for any first-order language, except the language of set theory.

This is interesting, and from my point of view, also a bit disturbing. As I said in one of my posts above, I'm looking for a nice way to explain the point of isomorphisms. Why do we define them at all, and in what sense are isomorphic structures equivalent? This concept of "elementarily equivalent structures" seems to ruin my idea that this theorem is what tells us exactly in what sense isomorphic structures are "equivalent".

Last edited: Sep 11, 2010
14. Sep 11, 2010

### JSuarez

I don't think this is a really good question, because the distinction is rather arbitrary. Metamathematics is just the mathematical study of formal (axiomatic or not) systems which, in turn, may be used to study certain mathematical objects and questions (like Set Theory, Algebra, etc.). A mathematician studying the Model Theory of, say, Groups or Fields, would say that this is a mathematical result, while a logician working in pure Model Theory would say metamathematical.

As far as being a formally provable in ZFC, the answer is yes: the proof needs only first-order classical logic, sets and accepted forms of inference, like induction. Furthermore, this is not a theorem about theorems; is a theorem about structures, which are the objects of study of Model Theory.

I'm afraid that I'm missing your question: the languages of almost any formal Set Theories are first-order languages.

Not at all. These notions of logical equivalence started with Alfred Tarski, who had hopes that they would be as strong as the algebraic notions of isomorphism; if that were the case, then you would have a set of alternative classificarion tools besides the algebraic ones.

No, no: it's the other way around. Isomorphism is the strongest equivalence notion that we have; Tarski's program was soon to be proved much more weaker than he hoped; first-order logic simply doesn't have the expressive power to be a powerful classification tool (except in finite model theory, but that's another story). If you can, see Wilfred Hodges's book "A shorter model theory" for a much more complete and clear exposition.

You may also think about isomorphic structures in a "physical" way: just as there isn't any experiment that can distinguish equivalent reference frames, there isn't a mathematical property that can distinguish isomorphic structures. This is an imprecise statement, but I think it conveys the general idea (in another sense, it can also be seen as a "categorification" of identity, but I'll leave this one for Hurkyl to pick apart).

Last edited: Sep 12, 2010
15. Sep 11, 2010

### Fredrik

Staff Emeritus
Yes, it's a about structures, but it certainly appears to be about theorems too. It specifically claims that if X and Y are isomorphic, any theorem that is satisfied by X is satisfied by Y too. Surely this is a good enough reason to call it a theorem about theorems and structures. It must also mean that the proof must use a definition of "theorem" (or "sentence" or whatever the appropriate concept is).

I know. I'll try to explain my point again. The alphabet of any first-order language consists of a set of symbols that all languages have in common, and a set of additional symbols that define the specific language we're dealing with. The latter set is often called the signature of the language. (I have seen other terms for it). What I'm saying is that when we're defining the formal language of set theory, it's absurdly circular to say e.g. that the signature is a finite set of symbols. It's circular because "set" is a concept in the theory we're trying to define, and "finite" is defined by that theory. I don't know how logicians deal with this. I suppose they could just avoid making such claims until the theory has been properly defined. They could define the alphabet by listing all its symbols explicitly, but it seems to me that they would have to think of the symbols as physical objects rather than sets.

On the other hand, if we're talking about some other first-order language, it makes perfect sense to say that its signature is a finite set of symbols, and even that the symbols are sets, because now we're working within the framework set up by the first-order language of set theory.

I don't quite understand. Let X be a structure and consider the following three classes: I={structures that are isomorphic to X}, E={structures that are elementarily equivalent to X}, T={structures that satisfy the same theorems as X}. The theorem implies that I is a subclass of T. Unless I misunderstood you, what you said implies that E is a subclass of T too, and also that T isn't a subclass of I. I'm sure there's some simple piece of information that I don't have that would clear this up, but right now I don't see why membership of I (rather than T) is the appropriate criterion for "equivalent to X for all practical purposes". I also don't see how it's possible for a member of T to not be isomorphic with X (but I suppose I will when I study the proof of the theorem).

Last edited: Sep 11, 2010
16. Sep 11, 2010

### JSuarez

Yes, but for the theorems that may be expressed as sentences in the same first-order language used for the structures. But this is not really important.

Ah! This is the most important point: it's not circular; what you have here is the language/metalanguage distinction. In this case, your language is, for example, the first-order language of ZFC, whose intended interpretation has sets as objects, but when you state that the language's signature is finite (it is a finite set of symbols), you have changed languages and are stating something in your metalanguage. In most cases, if you don't distinguish between the two, the result is inconsistency.

Those may not be sets, but it doesn't affect the response. The catch is that there are mathematical theorems that can't be fully expressed in first-order logic. For example, second-order Peano arithmetic (the so-called Peano axioms) is categorical: any two structures that satisfy them are necessarily isomorphic; but if you consider first-order PA (the usual one in logic textbooks), you have non-isomorphic models; this is because the full induction axiom cannot be formulated in FOL.

17. Sep 11, 2010

### Hurkyl

Staff Emeritus
ZFC is just a second-order formal theory, like any other, and treatable by the methods of formal logic.

What is closer to truth is:
And we can also identify the symbols of the alphabet with the members of a finite set...if we're not talking about the metalanguage of physical symbols on real-world paper and such​
but we can still make an identification; it's just the idea of modeling is more like that used in science than that of formal model theory: we're supposing that these real world objects are described by the mathematical subject of formal logic.

18. Sep 11, 2010

### Hurkyl

Staff Emeritus
Fredrik: I forget, have you seem Skolem's paradox?

There is a the theorem:
There exists a countable model of a first-order version of ZFC​
Skolem's paradox is that this apparently contradicts the theorem that the real numbers are not countable

However, it boils down to a equivocation. There are two notions of countable here: there's "externally countable" in which cardinality is measured by the set theory in which we have built up our methods of set-theory-based formal logic, and there's "internally countable", in which cardinality is measured by the notion of cardinality defined in the formal theory.

The paradox comes from assuming the two notions of countable coincide, but there is no formal reason to do so. This argument refutes philosophical positions that would imply the two notions really should coincide.

(In the above, I'm assuming we have chosen our model of ZFC so that the internal and external notions of set membership coincide -- IIRC there is no loss in generality for making this assumption)

19. Sep 11, 2010

### Hurkyl

Staff Emeritus
Also, note we can recurse. In our countable model of ZFC, we can develop an internal version of formal logic, so now we have an external formal logic and an internal formal logic.

And, of course, we can use this formal logic to study an internal formalization of first-order ZFC, and them....

20. Sep 12, 2010

### yossell

Ha! Ok, I'll try and outline the steps. Let me know when you think things get circular.

In set-theory, you could first define the notion of a well ordering on pairs, <A R>, in set-theoretic terms.

Then define the notion of an ordinal as a transitive set which is well ordered by the membership relation on that set.

Then define an ordering on the ordinals: a < b iff there is a 1-1 mapping from <a, $\in_a$> to a proper initial segment of <b, $\in_b$>

Then define the successor of an ordinal S(x) as x u {x}.

Then define a as a natural number if, for all b < a, b = 0 or b is a successor.

Then you can define $\omega$ as that ordinal which contains all and only natural numbers.

Then make arbitrary identifications between the symbols of the theory you wish to investigate and sets. For instance, let $\all$ be {{}{{{}}}}, let ¬ be {{}{{}}, let $\in$ be {{{{{}}}}}.

Note that there is no circularity here: we are not trying to define the concept of membership here - we are merely identifying the symbol with a particular set.

As we have defined the natural numbers in set-theoretic terms, we are also able to define the variable x_n in set-theoretic terms, say as <{{}}, n>.

In these terms, we can define the predicate SYM(x) in set-theoretic terms, `x is a symbol' - a predicate of set-theory which picks out those sets that are the symbols of our language.

Then we can define a predicate STRING(x) - a finite sequence of symbols as a function from a proper initial segment of $\omega$ to symbols. Because it's a PROPER initial segment of natural numbers, our sequences will be finite.

Then, by mimicking the familiar recursive definitions of well-formedness, we can get a (unnatural, ugly and arbitrary) predicate of set theory WFFx, which says which functions are the wffs.

Of course, there are other ways of doing the same thing: different codings, different definitions of natural number, different ways of defining a finite sequence. There is a worry whether first order set-theory actually has the resources to properly define the notion of a well ordering: a set is well ordered under R iff EVERY subset of S has a least member under R. Some think this notion of EVERY subset of S is not adequately captured in first order set-theory. If you feel this way, then a second order EVERY may have to be used. Perhaps this is what's worrying you? It's certainly worried others.

Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook