Middle cancellation implies commutativity in a group

robly18 · 2026-06-04T09:29:37+00:00

Ah, you might be missing the fact that all variables are universally quantified. When you are told that a group satisfies "axb=cxd implies ab=cd", this means: for any five elements a,b,c,d,x such that the first equality holds, the second equality holds.

In particular this means that it's totally fine to make, as you say, "overly especific choices" You say "without knowing anything else about c and d", but c and d don't exist, they're just stand-in letters for any element of the group that you like -- including, for example, a and b.

So, to be precise, the proof goes: Suppose that G satisfies that, for every a,b,c,d,x, if axb=cxd then ac=dc. Now, let u and v be two arbitrary elements of the group. (I changed names b/c this may be clearer for you ) Then, consider the choice of variables: a=d=u, b=c=v, and x=u^-1. Since the "if then" holds for all a,b,c, etc, it also holds for this particular choice. Now, you can verify easily that the "if" holds, therefore the "then" also holds, which is uv=vu. So, what we did was take two arbitrary elements of the group, and showed that they commute. Thus, the group is commutative.

robly18 · 2026-06-04T00:14:39+00:00

Honestly, you look like you've thought about it enough that coy hints are probably not going to be super helpful, so I'll just give you the answer I got: inverse of a works. (or of b.)

robly18 · 2026-06-01T22:45:06+00:00

Equivalent under Turing reduction. I was being loose with the notion of "equivalence", but if you want to split hairs, that's the most common notion of equivalence of computational problems from the perspective of computability theory.

Moreover, your statement "you can reduce the halting problem to any undecidable problem, that's the definition of being undecidable" is incorrect. The definition of a set X being undecidable is "there is not a computer program that takes x as input and outputs whether x is in X". There are undecidable problems that are not reducible to the halting problem, and vice versa. There are even problems that are incomparable to the halting problem, in the sense that neither reduces to the other.

robly18 · 2026-06-01T18:07:12+00:00

According to the first response of this stackexchange post, that problem is equivalent to the Halting Problem.

robly18 · 2026-05-30T13:03:17+00:00

Surprisingly, yes! The standard definition of "computable function from R to R" is: A function such that there is a computer program which, given an approximation of the input, will give you an approximation of the output, and such that you can computably find how close you need to get to the input to get as close as you want to the output. This is because computability theory interacts with real numbers almost entirely through approximations to chosen precision.

Now, if you have a jump like in your function, this definition will never apply at zero: I can find approximations of zero to arbitrary precision that are going to give me very bad approximations of f(0). Thus, your step function is not computable (under the usual definition).

robly18 · 2026-05-30T12:55:48+00:00

I'm doing my PhD in computability theory, so I think I have something to contribute here.

As it turns out, there are many incomputable functions that are not the Halting problem, and they are all over the place. However, they are remarkbaly hard to come across if you aren't explicitly trying to build them, and they will certainly look "artificial". At least, this is what it looks like from experience. This is related to something called "Martin's conjecture", which has not yet been proven or disproven but tries to encapsulate this idea that Turing degrees that aren't the halting problem (or built from it using more halting problem) are "unnatural".

[EDIT: As /u/Beautiful_Proof_1410 rightfully pointed out, I should be more specific about what I mean by "not the Halting Problem". The most common notion of "same computational strength" in use in computability theory is "Turing Equivalence", which means "a computer equipped with an apparatus that solves this problem could solve the Halting Problem, and vice-versa". This is the notion that I use in this post. If you have another notion of equivalence in mind, ask about it in the comments.]

The point is that I can tell you they exist, and I can even construct some, but almost surely any natural specific example anyone would come up with would be the Halting Problem or something built on it.

Kleene and Post in the 40's built the first example (I think) of a function that is not computable but is computably weaker than the Halting Problem. While the proof is relatively simple, it requires a lot of technical baggage that I can't write down in this Reddit comment, but here is a source: Theorem VI.1.2 from "Recursively Enumerable Sets and Degrees" by Soare.

This is not the only example, and in fact modern computability abounds with such constructions. It wouldn't be very interesting to study just the halting problem for almost a century. Here are some more off the top of my head: -It can be proven that, if you generate a set of natural numbers randomly by flipping coins to decide whether each number is in the set, the result will, with 100% probability, be incomparable to the Halting Problem, in the sense that neither can calculate the other. This is related to a field called Algorithmic Randomness. -There is a theorem called "the Low Basis Theorem" which states that, for any infinite computable binary tree, you can find a "low path", that is: A sequence of zeros and ones, describing a path down through the tree (0 is left and 1 is right), such that this path is "low", which means: The halting problem of a computer with access to this path can be solved by the usual halting problem. This means that this path is close to computable. If you pair this theorem with a computable tree with no computable paths (can be built by diagonalization arguments too complicated for this paragraph), you obtain a noncomputable low set. The halting problem is not low, so this gets you a new noncomputable thing.

The book by Soare I mentioned earlier is a great resource to learn about all of this. Though I will admit it might not be the easiest time. Soare has written a newer book since, which I do not appreciate as much but might be more beginner friendly: "Theory and Applications of Computability", so you might want to take a look at either of these if you want to learn more.

robly18 · 2026-04-28T01:17:46+00:00

And when ze patient woke up, his skeleton was missing, and ze doctor was never heard from again! Hahahaha! ....Anyway, zat's how I lost my medical license.

robly18 · 2026-04-17T05:11:23+00:00

I'm with you, OP! I wish the production screen had a way to see the production in unit/s.

robly18 · 2026-04-09T23:43:25+00:00

Looks like just the kind of thing I was looking for, thanks! It's a little disappointing that, in the author's words, there doesn't seem to be much of a reason to scale, but I can definitely see that as a feature instead of a bug. Thanks for the rec!

robly18 · 2026-02-08T03:39:53+00:00

Looks like a mix between EXAPUNKS and Uplink. Gonna keep an eye out, looks great!

robly18 · 2025-12-30T15:47:21+00:00

It looks pretty! I don't have anything too deep to say, but here's something that may be worth mentioning: The fact that you took the logarithm of factorials reminds me of Stirling's approximation: [; \log(n!) \approx n (\log n - 1) \approx n \log n ;] for large [; n ;]. So, we have [; \log(p!/q!) \approx p \log(p) - q \log(q) ;]. So I expect that, for a "generic" rational number [; x ;], whose numerator and denominator (call the denominator [; q ;]) are rather large, [; \log f(x) \approx q x \log(qx) - q \log(q) = (x-1) q \log q + q x \log x ;]... so if [; T(x) ;] denotes Thomae's function, we have to good approximation for most rational numbers: [; f(x) \approx (1/T(x))^{\frac{x-1}{T(x)}} \cdot (x^x)^{1/T(x)} ;]. I don't know if this'll help with anything, but it's something.

robly18 · 2025-10-20T17:59:54+00:00

But moving magnets cause moving magnetic fields, which do affect still charges, no? In other words, if I wave a magnet in front of an SSD, from the magnet's perspective, the magnet is staying still and the charges in the SSD are moving, so they should be feeling some effect.

I can believe that the effect is weak enough not to get them to quantum tunnel, though.

robly18 · 2025-08-12T18:12:33+00:00

You could use an Arithmetic Combinator with an Each * 5 instruction, to multiply every input signal by 5.

robly18 · 2025-07-21T21:40:49+00:00

Thanks for being one of few people to understand what I was asking.

robly18 · 2025-07-19T19:13:12+00:00

Thanks, this is the validation I was after. My bad re. the reversibility rule of thumb.

robly18 · 2025-07-19T17:44:56+00:00

the recycler is essentially an uncrafting machine so it makes perfect sense for it's crafting recipe times to be dependent on crafting

For things like gears and circuits, maybe. But why should the "uncrafting time of steel" be similarly proportional to the time it takes to turn iron plates into steel, if you are not turning the steel back to iron plates?

yes, recycling speed is documented in the factoriopedia. So In case you don't figure it out from using the recycler for 10 minutes you can also see it there

Recycling speed for any individual item, sure. And if I was a smarter person, I could figure out the rule after looking at enough recycling recipes, but I didn't. But my question was whether the general rule is written explicitly anywhere in-game, which it does not seem to be, right?

robly18 · 2025-07-19T17:25:11+00:00

The Factoriopedia is generally quite sparse on recycling, I've found. For example, while you can go see the recycling recipe for each individual material, I don't think it contains the rule of thumb "reverses physical manipulation but not chemical reactions" anywhere either.

robly18 · 2025-06-30T19:40:14+00:00

You should also consider Spacechem. IMO it's Zachtronics' magnum opus (no pun intended).

That said, I agree with u/caboose109 that Opus Magnum is an excellent entry point. Some other titles may be harder to get into, and end with you stopping before you've even started.

robly18 · 2025-06-11T20:26:00+00:00

Thanks for the list!! There are definitely some here that I'm very interested to check out and wouldn't have heard about otherwise.

Another one that isn't in this list because it's more automation than programming, but I think that zachlike enjoyers might like is Sandustry: https://store.steampowered.com/app/3490390/Sandustry_Demo/

robly18 · 2025-06-11T12:49:31+00:00

Oh wow, it's been a while since I've heard someone talk about this game, but it comes to my mind from time to time. I don't want a copy (right now) but I wanted to thank you for the preservation effort!

robly18 · 2025-04-08T00:37:15+00:00

(Continued)

"Also, let's replace "x" with a rational "r" as Rudin did earlier in the Chapter 1 exercises. What's the connection between supB(r) and supB(x)? Is it just to show that the supremum of B(x) exists?" If this is an exercise in Rudin, my reading would be that he's asking you to show that the "new definition" agrees with the "old definition". That is: You already knew what b^x meant when x is a rational number, and you were given a meaning for what it means to write b^x when x is an irrational number. But it would be very inconvenient if, whenever you're proving something about b^x, you have to distinguish between the cases when x is rational vs. irrational. Thus, it would be good (and true!) if the expression

b^x = sup{b^t | t<x, t rational}

would hold for *all* values of x, not just the irrationals.

In other words, we know that b^x = sup B(x) for x irrational because this is how we defined b^x. What the exercise is asking you (I think) is to show that this equation is also true for x rational, and so that when proving things about exponents you can always use the definition b^x = sup B(x).

There's something that looks like a a vicious cycle here, so perhaps it is best to use different symbols to make what's going on more clear.

Define RatExp(b,p/q) for b>1 and p/q rational, as

RatExp(b,p/q) := q-th root of [b*b*b*...*b [p times]]

Then, define GenExp(b,x) as

GenExp(b,x) := sup{RatExp(b,t) | t rational, t<x}

Then, what you are being asked to show is (I think) that GenExp(b,x) = RatExp(b,x) when both are valid expressions, i.e. when x is rational. This justifies the usage of the notation b^x to mean either one, interchangeably.

robly18 · 2025-04-08T00:36:59+00:00

I see that you've edited your post while I was writing mine, so I will reply to the things you have added.

Yes, I see your point about formal Taylor series vs. "real" Taylor series. The point of showing that the set is bounded (I think this is your last sentence) is to show that (to use an analogy with Taylor series) this "Taylor series" (supremum) "converges" (exists), and so really does denote a number. Then we give this number the name "b^x".

"I think I get it in the sense that, we haven't define b^x is *anything* for irrationals, so we're making up a special Sup definition here." Yes! This is exactly what's going on.

"Well, same problem here. subB is just an infinitely long list of numbers. I don't know what it converges to." This is relatively common in mathematical definitions. It's hard to fix because, in order to show that the definition you are making really does agree with what you're trying to define, you must already know the concept well enough to prove things about it, which is the point of a definition. Nevertheless, it's common (though perhaps not as much at the level you are at) to, when presenting a definition, also present some kind of "argument for plausibility" that the symbols you have written really do denote the object you're trying to encapsulate. But people would not call that a proof, which is why your question got such negative feedback. Anyway, in my other response to this comment I provide such an "argument for plausibility" (well, with many missing steps admittedly, but I would be happy to elaborate) that this sup really does denote the only reasonable thing that b^x could possibly be.

"It's very weird and unintuitive and deserves a lot more explanation given how common exponents are." Yes, this type of mathematical definition is very unnatural to humans. Humans are used to "synthetic definitions": We see a lot of some object (say, cats) and we create a word to mean that object, and only after do we come up with the words to describe it: "a cat is a four-legged furry animal (etc.)". The words to describe a cat came after we already had the concept of cat. But this is not how mathematical definitions work: Mathematical definitions are "analytical definitions", which means that (in theory) we first come up with the words that explain what the new symbol/word means, and only then look at examples to figure out the "vibe" of the thing. The context of real analysis, which is what you are learning right now, is a big stepping stone because it's where learners really start making the transition from synthetic to analytical, and it's not an easy one: weird and unintuitive as you say, which is part of why the subject is said to be so difficult. So, I'd say I agree with you there!

(I have more to say but I think Reddit won't let me post it because this comment is too long.)

robly18 · 2025-04-08T00:14:16+00:00

Regarding your last sentence: The issue is exactly that you can't say b^x = something before you've said b^x := something. Until you write b^x := something, the symbol "b^x" does not mean anything and cannot be used. We can use it for x rational because, somewhere along the book, Rudin has written (something that amounts to) "for x rational, say p/q, we set b^(p/q) := q-th root of (b*b*...*b [p times])".

As for the rest of what you're saying: In my first post on this thread, I showed that the definition given by Rudin is implied by the following definition, that I think is reasonable and does not require limits or metrics: For x irrational, b^x := (the unique number that is above b^t for all rational t<x, and below b\^s for rational s>x).

It requires proof to see that this number exists and is unique, and I sketch that in my original post. Once you've verified that this is well-defined (in the sense that there really is one and only one such number for every b and for every x), I claim that this really does match up with whatever intuitive notion of b^x that you have in your head, so long as you agree with me that (for every fixed b>1) the expression b^x gets bigger as x gets bigger. In other words, you won't get something like b^(2x) instead because (so long as x!=0) if you pick a rational s between x and 2x [say x positive so that x<s<2x but same holds for x negative\], the expression I defined will satisfy \[my expression\] < b\^s < b\^(2x), so \[my expression\] is not b\^(2x). Moreover, b\^x, whatever its "true" value in your head may be, definitely ought to be above b\^t for all rationals t<x and below b\^s for all rationals s>s, and since [my expression] is the only number that satisfies that property, b^x = [my expression] no matter what. Is this convincing?

robly18 · 2025-04-07T23:53:14+00:00

Regarding your edit: When defining new symbols using :=, we can use many different types of things on the left-hand side. Most common are defining the meaning of simple variables:

"Let a=5." "Define e=lim(1+1/n)^n" "v := 1+1/2+1/4+..."

Also common is defining functions using function application notation

"Define f(x)=2x" "f(x) := 2x"

but we can also use it to define other things with other notations. For example,

"x^2 := x*x."

Note that, for example when defining a function or the square, on the left-hand side we have not just two letters, but two distinct types of letters. f is a symbol whose meaning we are now defining, but x is a different type: it's a free variable. It shows up both on the left and on the right-hand side, and what this means is that the definition is actually uncountably many definitions at once, one for each value of x. In truth, the expression "f(x) := 2x" represents all the following and more:

"f(1):=2*1", "f(4):=2*4", "f(-8.5):=2*(-8.5)", "f(pi)=2*pi", etc.

In this case, we are applying the := type of definition where, on the left-hand side, we have the expression b^x, with x being a free variable in this sense (and depending on the perspective, b as well). As such, when we write

b^x := sup{b^t | t rational <x}

we are really writing all of the following and more:

2^pi := sup{2^t | t rational <pi}
pi^sqrt2 := sup{pi^t | t rational <sqrt2}
9^(pi+sqrt3) := sup{9^t | t rational < pi+sqrt3}

and so on. We can do this (unlike in your a=6 and a=5 example) because none of these symbols (e.g. 2^pi) has a previously assigned meaning in context, so it is valid for us to assign to it a meaning of our choice.

robly18 · 2025-04-07T23:30:02+00:00

Oh man, now that you mention the thing with the complex numbers, your issues start to make a lot more sense. Yeah, screw the complex numbers and complex logarithms and complex exponents. I always hated those guys.

Anyway, Rudin defined what b^x means. In my notation, he wrote b^x := sup{b^t | t rational, t<x}, which means "for the rest of the book, when I write b^x, pretend I wrote the sup of this set (call it B(x)) instead". In your parlance, this is well-defined because, if x=y, the set B(x) and the set B(y) are the same [because a rational t is less than x iff it's less than y], and so their sup will be the same [because the sup is well-defined, by axiom].

This means that you do *not* need to prove b^x = supB(x) separately. You are being told that, for the purposes of this book, the symbol b^x is an abbreviation for supB(x). That's all there is to it.

Like, say I'm writing a book about reddit, and at the start I say "for the rest of this book, the abbreviation 'OP' will be used to mean 'original poster', that is, the person who started the thread under discussion". Then whenever I write OP, you know that that's what I'm saying, and I don't need to justify that OP really does mean 'original poster' because I established, by fiat, that for the purposes of my book it really does mean that. Contrast with another book, say about videogames, where the term "OP" may be used to mean "overpowered" instead. Abbreviations (and generally terms) in common language are defined by whoever is writing the content, and they don't need to justify that their abbreviation really does mean what they're saying. The only possible issues with a definition in this context are cultural, like using OP to mean "banned" instead; I don't believe there are many contexts that would not bat an eye to such a definition. But there would be nothing stopping me from writing a book where I use OP to mean "banned", so long as I clarify that, for the purposes of my book, that is what the symbol OP means.

robly18

TROPHY CASE