An Ozone Hole in Logic

“Literature and the Real Person” source

Mr. Apollinax might have made a good escort for Lofa Polir, had she lived a hundred years ago. The titular character of a poem written circa 1915 by Thomas Eliot was based on Bertrand Russell, whose 1901 paradox revealed a gaping inconsistency in set theory as it was then known. Russell spent much of the intervening years trying to repair the gap via type theory.

Today we present a recently-discovered inconsistency in the type theory of the Scala programming language, which forced a feature-chopping revision in its new version 3.0. Then, in a worldwide exclusive, we reveal a new theorem by Polir that explains why such inconsistencies are inevitable.

Ernst Zermelo had already noticed the paradox in 1899 but brushed it off because his axiom system already evaded it. It is possible that Georg Cantor knew it in letters in 1897 to Richard Dedekind and David Hilbert. I could call this a continuation of a theme we’ve often addressed about discoveries not being named for their first discoverers, but I will not, for this reason: The discoveree was Gottlob Frege, who immediately recognized that the treatise on set theory he was about to publish had been devastated by the paradox. And the person he heard that from, in June 1902, was Russell—not any of his own compatriots.

The poem comes with an epigram from a Greek text by Lucian satirically praising the painter Zeuxis of Herakleia: “Ω τῆς καινότητος. Ἡράκλεις, τῆς παραδοξολογίας. εὐμήχανος ἄνθρωπος.” The reference translation Eliot had to hand goes: “Such novelty! Heavens, what paradoxes! How inventive he is!” I believe, however, that Eliot intended a more-particulate reading: “Oh for his innovation! Hercules, his paradoxology! Sweet machine man!” That goes better with the poem text and with aspects of Russell that were visible to Eliot at the time. We’ll only talk about the paradoxology. Russell was well aware that other monsters besides his own were lurking, like ones that emerged in the US. What if patching paradoxes is just the way of progress? Let’s see this play out in the Scala programming language.

The Inconsistency

The root of the inconsistency is allowing projection of an abstract type. Let’s explain the former concept with concrete types first. A standard way to represent trees and other graphs is by having a nested node class, for instance:


class BinaryTree[A <: Comparable[A]] {

   private var root: Node = null
   //etc.
}


A key wrinkle of Scala is that if you have two different trees T1 and T2, then T1.Node and T2.Node are separate types. This notion of path-dependent types enables the compiler to catch bugs where you might try to connect a node on one tree as a child of a node in the other tree. If there were just one BinaryTree.Node type, as is standard in Java for instance, then you could easily make this kind of bug and the compiler would not bat an eye.

If you really do want to combine nodes from two different trees, however, you can do so via code using the projection type BinaryTree#Node. The hash sign # makes this defined to be the supertype of nodes of all possible binary trees.

The [A <: Comparable[A]] part means that the tree can hold any type A of data that extends a trait called Comparable, whose function is to mandate having a comparison function for A so that the tree can be kept sorted. The symbol >: written the other way means supertype rather than subtype.

We could try to make our binary tree class more versatile by making it more abstract. By itself it could be a trait so as to allow deferred implementations. It could try to define a more general notion of Node that might relate more directly to stored data, for instance strings or numbers. This is not to say such abstractions are necessarily well-motivated, but the point is this:

• The Scala compiler defines what is workable.

• Its notion of workability is based on mathematical type theory.

• Lots of abstract constructions are made workable to encourage creativity.

Workability is not supposed to lead to type errors, however. That is the unsoundness allowed in versions 2.x of Scala.

The Code

If you have a lot of time—time to read the longest post ever on this blog—then you can draw some motivation for the unsound code. That post shows how to represent the NBG version of set theory, due to John von Neuman, Paul Bernays, and Kurt Gödel, as an infinite graph. At the top of the graph are nodes representing the class of all sets and various other expansive types, which are symbolized by V in the post. At the bottom is a node for the null set identified with O. We can think of them as representing “zones” for possible supertypes and subtypes of some types of interest, such as string and number.

Aside from some abstract manipulation of types, the following code does nothing except compose two versions of the identity function, applied to a String. As you are welcome to try yourself, it compiles in Scala 2.x. But before you try to run it, you can ask yourself: exactly what number would the string “Hello World!” become?


/** File "Unsound.scala", mod by KWR from the last example in
https://lptk.github.io/programming/2019/09/13/type-projection.html
*/
object Unsound extends App {

   println(hole("Hello World!"))
}


The point remains, however, that this program is accepted as a “theorem” in the logical theory underlying the Scala 2.x type system. That theory is thereby unsound.

Lofa Polir’s Theorem

A point we have been at pains to make is that this kind of happening is far from rare. Systems are proven secure and then break all the time. Creating more ways to write correct programs has created new ways to have bugs, even as the frequency of old kinds of bugs is reduced. As with the Earth’s ozone hole, the situation is not worsening but the problem persists.

Dr. Polir’s new theorem not only explains why but also argues that we should be neither surprised nor dismayed by this state of affairs. It can be given the following intuitive statement:

Theorem 1 There is a sound theory A.F. that can be represented as a complexity-bounded limit of inconsistent theories, but not as an effective limit of consistent theories.

The soundness is with respect to the standard model of arithmetic and includes every statement of arithmetic proved in set theory. The clever new idea in her proof is the manner of the proof itself: it formalizes and self-applies a criterion of feasible correctness in the limit for a sequence of incorrect proofs.

The upshot is the following:

The most productive and feasible way to do mathematics is to design inconsistent theories and fix them incrementally, rather than to demand global correctness from the get-go.

Before Dr. Polir types up her paper, she has a request for readers of this blog: What should the initials A.F. of her theory stand for? The name “Arithmetical Foundations” is both hackneyed and taken.

Open Problems

What do you think Lofa’s A.F. stands for?

[hand-fixing of content after posting while still April 1, added paragraph to intro, changed image at top]