2026-10-07 03:46:28
Gödel’s incompleteness theorem illustrated the need to distinguish between what is true and what is provable. There are true statements that cannot be proven.
Let □p denote the assertion that p is provable in Peano arithmetic. The logic with this interpretation for the □ operator is the Gödel-Löb logic, also called provability logic. This is a normal modal logic with the additional axiom
□(□p → p) → □p,
known as Löb’s axiom.
A couple days ago I wrote about topological models for modal logic. Is there a topological model for Gödel-Löb logic? There is, but it’s not quite the same construction as in the previous post.
A topological model of Gödel-Löb logic associates p with a set P and ◇p with the derived set of P rather than its closure.
The difference between the closure of P and the derived set of P is subtle, but important to this discussion. The closure of a set P is the union of P and all of its limit points. The derived set of P is the set of limit points of P. The distinction is that not every point of P is necessarily a limit point of P. A point x is a limit point of P if every open set containing x contains a point of P in addition to x itself.
A topological space X that models Gödel-Löb logic must be scattered, meaning that every open set must contain an isolated point, a point with no limit points. For example, consider
X = {0} ∪ {1, ½, ⅓, ¼, …}
with the topology inherited from the ordinary topology on the real line. Then every point except 0 is isolated, and every open set contains isolated points.
A statement in Gödel-Löb logic is true if its topological interpretation holds for all scattered spaces.
The post A topological model for provability logic first appeared on John D. Cook.2026-10-04 20:34:22
An earlier post presented an elegant plane geometry theorem discovered by the 19th century school teacher Auguste Miquel. This post presents his pentagon theorem.
Start with a pentagon. It may be irregular, but it needs to be convex.
Extend each of the sides of the pentagon to form a star, then draw give circles, one through each of the triangles formed by a side of the pentagon and a vertex of the star.
The five circles intersect in pairs at ten points: the five vertices of the pentagon and five new points. The five new points lie on a circle.
The converse of this theorem is known as the five circles theorem.
The post Miquel’s pentagon theorem first appeared on John D. Cook.2026-10-04 20:25:19
The previous post discussed a superficial connection between modal logic and topology, that both use the terms regular and normal to indicate added sets of axioms. McKinsey and Tarski developed a deeper connection between modal logic and topology that we’ll discuss here.
Starting with a topological space X and a proposition p, define [[p]] as the set of points in X at which p is true. Define □p to be true at points in the interior of [[p]] and define ◇p to be true on the closure of [[p]].
You could think of □p as the points where p is robustly true. Not only is p true at x, there’s some wiggle room around x, i.e. an open set, in which p remains true.
You could think of ◇p as the points where we cannot rule out the possibility of p being true using open sets. If ◇p includes x, any open set containing x also contains part of ◇p, though it may also contain points outside of ◇p.
For any topology on X, the logic constructed above is normal. The axiom
holds because the closure of a set is the complement of the interior of its complement [1].
Note that this is a regularity result for the modal logic, not the topology. The topology could be arbitrary, and not necessarily regular or normal in the topological sense.
The logic constructed above also satisfies a couple more axioms. We have
because the interior of a set is a subset of the set, and
because the interior of the interior of a set is simply the interior. This means the modal logic corresponding to a topology satisfies the S4 axioms. You could say S4 is the logic that corresponds to the McKinsey and Tarski logic of all topological spaces.
So S4 is the logic that corresponds to all topologies. We could look at more restricted topologies and ask what are their corresponding logics. Or we could start with a modal logic and ask whether there’s a topology that models that logic.
Interesting logics correspond to badly behaved topological spaces. Familiar topological spaces like the real line correspond to S4.
The discrete topology corresponds to the trivial modal logic. All sets are open, and closed, so any set is the same as its interior and its closure. So □p and ◇p reduce to just p.
For the indiscrete topology, □p corresponds to a proposition holding everywhere and ◇p corresponds to it holding somewhere. If the topological space has infinitely many points, the corresponding modal logic is S5. [2]
The cofinite topology on an infinite set X defines a set U to be open if the complement of U is finite. The McKinsey-Tarski logic of the cofinite topology is somewhere between S4 and S5. You can show that the formula
holds, which doesn’t hold in S4, and the formula
does not hold, though it must hold in S5.
[1] We should also verify that if A ∩ B ⊂ C, then Interior(A) ∩ Interior(B) ⊂ Interior(C).
[2] Propositions can only have a finite number of terms. Having infinite points in the topological space prevents the corresponding logic from proving theorems that don’t necessarily hold in S5.
The post Topological models of modal logic first appeared on John D. Cook.2026-10-04 20:24:33
You can’t say much about modal logic in general. You have to be more specific to get anywhere. You have to choose some axioms. Ideally the axioms you need for your application correspond to a named set of axioms that has been studied before.
The situation is similar in point-set topology. You can’t say very much about a general topological space. You have to specify some separation axioms to get going.
A modal logic is any set of formulas in the modal language that:
In particular, this definition requires nothing of the modal operator □ (“box”). You just have propositional logic with a funny symbol added that could mean anything.
A topological space is a set X along with a set of subsets of X called open sets. The empty set and the full space X are open sets. Furthermore, the set of open sets is closed under finite intersections and arbitrary unions.
There’s not much you can say about topological spaces in general because, for example, the definition includes extreme cases such as the discrete topology (every subset of X is open) and the indiscrete topology (only the empty set and X are open).
Like many areas of mathematics, logic and topology use the terms “regular” and “normal” to refer to systems with common choices of extra structure.
A regular modal logic is a normal modal logic with a second modal operator ◇ (“diamond”) that satisfies
◇ p ⇔ ¬ (□ ¬ p)
and has the inference rule (p ∧ q) → r implies (□p ∧ □q) → □r.
A modal logic is normal if it satisfies the axiom
□ (p → q) → (□ p → □ q)
and the inference rule that if p is a theorem, □p is also a theorem.
Topology also uses regular and normal to refer to adding a few axioms.
A regular topological space is one in which you can separate points from closed sets. Given a point x and a closed set F not containing x, there exist disjoint open sets U and V such that x is contained in U and F is contained in V. [1]
A normal topological space is one in which you can separate disjoint closed sets.
For many mathematicians, a metric space is the weakest topology they’re interested in, and metric spaces are normal. But weaker topologies come up. The Zariski topology in algebraic geometry is not regular, and the weak topology on an infinite dimensional Banach space is regular but not normal.
[1] Why do we use F to denote a closed set? It’s a convention that goes back to the French word fermé for “closed.”
The post Modal logic and topology first appeared on John D. Cook.
2026-10-04 06:53:41
Euclidean geometry dates back at least to Euclid (circa 300 BC), and so you might think it’s been pretty well picked over by now. And yet people still occasionally discover new plane geometry theorems.
Some of these new theorems are complicated, asking question that the ancients would not have asked. But once in a while someone discovers a gem that the ancients could have appreciated but didn’t find.
One example is Miquel’s pivot theorem [1]. The theorem was discovered in 1838, which relative to the timeline of Euclidean geometry makes it a recent discovery.
Choose a point on each side of a triangle. Then for each vertex draw a circle through it and the chosen points on the adjacent sides. Miquel’s theorem says the three circles meet in one point.
Here’s an example. For a trangle ABC, choose points D, E, and F on each side. The three circles described in the theorem intersect at M.
Now the three points D, E, and F don’t have to be limited to the sides of the triangle; they can be on the line segment containing the side. Here’s an example where D is outside the triangle.
And here’s an example where two of the chosen points, D and F, are outside the triangle. The three circles still intersect at one point M.
[1] Miquel, Auguste (1838), “Mémoire de Géométrie”, Journal de Mathématiques Pures et Appliquées, 1: 485–487
The post Miquel’s pivot theorem first appeared on John D. Cook.2026-09-25 19:45:31
Despite the predictions that no one would ever put build data centers in space, Google is starting on Thursday. Google’s prototype satellite will be one of 130 payloads on SpaceX’s Transporter 18 mission on October 1.
The server will follow a dawn-dusk orbit, a special case of a sun-synchronous orbit (SSO), following the terminator line between daylight on dark on the earth below. A dawn-dusk orbit allows the satellite’s solar panels to stay in nearly continuous daylight, while also being in a relatively inexpensive low earth orbit (LEO). Geostationary orbit (GEO) would allow solar panels to always receive sunlight, but launching a satellite into GEO requires more fuel and so is more expensive.
Another advantage of LEO is that radiation levels are a couple orders of magnitude less than at GEO. Lower radiation means electronics do not need to be as hardened against radiation.
A dawn-dusk orbit would not be possible if the earth were perfectly spherical. The earth’s equatorial bulge makes it possible to design an orbit that precesses once per year. David Hammen explains this in an answer to a question on the Space Exploration Stack Exchange site.
If the Earth had a spherically distributed gravitational field, a satellite’s right ascension of ascending node would be constant. … Fortunately, the Earth’s gravitational field is not spherical. The Earth’s rotation results in an equatorial bulge. This equatorial bulge causes RAAN to precess (or recess). …
Sun synchronous orbits are chosen so that RAAN precesses by 360 degrees per year, or a bit less than one degree per day. …
A dawn-dusk satellite is a special case of a sun synchronous orbit. … A dawn-dusk orbit typically does not quite follow the terminator. Following the terminator would require a rather high orbit.
