Another one is Presburger Arithmetic, which is Peano Arithmetic minus the multiplication. What makes it interesting (and useful) is that this removal makes the theory decidable.

https://en.wikipedia.org/wiki/Presburger_arithmetic

Skolem arithmetic is decidable too: https://en.wikipedia.org/wiki/Skolem_arithmetic

I'm wondering whether there are decidable first-order theories about the natural numbers that are stronger than either Skolem or Presburger arithmetic, that presumably use more powerful number theory. Ask "Deep Research"?

[edit] Found something without AI help: The theory of real-closed fields is decidable, PLUS the theory of p-adically closed fields is also decidable - then combined with Hasse's Principle, this might take you beyond Skolem.

[edit] Speculating about something else: Is there a decidable first-order theory of some aspects of analytic number theory, like Dirichlet series? That might also take you beyond Skolem. https://en.wikipedia.org/wiki/Analytic_number_theory#Methods...

I recently learned about https://en.wikipedia.org/wiki/Self-verifying_theories which gives you most of multiplication while still being decidable, which is pretty crazy.

That's cool, but where does it say it's decidable?

Not on that Wikipedia page, but you might want to have a look at the papers?

Some decidable extensions of Skolem and Presburger, searched for and found by ChatGPT: https://chatgpt.com/share/67e1d302-c930-800f-bc2a-85bdc60563...

There are no specific extensions mentioned, a bunch of math symbol rendering issues, and what seems like maybe some hallucinations? Thanks for proving once again how useless chatgpt is if you're not already an expert on what you're asking it

> fixing the climate

I would be happy to be convinced that climate is an intelligence problem.

One could argue it could be solved with "abundant energy" but if this abundant energy comes from some new intelligence then we are probably several decades away from having it running commercially. I would also be happy to be convinced that we do have this kind of time to act for climate.

I counted one trillion or 9! * 3!^8 * 2 : the 8 because you have can choose 3 independent permutations of columns inside column blocks + 1 permutation of column blocks, plus same for rows. Then only one rotation should be counted, because flips are included in col/row permutations.

I think wreath products relate to the second sentence; see this page, which mentions the same result: https://en.wikipedia.org/wiki/Mathematics_of_Sudoku#The_sudo...

You're correct, the horizontal and vertical flips for the square, are already accounted for in the wreath product. And I miscounted the products themselves. Up to 1.2*10^12 symmetries.

Though burning random cars might be French, we are talking here about arson with precise strategic targets (although I'm not staying this is more Russia's style)

Current discussion: https://news.ycombinator.com/item?id=41076831

The scale is different: "thousands of travellers" vs "hundreds of thousands"

One line was blocked because of "two optic fibers" in Germany "for around three hours".

Now in France three main lines are blocked: West, North, East (+ attempt on South), the disruption will probably last for days, it's a lot more than two optic fibers.

The Eiffel tower's is fun (:

A modular and safe way to achieve this is probably effect handlers. It's like python's yield but can return a value and is scoped like an exception, it's not local to a function call. If you're unfamiliar with it, this article is a good motivation.

Each function, written in direct style, can perform an "effect" when the function wants control to go somewhere else (for c=getchar() and emit(c) here).

Control then goes to the effect handler, in this case probably the caller of the two functions, which decides what to do next: decompressor emits a char? Let's resume the parser's code with the char until it asks for more, then resume decompressor again, etc.

Effects can be efficiently implemented, especially if the continuation is only allowed to be called once (which is the case in OCaml), and allow writing code in direct style, together with type/memory safety. They are also very helpful in a concurrent setting.

An example here : https://effekt-lang.org/docs/casestudies/lexer

Nice!

Note that this page has no category theory yet since it explains sets, so if you already know sets, set product, etc and want to learn about category theory, my advice is to go directly to the next chapter, more specifically to this section:

https://abuseofnotation.github.io/category-theory-illustrate...

which uses set theory terms to define the category theory way of defining products (the corresponding "universal property").

I really like this approach, but it contains some confusing mistakes. For example, unless I'm very much mistaken, the illustration of the initial object is backwards: https://abuseofnotation.github.io/category-theory-illustrate...

The author said he is just starting on the book, so he's not claiming it's perfect. And the beauty of github, open source is you can fix them with a pull request. For example, the svg is here: https://github.com/abuseofnotation/category-theory-illustrat...

> For example, unless I'm very much mistaken, the illustration of the initial object is backwards: https://abuseofnotation.github.io/category-theory-illustrate...

You are right. (Curiously, the picture of the terminal object is correct, so they didn't just switch them!)

Looks fine to me. What's wrong with it?

Author here. It was backwards, I fixed it when I saw the comment. Feel free to report any other mistakes you see on https://github.com/abuseofnotation/category-theory-illustrat... or email.

Seems you might have fixed it before I saw it! Thanks!