Is it possible to translate theorems between isomorphic groups?

[Fredrik]

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.

 

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

 

[Fredrik]

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.

 

[farleyknight]

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.

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?

 

[Fredrik]

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

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

 

[Hurkyl]

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.

 

[farleyknight]

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.

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.

 

[yossell]

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

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?

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.

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 modeled by certain sets; concatenation of symbols is modeled 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.

 

[Fredrik]

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.

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.

 

[Fredrik]

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?

That's what I had in mind.

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?

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

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 modeled by certain sets;

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.

 

[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 think I was a bit confused by the fact that this doesn't make sense for the formal language of set 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.

 

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

 

[Fredrik]

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

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.

I'm not sure what's worrying you in your response to Hurkyl.

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.

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.

Can you tell me how?

...the isomorphism statement is a basic result in classical model theory:

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.

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.

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

 

[JSuarez]

It's more like "is it a theorem in mathematics or metamathematics?"

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.

maybe it's not a theorem in ZFC or any other set theory

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 can see how that makes sense for any first-order language, except the language of set theory.

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

...also a bit disturbing.

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.

This concept of "elementarily equivalent structures" seems to ruin my idea that this theorem...

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

 

[Fredrik]

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.

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'm afraid that I'm missing your question: the languages of almost any formal Set Theories are first-order languages.

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.

No, no: it's the other way around. Isomorphism is the stronger equivalence notion that we have;
...
there isn't a mathematical property that can distinguish between isomorphic structures.

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

 

[JSuarez]

...any theorem that is satisfied by X is satisfied by Y too

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.

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.

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.

Let X be a structure and consider the following three sets...

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.

 

[Hurkyl]

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.

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.

 

[Hurkyl]

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)

 

[Hurkyl]

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

 

[yossell]

Can you tell me how?

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.

 

[Fredrik]

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.

So when the metalanguage refers to a "symbol" or a "set of symbols" (when talking about the first-order language of set theory), what do those terms mean? Should I think of them as physical objects (e.g. the actual symbols on an actual piece of paper)? Edit: That seems to be what Hurkyl is saying in #17.

Those may not be sets, but it doesn't affect the response.

I realized that, and changed the word to "class", but you had already started typing your 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.

So why is isomorphism the appropriate measure of "equivalent for all practical purposes"? Is it that X and Y are isomorphic if and only if they satisfy the same theorems of nth-order logic, for all n?

 

[Fredrik]

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

Is it specifically second order? Not first, and not third? Is there a simple explanation for that?

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.

I'll ask you the same thing I asked JSuarez: When the metalanguage (that we use to talk about the formal language of ZFC) refers to "symbols", should I think of them as physical objects?

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

Interesting. I think I've never heard of that before (so I apologize if you have mentioned it before ). Hm, there's a Löwenheim-Skolem theorem that says something about the cardinalities of models.

 

[yossell]

Is it specifically second order? Not first, and not third? Is there a simple explanation for that?

I'm only used to seeing first order versions of ZF-set-theory.

There are two axioms where we might feel we want to go further than the first order axioms allow. The first is in the comprehension axiom. Intuitively, this says: given a set s, and given absolutely any arbitrary bunch of things in that set, then there's a set t which contains all and only those arbitrary things.

The difficulty is this `any arbitrary bunch of things'. If this just means set, then this axiom has no content. Accordingly, the first order theory tries to get the effect of this axiom by introducing a schema: for every predicate of the language F(x): for any set s, there is a set t which contains precisely those elements u which are in s and which are such that F(u).

The weakness here is that there are only denumerably many such predicate F(x), and so the schema isn't as strong as we would intuitively like - if there is an arbitrary bunch of things that are not definable by a predicate of our language, the axiom schema can fail to guarantee that enough subsets exist. This is why there are non-standard models of first order set-theory, how Skolem's paradox arises.

A solution: second order variables: treat `every bunch of things' as a second order quantification over absolutely every subset of the first order domain. No need for third order.

The other schema that I can recall is the replacement schema. This time, it's a relation that we approximate with a schema, a two-place predicate. Again, the first order theorist approximates it with a set of axioms, the second-order theorist with full quantification over all RELATIONS on the first order domain. No need for anything higher.

 

[yossell]

So when the metalanguage refers to a "symbol" or a "set of symbols" (when talking about the first-order language of set theory), what do those terms mean? Should I think of them as physical objects (e.g. the actual symbols on an actual piece of paper)? Edit: That seems to be what Hurkyl is saying in #17.

Some set-theory allows you to form sets of ordinary objects - so, provided it has some predicates for physical objects, you could do it this way. First order theories contain infinitely many sentences, though, so you'd have to be a little clever to make this reduction.

However, as I tried to outline in an earlier post, they needn't be. The logical-mathematical investigation of languages doesn't require that the languages we work with be concrete or physical; words and languages can be arbitrarily identified with sets and constructions on these sets. A little cleverness has to be applied in coding it up, but everything can be done in pure set theory.

 

[Hurkyl]

Interesting. I think I've never heard of that before (so I apologize if you have mentioned it before ). Hm, there's a Löwenheim-Skolem theorem that says something about the cardinalities of models.

IMO it's worth twisting your mind around. Once you can confidently say "it's obvious there is no contradiction", you have a good chance at avoiding the confusion that can arise from using a set-theory based theory of formal logic to study a set theory.

 

[Fredrik]

Yossell, I don't intend to ignore your posts, but there's some stuff I want to read before I study your posts carefully. So I won't write a real reply today, but I will within a few days.

 

[JSuarez]

So when the metalanguage refers to a "symbol" or a "set of symbols" (when talking about the first-order language of set theory), what do those terms mean? Should I think of them as physical objects (e.g. the actual symbols on an actual piece of paper)? Edit: That seems to be what Hurkyl is saying in #17.

Yossel has already answered this in #24: you don't have to think of them physically; as for their meaning, it's just the 'usual' meaning that we ascribe them when using the metalanguage: a 'set' in the metalanguage is just a collection of objects, while in the object language is an element of the universe of discourse.
This may be confusing because our intuition seeks some sort of 'ultimate' foundation, but the current is shifting from the quest for it (in fact, many people are arguing against its existence or possibility) and focusing instead on foundational problems in logic, set theory, category theory, etc., without giving any of them the status of a foundation.

So why is isomorphism the appropriate measure of "equivalent for all practical purposes"?

The reason is, at least in part, historical. Formal logic only began to be studied and used in Mathematics in the XXth century (and the latter with sometimes stubborn resistence from mathematicians); despite this, isomorphisms are still the most powerful (that I know of) tools for algebraic classification.

Is it that X and Y are isomorphic if and only if they satisfy the same theorems of nth-order logic, for all n?

Usually, a suitable fragment of second-order logic is enough. Full second-order is a mess and higher order may be reduced to the second.

 

[Fredrik]

Yossell: I see now that we've been talking past each other a bit. I was never worried that ZFC can't be used to define the natural numbers and "finite" in a non-circular way. I was only concerned about the moment when you write down the language of ZFC for the first time. At that time, there is no ZFC theory, so I felt that it doesn't make sense to say that the symbols of that language are sets, or that the formulas of the theory are finite sets of symbols.

JSuarez explains this sort of thing by saying that "a 'set' in the metalanguage is just a collection of objects, while in the object language is an element of the universe of discourse." I like this explanation, and I find it very interesting. To avoid the circularity (that we would have been stuck with if we had claimed that the sets of the metalanguage are the sets of ZFC), we have to use a different kind of set. It can't be the sets of the theory we're trying to define. So what are they? We could take them to be the elements of the universe of discourse of another formal set theory, but that would obviously create a problem that's almost identical to the one it solves. So I would say the ultimate foundation* of mathematics is the fact that we live in universe were information can be stored** (e.g. in the form of symbols on paper).

*) It's not an "ultimate foundation" in the sense that it implies that our axioms are true, but it seems to be sufficient to justify the formalism of mathematics.

**) There is of course no way that we could live in any other kind of universe, since consciousness involves time, and temporary storage of information.

JSuarez (or anyone): I'm still not sure what I should say if someone asks me why isomorphism is the appropriate measure of "equivalent for all practical purposes". Isn't there some theorem that gives us a complete answer?

By the way, I have a new question: It's about the = symbol in ZFC. I figured I might as well ask it here instead of starting a new thread. Is there a theorem in ZFC that says roughly that if φ is a formula with x free, then if x=y, we can replace every (free) occurence of x in the formula with y?

 

[yossell]

Yossell: I see now that we've been talking past each other a bit.

That's a shame.

At that time, there is no ZFC theory, so I felt that it doesn't make sense to say that the symbols of that language are sets, or that the formulas of the theory are finite sets of symbols.

I guess I just don't understand your problem.

 

[Fredrik]

That's a shame.

I guess, but it's hard to avoid in forum discussions. Some of what you said was very useful though, especially the stuff on page 1 that forced me to think about what I had said.

 

[Preno]

So why is isomorphism the appropriate measure of "equivalent for all practical purposes"?

Because if we are structuralists, we are only concerned with the roles the elements of a certain structure play, not their absolute identity outside of their interrelations defined by the structure. The integers with addition and the even integers with addition are the same group, because you can do the same groupy things with them. Whether an object is labelled 1 or 2 is irrelevant from the pov of the group - the 2 in the group of even integers has the same role as the 1 in the group of integers. An uncountable group elementarily equivalent with the even integers, however, is not the same group as the even integers, because only one of them has an injective homomorphism to Z.

Is it that X and Y are isomorphic if and only if they satisfy the same theorems of nth-order logic, for all n?

I don't think so. The models of second-order ZF are levels of the cumulative set hierarchy corresponding to some (strongly) inaccessible cardinal (I don't think all of them are models of second-order ZF, though), i.e. are of the form $V_\alpha$, $\alpha$ strongly inaccessible (see the definition). That is, for every two models of second-order ZF, one is an initial segment of the other, so the two are obviously not isomorphic.

[Edit]Of course, if one holds that there are no strongly inaccessible cardinals (or only one), then this doesn't help much.

(Also, as has already been mentioned third- and higher-order logic is reducible to second-order logic.)

 

[Fredrik]

because you can do the same groupy things with them.

Yes, but is there perhaps a mathematical way to say "you can do the same groupy things with them"? My idea that two structures are isomorphic iff they "satisfy the same theorems" didn't work, because I didn't know about "elementarily equivalent structures". But isn't there a modified version of that idea that does work? Your counterexample involves a countable and an uncountable set. What if I change my suggestion to this instead? Two structures of the same type/signature are isomorphic iff their underlying sets have the same cardinality, and they satisfy the same sentences in the first-order language defined by the signature.

A sentence is a formula with no free variables, right? Maybe we should allow free variables too. Then we have to say something about functions that assign values to variables. Let X and Y be structures and |X| and |Y| their underlying sets. Suppose that they have the same cardinality. What if (X,f) and (Y,g_°f) and satisfy the same formulas for each value function f:V→|X| and each bijection g:|X|→|Y|. Isn't that enough to guarantee that X and Y are isomorphic?

 

[Preno]

Yes, but is there perhaps a mathematical way to say "you can do the same groupy things with them"?

Well, yes, namely that they're isomorphic. Why are you seeking another definition to justify that one?

My idea that two structures are isomorphic iff they "satisfy the same theorems" didn't work, because I didn't know about "elementarily equivalent structures". But isn't there a modified version of that idea that does work? Your counterexample involves a countable and an uncountable set. What if I change my suggestion to this instead? Two structures of the same type/signature are isomorphic iff their underlying sets have the same cardinality, and they satisfy the same sentences in the first-order language defined by the signature.

No, that doesn't work. Consider the theory of the successor function (with a single function S and constant 0) with the axioms:

$\forall x \forall y (S(x)=S(y) \rightarrow x=y)$
$\forall x (x \neq 0 \rightarrow \exists y S(y)=x)$
$\forall x (S(x) \neq 0)$
$\forall x (S^m(x) \neq x)$ (this is an axiom schema containing one axiom for each natural m)

This theory has infinitely many mutually non-isomorphic countable models, and these are all elementarily equivalent, because by uncountable categoricity and the Vaught test (or by quantifier elimination), this is a complete theory.

A sentence is a formula with no free variables, right? Maybe we should allow free variables too. Then we have to say something about functions that assign values to variables. Let X and Y be structures and |X| and |Y| their underlying sets. Suppose that they have the same cardinality. What if (X,f) and (Y,g_°f) and satisfy the same formulas for each value function f:V→|X| and each bijection g:|X|→|Y|. Isn't that enough to guarantee that X and Y are isomorphic?

You're being a bit elliptic here, because a valuation is not a function V→|X|, but rather it assigns relations of the appropriate arity to each symbol in the language, but it seems to me that you're basically trying to define Y as the isomorphic image of X, so yes, trivially an isomorphic image of X is isomorphic to X.

 

[Fredrik]

Well, yes, namely that they're isomorphic. Why are you seeking another definition to justify that one?

I told you already: I want to be able to explain why two isomorphic structures can be considered "equivalent for all practical purposes".

No, that doesn't work. Consider the theory of the successor function (with a single function S and constant 0) with the axioms:

$\forall x \forall y (S(x)=S(y) \rightarrow x=y)$
$\forall x (x \neq 0 \rightarrow \exists y S(y)=x)$
$\forall x (S(x) \neq 0)$
$\forall x (S^m(x) \neq x)$ (this is an axiom schema containing one axiom for each natural m)

This theory has infinitely many mutually non-isomorphic countable models, and these are all elementarily equivalent, because by uncountable categoricity and the Vaught test (or by quantifier elimination), this is a complete theory.

OK, thank you for that. I'm not familiar with...any of the things you mentioned after the word "because", but I understand that your point is that my idea doesn't work.

You're being a bit elliptic here, because a valuation is not a function V→|X|, but rather it assigns relations of the appropriate arity to each symbol in the language,

That's not the sort of function I'm talking about. I meant the same kind of function as the w in the definition here.

 

[Preno]

I told you already: I want to be able to explain why two isomorphic structures can be considered "equivalent for all practical purposes".

The definition of isomorphism says that the two structures are the same up to relabelling. Tbqh I don't see what other explanation you're seeking for the fact that they can be "considered equivalent for all practical purposes". Surely if we have a two-element group consisting of elements a,b and a two-element group consisting of elements c,d, then we don't need any additional explanation for why they're the same.

OK, thank you for that. I'm not familiar with...any of the things you mentioned after the word "because", but I understand that your point is that my idea doesn't work.

For all non-negative n, the theory has a model of the form N + n copies of Z, and these models are clearly not isomorphic. But I was saying it can be proven that the theory is complete (it decides all sentences), so any two models satisfy the same sentences.

That's not the sort of function I'm talking about. I meant the same kind of function as the w in the definition here.

Sorry, stupid mistake on my part. Yes, it's just a restatement of the definition of isomorphism, if you unpack the definitions, you get (for f such that f(x)=a, ...):

$(a,b,\ldots) \in \varphi^X \Leftrightarrow (f(x),f(y),\ldots) \in \varphi^X \Leftrightarrow X \vDash_f \varphi(x,y,\ldots) \Leftrightarrow Y \vDash_{gf} \varphi(x,y,\ldots) \Leftrightarrow (g(f(x)), g(f(y)), \ldots ) \in \varphi^Y \Leftrightarrow (g(a),g(b),\ldots ) \in \varphi^Y$

where $\varphi$ is a n-ary relation symbol and $\varphi^X$,$\varphi^Y$ its realizations in X, Y. Similarly for function symbols.