This Sentence is False, or: On Natural Language, Typing and Proof

Posted on September 9, 2020
1149

The Liar’s paradox is often the first paradox someone dealing with logic, even in an informal setting, encounters. It is intuitively paradoxical: how can a sentence be both true, and false? This contradicts (ahem) the law of non-contradiction, that states that “no proposition is both true and false”, or, symbolically, ¬(A¬A)\neg (A \land \neg A). Appealing to symbols like that gives us warm fuzzy feelings, because, of course, the algebra doesn’t lie!

There’s a problem with that the appeal to symbols, though. And it’s nothing to do with non-contradiction: It’s to do with well-formedness. How do you accurately translate the “this sentence is false” sentence into a logical formula? We can try by giving it a name, say LL (for liar), and state that LL must represent some logical formula. Note that the equality symbol == here is not a member of the logic we’re using to express LL, it’s a symbol of this discourse. It’s meta​logical.

L= L = \dots

But what should fill in the dots? LL is the sentence we’re symbolising, so “this sentence” must mean LL. Saying “X is false” can be notated in a couple of equivalent ways, such as ¬X\neg X or XX \to \bot. We’ll go with the latter: it’s a surprise tool that will help us later. Now we know how to fill in the dots: It’s LL \to \bot.

Truth tables demonstrating the equivalence between ¬A\neg A and AA \to \bot, if you are classically inclined.
AA ¬A\neg A
\top \bot
\bot \top
AA AA\to\bot
\top \bot
\bot \top

But wait. If L=LL = L \to \bot, then L=(L)L = (L \to \bot) \to \bot, and also L=((L))L = ((L \to \bot) \to \bot) \to \bot, and so… forever. There is no finite, well-formed formula of first-order logic that represents the sentence “This sentence is false”, thus, assigning a truth value to it is meaningless: Saying “This sentence is false” is true is just as valid as saying that it’s false, both of those are as valid as saying “¬\neg is true”.

Wait some more, though: we’re not done. It’s known, by the Curry-Howard isomorphism, that logical systems correspond to type systems. Therefore, if we can find a type-system that assigns a meaning to our sentence LL, then there must exist a logical system that can express LL, and so, we can decide its truth!

Even better, we don’t need to analyse the truth of LL logically, we can do it type-theoretically: if we can build an inhabitant of LL, then it is true; If we can build an inhabitant of ¬L\neg L, then it’s false; And otherwise, I’m just not smart enough to do it.

So what is the smallest type system that lets us assign a meaning to LL?

A system of equirecursive types: λoh no\lambda_{\text{oh no}}1

We do not need a complex type system to express LL: a simple extension over the basic simply-typed lambda calculus λ\lambda_{\to} will suffice. No fancy higher-ranked or dependent types here, sorry!

As a refresher, the simply-typed lambda calculus has only:

Type assignment rules for the basic λ\lambda_{\to} calculus.

x:τΓΓx:τ\frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}

bBxTbΓx:b\frac{b \in \mathbb{B} \quad x \in \mathbb{T}_{b}}{\Gamma \vdash x : b}

Γ,x:σe:τΓλx.e:στ\frac{\Gamma, x : \sigma \vdash e : \tau}{\Gamma \vdash \lambda x. e : \sigma \to \tau}

Γ,e:στΓe:σΓe e:τ\frac{\Gamma, e : \sigma \to \tau \quad \Gamma \vdash e' : \sigma}{\Gamma \vdash e\ e' : \tau}

First of all, we’ll need a type to represent the logical proposition \bot. This type is empty: It has no type formers. Its elimination rule corresponds to the principle of explosion, and we write it absurd\mathtt{absurd}. The inference rule:

Γe:absurd e:A\frac{\Gamma \vdash e : \bot}{\mathtt{absurd}\ e : A}

We’re almost there. What we need now is a type former that serves as a solution for equations of the form v=...v...v = ... v .... That’s right: we’re just inventing a solution to this class of equations—maths!

These are the equirecursive types, μa.τ\mu a. \tau. The important part here is equi: these types are entirely indistinguishable from their unrollings. Formally, we extend the set of type formers with type variables aa and μ\mu-types μa.τ\mu a. \tau, where μa\mu a acts as a binder for aa.

Since we invented μ\mu types as a solution for equations of the form a=τa = \tau, we have that μa.τ=τ[μa.τ/a]\mu a. \tau = \tau[\mu a.\tau/a], where τ[σ/a]\tau[\sigma{}/a] means “substitute σ\sigma{} everywhere aa occurs in τ\tau”. The typing rules express this identity, saying that anywhere a term might have one as a type, the other works too:

Γe:τ[μa.τ/a]Γe:μa.τ\frac{\Gamma \vdash e : \tau[\mu a.\tau / a]}{\Gamma \vdash e : \mu a. \tau}

Γe:μa.τΓe:τ[μa.τ/a]\frac{\Gamma \vdash e : \mu a.\tau}{\Gamma \vdash e : \tau[\mu a. \tau / a]}

Adding these rules, along with the one for eliminating \bot, to the λ\lambda_{\to} calculus nets us the system λoh no\lambda_{\text{oh no}}. With it, one can finally formulate a representation for our LL-sentence: it’s μa.a\mu a. a \to \bot.

There exists a closed term of this type, namely λk.k k\lambda k. k\ k, which means: The “this sentence is false”-sentence is true. We can check this fact ourselves, or, more likely, use a type checker that supports equirecursive types. For example, OCaml with the -rectypes compiler option does.

We’ll first define the empty type void and the type corresponding to LL:

type void ;;
type l = ('a -> void) as 'a ;;

Now we can define our proof of LL, called yesl, and check that it has the expected type:

let yesl: l = fun k -> k k ;;

However. This same function is also a proof that… ¬L\neg L. Check it out:

let notl (x : l) : void = x x ;;

I am Bertrand Russell

Bertrand Russell (anecdotally) once proved, starting from 1=01 = 0, that he was the Pope. I am also the Pope, as it turns out, since I have on hand a proof that LL and ¬L\neg L, in violation of non-contradiction; By transitivity, I am Bertrand Russell. \blacksquare

Alright, maybe I’m not Russell (drat). But I am, however, a trickster. I tricked you! You thought that this post was going to be about a self-referential sentence, but it was actually about typed programming language design (not very shocking, I know). It’s a demonstration of how recursive types (in any form) are logically inconsistent, and of how equirecursive types are wrong.

The logical inconsistency, we all deal with, on a daily basis. It comes with Turing completeness, and it annoys me to no end every single time I accidentally do let x = ... x .... I really wish I had a practical, total functional programming language to use for my day-to-day programming, and this non-termination everywhere is a great big blotch on Haskell’s claim of purity.

The kind of recursive types you get in Haskell is fine. They’re not great if you like the propositions-as-types interpretation, since it’s trivial to derive a contradiction from them, but they’re good enough for programming that implementing a positivity checker to ensure your definitions are strictly inductive isn’t generally worth the effort.

Unless your language claims to have “zero runtime errors”, in which case, if you implement isorecursive types instead of inductive types, you are wrong. See: Elm. God damn it.

So much for “no runtime errors”… I guess spinning forever on the client side is acceptable.
-- Elm
type Void = Void Void
type Omega = Omega (Omega -> Void)

yesl : Omega
yesl = Omega (\(Omega x) -> x (Omega x))

notl : Omega -> Void
notl (Omega x) = x (Omega x)

Equirecursive types, however, are a totally different beast. They are basically useless. Sure, you might not have to write a couple of constructors, here and there… at the cost of dramatically increasing the set of incorrect programs that your type system accepts. Suddenly, typos will compile fine, and your program will just explode at runtime (more likely: fail to terminate). Isn’t this what type systems are meant to prevent?

Thankfully, very few languages implement equirecursive types. OCaml is the only one I know of, and it’s gated behind a compiler flag. However, that’s a footgun that should not be there.


  1. The reason for the name will become obvious soon enough.↩︎