Categorical models of logics

A few days ago I wrote about topological models of modal logic. If you find general topology more familiar than modal logic, this correspondence could be helpful. If you think the motivation for general topology is evident but the motivation for modal logic is suspect, the correspondence between the two fields might relieve some of your suspicion of the latter.

Topological models, however, are quite limited. You can’t model provability logic, for example, by the usual approach to constructing topological models, though there is an alternative construction.

Categorical models are less limited. You can model a wide variety of logics using categories via the Curry-Howard-Lambek correspondence. This may be cold comfort if you find category theory and logic equally mysterious. Even so, there’s something intriguing about a correspondence between two things you find mysterious.

Categorical semantics is deep and broad, but I’ll keep this post brief. The correspondence between logic [1] and categories [2] is summarized in the table below.

\begin{tabular}{ll} \hline \textbf{Logic} & \textbf{Category theory} \\ \hline Proposition / formula & Object \\ Proof of \(A\) from \(\Gamma\) & Morphism \(\Gamma\to A\) \\ Truth \(\top\) & Terminal object \(1\) \\ Falsehood \(\bot\) & Initial object \(0\) \\ Conjunction \(A\land B\) & Product \(A\times B\) \\ Disjunction \(A\lor B\) & Coproduct \(A+B\) \\ Implication \(A\to B\) & Exponential \(B^A\) \\ Negation \(\neg A\) & Exponential \(0^A\) \\ \hline \end{tabular}

It’s interesting how model logic fits into this picture. Axiom K, required by normal modal logics, says

\Box(A\to B)\;\longrightarrow\;(\Box A\to\Box B)

In categorial semantics, this says this says the box operator □ is a functor, mapping objects representing propositions to objects representing propositions, and mapping morphisms representing proofs to mapping morphisms representing proofs.

Related posts

[1] More precisely, intuitionistic propositional calculus.

[2] More precisely, bicartesian closed categories.

Consequences of progress toward the Riemann Hypothesis

The Riemann Hypothesis (RH) is the conjecture that all the zeros of the Riemann zeta function ζ(s) in the critical strip, i.e. the region of the complex plane with real part between 0 and 1, have real part equal to ½.

The Quasi Riemann Hypothesis (QRH) says that there exists a constant θ < 1 such that no zeros of ζ(s) have real part greater than θ. OpenAI has published a paper claiming QRH with θ = 7/8.

The RH is so important to number theory that even partial results can have big consequences. This post will focus on one consequence: the error term in the Prime Number Theorem.

The Prime Number Theorem says that π(x), the number of primes less than x, is asymptotically equal to Li(x). We’d like to know more specifically at what rate π(x) approaches Li(x).

The best known result before the QRH announcement was

\pi(x) = \operatorname{Li}(x) + {\cal O} \left(x \exp\!\left(-c\,\frac{(\log x)^{3/5}}{(\log\log x)^{1/5}}\right)\right)

If the QRH holds for some θ, such as OpenAI’s assertion that θ = 7/8,

\pi(x) = \operatorname{Li}(x) + {\cal O} \left(x^\theta\,\log x\right).
If RH holds, θ = ½.

Incidentally, you may have seen the Prime Number Theorem stated with x/log(x) rather than Li(x). These two functions are asymptotically equal, so they give the same theorem, if you’re not interested in quantifying the rate of convergence. The function Li(x) gives better error bounds.

Faster Fourier Transform

The Fast Fourier Transform (FFT) algorithm can compute the discrete Fourier transform of a sequence of length n in time

O(n log n).

OpenAI recently posted a paper saying there is an algorithm that could compute the discrete Fourier transform in

O(n (log n)1 − ε)

time for ε = 10−13.

This result is amazing. It seemed that O(n log n) was as good as you could do, which it provably is for sorting algorithms.

The result is also of absolutely no practical value, for now. But since the theorem shows that our assumptions were wrong, however slightly, about what is possible, maybe we’re in for further surprises. Maybe the ε crack will grow. It wouldn’t be the first time.

Related posts

Irrationality exponent of π

For a real number x, the irrationality index μ(x) is a way of measuring how well x can be approximated by rational numbers. If x is rational, μ(x) = 1. If x is irrational, μ(x) ≥ 2.

OpenAI recently published a proof that μ(π) = 2. Almost all real numbers have irrationality exponent 2, so the new result says π is typical in this regard. There are numbers proven to have irrationality index greater than 2 (more on that below), but π isn’t one of them.

The irrationality exponent μ(x) is defined as the supremum of the set of values ν such that

0 < \left| x - \frac{p}{q} \right| < \frac{1}{q^\nu}

for infinitely many coprime integers p and q with q > 0.

This means that the approximation error for approximating π with a rational number p/q is typically on the order of 1/q², just like most irrational numbers.

There are numbers with higher irrationality exponents. For example, Cahen’s constant C has irrationality exponent 3. This means C is an irrational number that has infinitely many rational approximations p/q with error less than 1/q³.

Lissajous and Bowditch

I was skimming through David Well’s book The Penguin Dictionary of Curious and Interesting Geometry and was surprised by this entry:

Lissajous figures or Bowditch curves First discussed by Nathaniel Bowditch in 1815, and later by Jules Antoine Lissajous in 1857 …

I wrote a couple posts about Lissajous curves years ago, and recently I wrote a couple posts about Nathan Bowditch, but I didn’t realize there was a connection between them.

I asked Claude to pin down Bowditch’s publication to see whether the curves came up in the course of his work on navigation. Here’s the answer I got.

Bowditch’s paper was “On the Motion of a Pendulum Suspended from Two Points,” published in the Memoirs of the American Academy of Arts and Sciences (Vol. 3, Part 2) in 1815.

He studied a compound pendulum hung from two points (a Y-shaped suspension, sometimes called a Blackburn pendulum). This lets the bob swing at different frequencies in two perpendicular directions, and he worked out mathematically the curves the bob traces. Those curves are what we now call Lissajous figures. Jules Antoine Lissajous studied them independently and much more visibly in 1857, using light beams reflected off vibrating tuning forks, and his name stuck. Because of Bowditch’s priority, the curves are sometimes called Bowditch curves.

A topological model for provability logic

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.

Miquel’s pentagon theorem

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.

Modal logic and topology

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.

Bare bones

Modal logic

A modal logic is any set of formulas in the modal language that:

  1. contains all propositional tautologies,
  2. is closed under modus ponens, and
  3. is closed under uniform substitution.

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.

Topology

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

Regular and normal

Like many areas of mathematics, logic and topology use the terms “regular” and “normal” to refer to systems with common choices of extra structure.

Modal logic

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

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.

Related posts

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

 

Miquel’s pivot theorem

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.

Related posts

[1] Miquel, Auguste (1838), “Mémoire de Géométrie”, Journal de Mathématiques Pures et Appliquées, 1: 485–487

Navigation with only addition, subtraction, and tables

In the novel Carry On, Mr. Bowditch, a sailor asked Nathaniel Bowditch to teach him how to do navigational calculations, but the man only knows how to add and subtract by counting on his fingers. He had not heard of multiplication. Bowditch is surprised, but realizes if he made tables of logs of trig functions, then it would be possible for barely numerate sailors to calculate their position.

Carry On, Mr. Bowditch is fiction, but it’s essentially factual, and so I imagine something like the conversation above did happen. I thought about how this might work, and it would be difficult.

It is true that if someone can add, subtract, and look-up numbers in a table of logarithms, they can effectively multiply. To find the product xy, they would look up the logarithms of x and y, add the results, then use the table in reverse to find what number has a logarithm equal to the sum.

Difficulties

But there are a couple difficulties in this imagined scheme. First, every calculation would require a lot of steps, including looking up numbers in multiple tables. It’s likely someone who cannot multiply also cannot read, so writing down instructions might not be viable. Second, carrying out calculations using tables is usually not simply a matter of looking up numbers; there are other things someone would need to know, such as interpolation and range reduction.

Bowditch was trying to train innumerate sailors to do specific calculations, not general mathematics, and so there would be ways to mitigate the problems above. Maybe he could create diagrams that would allow a semi-literate person to carry out an algorithm. The sailor wouldn’t need to be able to read per se. The instructions could be aids to help him recall memorized steps. The specialized nature of the calculations might also eliminate the need for range reduction and interpolation.

Tables

How many tables would be necessary? Someone who understands trigonometry doesn’t need separate tables for sine and cosines. And they wouldn’t need a table with entries for all angles. A table of sines for angles between 0 and 45° would be enough. But someone who doesn’t know multiplication would need more tables and bigger tables. Or they would need instruction in how to get by with less. It would be an interesting trade-off.

The novel mentioned tabulating logs of trig functions. For example, if you need to calculate

cos(a) cos(b)

it would be convenient to be able to look up log(cos(a)) and log(cos(b)) rather than look up the cosines and then look up their logs. But you’d still need to be able to convert

log( cos(a) cos(b) )

into

cos(a) cos(b).

This would require a table of logarithms, if the user is able to infer exponentials by reading a table in reverse. Otherwise you’d need a table of exponentials.

In general, you can assume less sophistication from a user by increasing the number of tables. But this also complicates the instructions the user must follow.

To give a specific example, suppose a sailor wanted to calculate his position using the law of haversines:

hav(c) = hav(a − b) + sin(a) sin(b) hav(C).

A mathematically sophisticated sailor would only need a table of sines to infer c from a, b, and C. He could calculate haversine via

hav(θ) = sin²(θ/2),

though inverting hav(c) to solve for c would require calculating a square root, either directly or via a table.

If one were to minimize the amount of sophistication needed by maximizing the use of tables, the algorithm for finding c would be

  1. Subtract b from a and look up the haversine of the difference.
  2. Look up log(sin(a)) and log(sin(b)) from one table and log(hav(C)) from another and add the results.
  3. Take the exponential of the result in the previous step using a table of exponentials.
  4. Add the results of steps 1 and 3, and look up the result in a table of inverse haversine values.

This would require five tables: sine, log sine, log haversine, exponential, and inverse haversine.

Condescension

Bowditch’s effort to make navigation accessible to the uneducated is an example of condescension in its literal and positive sense. If we say a person is condescending, we imagine an arrogant person who belittles those around him. But condescension literally means coming down to be with someone. Theologians use the word to describe the incarnation of Christ.

Like all scholars, Bowditch wrote for his peers, notably in his English edition of Laplace’s magnum opus on celestial mechanics. But unlike most scholars, he also devoted years of his life to a making knowledge accessible to uneducated men, culminating in his book The New American Practical Navigator, still in print here [1].

Related posts

[1] The book has been updated over the last couple centuries. Obviously the section on GPS, for example, does not date back to Bowditch.