Privacy policies and modal logic

Posted on by John

If you’ve followed this blog for a while, you may know that I do a lot of work with data privacy and that I have an interest in modal logic. Recently these two worlds collided: I became aware of work that uses modal logic to reason about data privacy.

The story begins with Helen Nissenbaum’s paper Privacy as Contextual Integrity [1]. Rather than simply classifying data as public or private, Nissenbaum looks at norms around the context in which data exists and moves.

… the benchmark of privacy is contextual integrity; that in any given situation, a complaint that privacy has been violated is sound in the event that one or the other types of the informational norms has been transgressed.

A couple years later Nissenbaum coauthored a paper [2] with three Stanford computer scientists using modal logic, specifically linear temporal logic (LTL), to reason about contextual integrity. The paper uses four modal operators: the usual box and diamond, plus past tense versions with a minus sign across the middle.

box, diamond, box minus, diamond minus

These four operators can be read as “henceforth”, “eventually”, “historically”, and “once.”

Henceforth means something will always be true into the future; historically means something was always true in the past.

Eventually means something will happen at some time in the future; once means something occurred at some time in the past.

You could imagine using these operators to formalize statements such as data sharing in some context is permissible (henceforth) if the data subject has (once) signed a consent form.

Understanding simple stand-alone policies does not require the machinery of formal logic, but analyzing large collections of interacting policies may. It may be, for example, that a collection of policies cannot all be satisfied, though this is not obvious from looking at the individual policies. Formalizing policies in the language modal logic makes their analysis amenable to well established algorithms.

Related posts

[1] H. Nissenbaum. Privacy as contextual integrity. Washington Law Review, 79(1):119–158, 2004.

[2] A. Barth, A. Datta, J. C. Mitchell, and H. Nissenbaum, “Privacy and contextual integrity: Framework and applications,” in Proc. 2006 IEEE Symp. Security and Privacy (S&P’06), Berkeley/Oakland, CA, USA, 2006, pp. 184–198, doi: 10.1109/SP.2006.32.

Consequences of progress toward the Riemann Hypothesis

Posted on by John

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

Posted on by John

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 π

Posted on by John

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

Posted on by John

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

Posted on by John

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

Posted on by John

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.

Topological models of modal logic

Posted on by John

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.

Regularity

For any topology on X, the logic constructed above is normal. The axiom

\Diamond p \Leftrightarrow \lnot (\Box \lnot p)

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.

S4

The logic constructed above also satisfies a couple more axioms. We have

\Box p \to p

because the interior of a set is a subset of the set, and

\Box p \to \Box\Box p

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.

More logics and more topologies

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.

Trivial modal logic

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.

S5

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]

Between S4 and S5

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

p \land \Diamond\Box p \to \Box p

holds, which doesn’t hold in S4, and the formula

\Diamond p \to \Box\Diamond p

does not hold, though it must hold in S5.

Related posts

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

Modal logic and topology

Posted on by John

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

Posted on by John

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