On the Papacy of Bertrand Russell
Table of Contents
Abstract. I present several Pie formalizations of the claim:
1 = 0 implies I am the Pope.
Some formalizations capture Bertrand Russell's original argument with high fidelity, and others are quite different (and in some regards simpler). The goal is to highlight the implicit assumptions of the various proofs, in particular with respect to explicit invocations of the principle of explosion. This piece is based on an email conversation with Stuart Kurtz and Ben Caldwell, who I consider to be co-authors but without the responsibility of answering for my mistakes or agreeing with my opinions.
Bertrand Russull is said to have proved that he was the Pope given that 1 = 0 in order to demonstrate the principle of explosion a.k.a. ex falso quodlibet.1 This principle states that any proposition follows from a contradiction. The argument in it's currently most cited form goes:
Add 1 to both sides of the equation: then we have 2 = 1. The set containing just me and the Pope has 2 members. But 2 = 1, so it has only 1 member; therefore, I am the Pope.
It's a clever argument, but is often presented aphoristically, leaving just enough room for a chuckle, but not enough for rigorous analysis. The purpose of this piece is to make some room.
Take, for example, this argument:
1 = 0 contradicts the fact that 1 ≠ 0. By the principle of explosion, I am the Pope.
It clearly lacks the disarming wit of the Russell's argument and is unlikely to persuade an individual who doubts the principle in the first place, but it does beg the question: what did Russell accomplish with his argument over this one? He avoids referring to the principle of explosion directly, but to what end? Is he making a claim about paraconsistent or minimal logic? Is he attempting to demonstrate the naturalness of the principle (perhaps by obfuscating its use)?2
In order to analyze this simple theorem to death, I'll consider several formalizations of it in Pie, a dependently typed programming language created for the book The Little Typer (which I recommend to anyone interested in learning about dependent type theory). The motivation for this is threefold.
- The Little Typer is used at UChicago by Stuart Kurtz in his course on type theory, and I'd like this piece to be approachable to anyone who's taken the course (and is willing to do a bit of keyboard head-banging).
- Pie is very explicit. This makes it easier (for me) to ensure I haven't done anything sneaky.3
- I like it.
Disclaimer: This is not a tutorial on dependent type theory or Pie. I realize this severely limits the scope of this piece, but also I don't really care (sorry). That said, please read The Little Typer! It's great!
Absurdity
The principle of explosion appears in Pie as ind-Absurd, the
induction principle for Absurd (i.e., the empty type). We can use
this to formalize the second, less witty argument above given a proof
that 1 is, in fact, not equal to 0.4 In what follows, I use atoms to represent me
and the Pope.5 Also
note the standard encoding of negation as implication of absurdity.
# lang pie (claim Not (-> U U)) (define Not (lambda (A) (-> A Absurd))) (claim <> (Pi ((A U)) (-> A A U))) (define <> (lambda (A x y) (Not (= A x y)))) (claim 1<>0 (<> Nat 1 0)) (define 1<>0 (lambda (1=0) (replace ; target 1=0 ; motive (lambda (n) (which-Nat ; target n ; base Absurd ; step (lambda (_) Trivial))) ; base sole))) (claim 1=0-implies-i-am-the-pope-0 (-> (= Nat 1 0) (= Atom 'me 'pope))) (define 1=0-implies-i-am-the-pope-0 (lambda (1=0) (ind-Absurd ; target (1<>0 1=0) ; motive (= Atom 'me 'pope))))
There's nothing wrong with this proof mathematically speaking; the
principle of explosion is an axiom in most standard logical
systems.6
But it's not the proof that Russell gave. He chooses to bring in some
pretty heavy artillery: sets.7 We'll come
back to this. But before formalizing Russell's argument, an interlude
on what I believe is the simplest papacy proof that doesn't use
ind-Absurd.
Congruence
One crucial feature of natural numbers that they have a distinguished
element: 0. This number is more than just distinguished (it's the
smallest with respect to the standard ordering, it's an additive
identity and a multiplicative annihilator) but at the moment it's
distinguished status is all we need. We can easily determine if any
number is or is not 0. In Pie, this is witnessed by a simplified
recursor (already featured above) called which-Nat, with which we
can make values (and types!) that depend on whether or not a given
number is 0.
Consider this simple (though still less clever) papacy proof:
Suppose we give the Pope a sticker with the number 0 on it, and give all other persons a sticker with the number 1 on it. It follows that if a person has a 0 sticker, then they are the Pope. Since 1 = 0, I have a 0 sticker, so I am the Pope.
In fact, everyone is the pope (that's kind of the point). This
argument can be formalized in Pie with cong, which allows us to
prove f(x) = f(y) given x = y.
(claim 1=0-implies-i-am-the-pope-1 (-> (= Nat 1 0) (= Atom 'me 'pope))) (define 1=0-implies-i-am-the-pope-1 (lambda (1=0) (cong ; target 1=0 ; fun (the (-> Nat Atom) (lambda (n) (which-Nat ; target n ; base 'pope ; step (lambda (_) 'me)))))))
And no use of ind-Absurd, so the principle of explosion isn't
necessary to prove Russell's papacy. But this proof might have you
thinking: if all we're doing is applying a function to each side of
the equation 1 = 0 (in essence replacing 1 with me and 0 with the
Pope) what's to stop us from making any two things equal? Answer:
nothing!
(claim 1=0-implies-any-equality
(Pi ((A U)
(x A)
(y A))
(-> (= Nat 1 0) (= A x y))))
(define 1=0-implies-any-equality
(lambda (A x y 1=0)
(cong
; target
1=0
; fun
(the (-> Nat A)
(lambda (n)
(which-Nat
; target
n
; base
y
; step
(lambda (_) x)))))))
(claim 1=0-implies-i-am-the-pope-2
(-> (= Nat 1 0) (= Atom 'me 'pope)))
(define 1=0-implies-i-am-the-pope-2
(lambda (1=0)
(1=0-implies-any-equality Atom 'me 'pope 1=0)))
But wait, there's more! With a little more finesse we can derive
anything from 1 = 0. Rather than using congruence, we can use
replace, which for any predicate8 P and
equality x = y, allows us to prove P(x) and conclude P(y).
Because 0 is a distinguished number, we can design a predicate P such
that P(1) easy to prove (e.g., Trivial) and P(0) is anything we
want.
(claim explode-1=0 (Pi ((A U)) (-> (= Nat 1 0) A))) (define explode-1=0 (lambda (A 1=0) (replace ; target 1=0 ; motive (lambda (a) (which-Nat ; target a ; base A ; step (lambda (_) Trivial))) ; base sole))) (claim 1=0-implies-i-am-the-pope-3 (-> (= Nat 1 0) (= Atom 'me 'pope))) (define 1=0-implies-i-am-the-pope-3 (explode-1=0 (= Atom 'me 'pope)))
In other words, the claim 1 = 0 is explosive. In fact, we could
define Absurd using the type (= Nat 0 1), i.e., we could do away
with Absurd altogether and used (= Nat 0 1) instead.9
Explosives
The first thing to observe is just how lucky Russell was in the choice of contradiction from which he needed to prove his papacy. It just so happens that 1 = 0 is explosive in the sense above. This gave him a fair amount power to come up with a proof. We can even re-imagine Russell's argument as a sort of magic trick:
Here I have here an ordinary sheet of paper. On one side I've written the number 1, and on the other the number 0. May I have a volunteer write a proposition on the side with 0?
Ah, "Bertrand Russell is the Pope", very good.
I will now, before your very eyes, prove to you that I am the Pope assuming that 1 = 0. I begin by writing on my sheet of paper, the side with the number 1: "My name is Bertrand Russell." We all accept this to be true, yes? Then it is certainly the case that the side with 1 has written on it a true fact, yes? Very good. Now, suppose 1 = 0. Then you must confess that the side with 0 has written on it a true fact! For, 1 or 0, what difference does it make if they are equal? But that true fact is … Presto! I am the Pope!
In the presence of the principle of explosion, everything provably
false is explosive, and this can be witnessed within Pie (without
using ind-Absurd). In fact, that everything provably false is
explosive is equivalent to the principle of explosion.
(claim ind-absurd-implies-explode
(-> (Pi ((A U)) (-> Absurd A))
(Pi ((A U)) (-> (Not A) (Pi ((B U)) (-> A B))))))
(define ind-absurd-implies-explode
(lambda (ind-absurd A not-a B a)
(ind-absurd B (not-a a))))
(claim explode-implies-ind-absurd
(-> (Pi ((A U)) (-> (Not A) (Pi ((B U)) (-> A B))))
(Pi ((A U)) (-> Absurd A))))
(define explode-implies-ind-absurd
(lambda (explode A)
(explode Absurd (lambda (x) x) A)))
But what we're saying about 1 = 0 is stronger than this: let's say
that a type A is truly explosive if we can derive anything from
A without ind-Absurd. Any equality between unequal natural
numbers is truly explosive. So is (Pi ((A U)) A) (which expresses
that everything is true).
There are also many claims which are provably false and not truly
explosive, e.g., Pair Absurd Absurd and Either Absurd (= Nat 13
5). Also, just Absurd. Imagine if Russell's interlocutor in the
original story had said:
You're telling me that anything follows from a contradiction? Well then, prove that you're the Pope from the false proposition!
I'm sure Russull would come up with a more intelligent response than I could, but he couldn't succeed in proving his papacy without appealing to the principle of explosion.10
Intermission
Let's take stock. What was Russell supposed to accomplish with his argument? I've presented things up to now as though our imagined interlocutor doubted the principle of explosion. We've shown that we can use a form of explosion to prove Russell's papacy without appealing to the principle proper.
But perhaps our imagined interlocutor was just challenging the
naturalness of the principle. Maybe they didn't doubt the principle
per se but wanted a demonstration of its use in "normal" discourse.
In this sense, the use of explode-1=0 is also likely to be not all
too satisfying; it has the feeling of a magic trick. And the
congruence proof has an equality-twiddling flavor which is
mathematically acceptable, but not necessarily intuitive.
In what remains, we look at a few formalization which are closer to Russell's argument, and hence more natural. I believe the first one (using vectors) is the "correct" one, but it depends on a loose interpretation of Russell's meaning of "set."
Vectors
We begin by putting me and the Pope into a 2-element vector:
(claim me-and-the-pope-Vec (Vec Atom 2)) (define me-and-the-pope-Vec (vec:: 'me (vec:: 'pope vecnil)))
We'd like to argue that if we extract 2 elements from a 1-element vector then they're the same element. But in order to identify me and the Pope, it must be that if we extract 2 elements in the same way from a 2-element vector, then they're different.
We already have one way of extracting an element from a vector: head
grabs the first one. We need another way of extracting an element
which gives the head element of a singleton, and a non-head element of
a 2-element vector. So we define a next function, which grabs the
second element of a vector, if it exists, and otherwise, falls back
to the head. This will be more convenient if we pre-destruct the
given vector; in other words, we're really defining a head function
with a default value for the empty case.
(claim next
(Pi ((A U)
(n Nat))
(-> A (Vec A n) A)))
(define next
(lambda (A n a v)
(ind-Vec
; target-1
n
; target-2
v
; motive
(lambda (_ _) A)
; base
a
; step
(lambda (_ a _ _) a))))
We then show that if the tail of our vector is empty (i.e., the vector is a singleton), then the head element is the same as the next element. We express the emptiness of the tail in terms of its length because this will make using the hypothesis 1 = 0 easier.
(claim empty-tail-implies-head=next
(Pi ((A U)
(n Nat)
(n=0 (= Nat n 0))
(v (Vec A (add1 n))))
(= A
(head v)
(next A n (head v) (tail v)))))
(define empty-tail-implies-head=next
(lambda (A n n=0)
(replace
; target
(symm n=0)
; motive
(lambda (k)
(Pi ((v (Vec A (add1 k))))
(= A (head v) (next A k (head v) (tail v)))))
; base
(lambda (v)
(replace
; target
(the (= (Vec A 0) vecnil (tail v)) (same vecnil))
; motive
(lambda (a) (= A (head v) (next A 0 (head v) a)))
; base
(same (head v)))))))
And so if 1 = 0, me-and-the-pope is a 1-element vector, and the
head element ('me) is the same as the next element ('pope).
(claim 1=0-implies-i-am-the-pope-4
(-> (= Nat 1 0) (= Atom 'me 'pope)))
(define 1=0-implies-i-am-the-pope-4
(lambda (1=0)
(empty-tail-implies-head=next
Atom
1
1=0
me-and-the-pope-Vec)))
Presto! (just kidding) I believe this proof captures the spirit of Russell's argument while remaining simple. And it doesn't appeal to the principle of explosion, just our ability to fool our type system into thinking that a 2-element vector only has 1 element. It's only real knock is that it doesn't use to any set-theoretic language (and this isn't a true knock in my opinion). Also, and this super nitpicky, it doesn't use the "add 1 to both sides" part of the argument.
But we're not here to stop at a reasonable stopping point, we're here
to overdo things. So let's suppose we do want to use set-theoretic
language (and add 1 to both sides). The first thing we'll have to
figure out is how to talk about membership. It's not possible to
define a membership predicate for vectors directly because of the
(somewhat surprising) absence of a rec-Vec recursor.11
But there is rec-List!
Lists
Round 2: we begin by putting me and the pope into a 2-element list:
(claim me-and-the-pope-List (List Atom)) (define me-and-the-pope-List (:: 'me (:: 'pope nil)))
Lists don't keep track of their own length, so we'll need to define a
length function, mostly so that we can determine if a list is a
singleton.
(claim length
(Pi ((A U))
(-> (List A) Nat)))
(define length
(lambda (A l)
(rec-List
; target
l
; base
0
; step
(lambda (_ _ length-tail)
(add1 length-tail)))))
We can use rec-List to recursively define a membership predicate on
lists. This predicate says (albeit more verbosely in the Pie version):
- x ∉ []
- x ∈ (y ∷ ys) if x = y or x ∈ ys
(claim Elem-List
(Pi ((A U)
(x A)
(l (List A)))
U))
(define Elem-List
(lambda (A x l)
((rec-List
; target
l
; base
(the (-> A U) (lambda (_) Absurd))
; step
(lambda (x xs elem-xs)
(lambda (y)
(Either
(= A x y)
(elem-xs y)))))
x)))
Now, the kicker: we can prove a natural looking lemma which says that any 2 elements of a singleton list are the same. The proof is hairy, so I won't go into the details, but it goes as you would expect:
if x ∈ [a] and y ∈ [a] then x = a and y = a, so x = y.
(claim singleton-has-unique-element-List
(Pi ((A U)
(x A)
(y A)
(l (List A)))
(-> (= Nat (length A l) 1)
(Elem-List A x l)
(Elem-List A y l)
(= A x y))))
(define singleton-has-unique-element-List
(lambda (A x y l)
(ind-List
; target
l
; motive
(lambda (l)
(-> (= Nat (length A l) 1)
(Elem-List A x l)
(Elem-List A y l)
(= A x y)))
; base
(lambda (0=1)
(explode-1=0
(-> Absurd
Absurd
(= A x y))
(symm 0=1)))
; step
(lambda (a as almost)
(ind-List
; target
as
; motive
(lambda (l)
(-> (= Nat (length A (:: a l)) 1)
(Elem-List A x (:: a l))
(Elem-List A y (:: a l))
(= A x y)))
; base
(lambda (_ x-in-a y-in-a)
(ind-Either
; target
x-in-a
; motive
(lambda (_) (= A x y))
; on-left
(lambda (a=x)
(ind-Either
; target
y-in-a
; motive
(lambda (_) (= A x y))
; on-left
(lambda (a=y)
(trans
(symm a=x)
a=y))
; on-right
(lambda (false)
(ind-Absurd
; target
false
; motive
(= A x y)))))
(lambda (false)
(ind-Absurd
; target
false
; motive
(= A x y)))))
; step
(lambda (b bs _ SSk=1)
(explode-1=0
(-> (Elem-List A x (:: a (:: b bs)))
(Elem-List A y (:: a (:: b bs)))
(= A x y))
(cong
; target
SSk=1
; fun
(the (-> Nat Nat)
(lambda (n)
(which-Nat
; target
n
; base
0
; step
(lambda (n-1)
(which-Nat
; target
n-1
; base
0
; target
(lambda (_) 1))))))))))))))
Those of you keeping score at home may have noticed: we snuck in a
couple uses of ind-Absurd! According to the somewhat artificial
rules of the game we're playing, this is necessary. We can
demonstrate this formally by deriving the principle of explosion from
the above lemma without using ind-Absurd. This works by applying
our lemma to [1], using our false assumption to prove that 0 ∈ [1],
and then exploding the resulting prove of 1 = 0.
(claim singleton-has-unique-element-List-implies-ind-absurd
(-> (Pi ((A U)
(x A)
(y A)
(l (List A)))
(-> (= Nat (length A l) 1)
(Elem-List A x l)
(Elem-List A y l)
(= A x y)))
(Pi ((A U)) (-> Absurd A))))
(define singleton-has-unique-element-List-implies-ind-absurd
(lambda (prf A absurd)
(explode-1=0
A
(prf
Nat
1
0
(:: 1 nil)
(same 1)
(left (same 1))
(right absurd)))))
Okay, fine.12 But we do get this nice papacy proof:
(claim 1=0-implies-i-am-the-pope-5 (-> (= Nat 1 0) (= Atom 'me 'pope))) (define 1=0-implies-i-am-the-pope-5 (lambda (1=0) (singleton-has-unique-element-List Atom 'me 'pope me-and-the-pope-List (cong ; target 1=0 ; fun (the (-> Nat Nat) (lambda (n) (add1 n)))) (left (same 'me)) ; 'me is in the list (right (left (same 'pope)))))) ; 'pope is in the list
And look! The "add 1 to both sides" part is there!
Finite Sets
What remains is an exercise in taking things too far. What we've done above is all fine and good, but the maximalist in me wants to say: but what about actual sets? So without further ado, a version of Russell's argument using an encoding of finite sets in Pie.13 I won't dwell on the details, it's for the most part ugly. But, to loosely quote Barendregt: "the attentive reader that has worked through the proofs in this [piece] may experience a free association of the whirling details."
The first step is to define an encoding of finite sets. We use a
pretty standard one: an n-element finite set is a n-stack of Sigma
types that keep track of an element and a proof that it's not equal to
any of the other elements in the set. We have to define the set type
and it's membership predicate simultaneously, and then extract each
part a posteriori. Note one important feature of this encoding that
will come back later: it depends on equality.
(claim FiniteSetAndElem
(Pi ((A U)
(n Nat))
(Sigma ((B U)) (-> A B U))))
(define FiniteSetAndElem
(lambda (A n)
(rec-Nat
; target
n
; base
(the (Sigma ((B U)) (-> A B U))
(cons Trivial (lambda (x empty) Absurd)))
; step
(lambda (n-1 set-and-elem)
(cons
(Sigma ((y A)
(set (car set-and-elem)))
(-> ((cdr set-and-elem) y set) Absurd))
(lambda (x set)
(Either
(= A x (car set))
((cdr set-and-elem) x (car (cdr set))))))))))
(claim FiniteSet (-> U Nat U))
(define FiniteSet (lambda (A n) (car (FiniteSetAndElem A n))))
(claim Elem-FiniteSet
(Pi ((A U)
(n Nat))
(-> A (FiniteSet A n) U)))
(define Elem-FiniteSet (lambda (A n) (cdr (FiniteSetAndElem A n))))
Next we write a little interface for constructing small sets. Again, note that constructing a 2-element set requires that the 2 elements are not equal.
(claim empty (Pi ((A U)) (FiniteSet A 0))) (define empty (lambda (A) sole)) (claim singleton (Pi ((A U) (x A)) (FiniteSet A 1))) (define singleton (lambda (A x) (cons x (cons sole (lambda (x) x))))) (claim pair (Pi ((A U) (x A) (y A) (x<>y (-> (= A x y) Absurd))) (FiniteSet A 2))) (define pair (lambda (A x y x<>y) (cons x (cons (singleton A y) (lambda (x=y-or-false) (ind-Either ; target x=y-or-false ; motive (lambda (_) Absurd) ; on-left (lambda (x=y) (x<>y x=y)) ; on-right (lambda (false) false)))))))
Let's take a look again at the language of the argument: "the set containing me and the Pope has 2 members." How do we know this? The only way to be sure is if we already know I'm not the Pope. We don't know this either, but if I'm the Pope, there's nothing to prove. The point: there's a hidden non-constructive assumption in Russell's argument. Or rather, Russell is assuming something perhaps non-obvious: that people admit decidable equality.14
Now for the key lemma:
if x ∈ S and y ∈ S and |S| = 1, then x = y.
The proof is similar to that of the analogous lemma for lists.
(claim singleton-has-unique-element-FiniteSet
(Pi ((A U)
(n Nat)
(x A)
(y A)
(s (FiniteSet A n)))
(-> (= Nat n 1)
(Elem-FiniteSet A n x s)
(Elem-FiniteSet A n y s)
(= A x y))))
(define singleton-has-unique-element-FiniteSet
(lambda (A n x y)
(ind-Nat
; target
n
; motive
(lambda (k)
(Pi ((s (FiniteSet A k)))
(-> (= Nat k 1)
(Elem-FiniteSet A k x s)
(Elem-FiniteSet A k y s)
(= A x y))))
; base
(lambda (_ 0=1 _ _)
(cong
; target
0=1
; fun
(the (-> Nat A)
(lambda (m)
(which-Nat
; target
m
; base
x
; step
(lambda (_) y))))))
; step
(lambda (n-1 _)
(ind-Nat
; target
n-1
; motive
(lambda (k)
(Pi ((s (FiniteSet A (add1 k))))
(-> (= Nat (add1 k) 1)
(Elem-FiniteSet A (add1 k) x s)
(Elem-FiniteSet A (add1 k) y s)
(= A x y))))
; base
(lambda (s _ x-in-s y-in-s)
(ind-Either
; target
x-in-s
; motive
(lambda (_) (= A x y))
; on-left
(lambda (x=r)
(ind-Either
; target
y-in-s
; motive
(lambda (_) (= A x y))
; on-left
(lambda (y=r) (trans x=r (symm y=r)))
; on-right
(lambda (false)
(ind-Absurd
; target
false
; motive
(= A x y)))))
; on-right
(lambda (false)
(ind-Absurd
; target
false
; motive
(= A x y)))))
; step
(lambda (n-2 _)
(lambda (_ SSk=1 _ _)
(cong
; target
SSk=1
; fun
(the (-> Nat A)
(lambda (m)
(which-Nat
; target
m
; base
x
; step
(lambda (m-1)
(which-Nat
; target
m-1
; base
y
; step
(lambda (_) x))))))))))))))
As in the list proof, we have to use ind-Absurd, but at this point
we've given up on that battle. Maybe what Russell accomplished was
not giving an argument independent of ind-Absurd, but rather giving
one so obfuscatory in it's use of ind-Absurd that it's somehow more
natural than many of the proofs that avoid it.
Finally addressing the aforementioned elephant: we can't construct the set containing just me and the Pope without already knowing that I am not the Pope. Note that we didn't have to deal with this for vectors and lists because there's nothing stopping me from create a list containing me and myself, or the pope and the pope. If we assume I'm not the Pope then the proof goes through.
(claim 1=0-implies-i-am-the-pope-kind-of (-> (<> Atom 'me 'pope) (= Nat 1 0) (= Atom 'me 'pope))) (define 1=0-implies-i-am-the-pope-kind-of (lambda (me<>pope 1=0) (singleton-has-unique-element-FiniteSet Atom 2 'me 'pope (pair Atom 'me 'pope me<>pope) (cong ; target 1=0 ; fun (the (-> Nat Nat) (lambda (k) (add1 k)))) (left (same 'me)) ; 'me is in the set (right (left (same 'pope)))))) ; 'pope is in the set
As a skeptic of intuitionism, Russell likely wouldn't consider this a legitimate roadblock. If we accept the law of excluded middle, we can work with the premise that either I am or am not the Pope, and the proof goes through as expected, though the trivial branch of the disjunction is elided in the original argument. We conclude with a simple generalization of the above result, which demonstrates that this argument works for equating any two values of a type which admits decidable equality.
(claim Dec-= (-> U U)) (define Dec-= (lambda (A) (Pi ((x A) (y A)) (Either (= A x y) (<> A x y))))) (claim 1=0-implies-x=y-given-dec-= (Pi ((A U) (x A) (y A)) (-> (Dec-= A) (= Nat 1 0) (= A x y)))) (define 1=0-implies-x=y-given-dec-= (lambda (A x y dec-= 1=0) (ind-Either ; target (dec-= x y) ; motive (lambda (_) (= A x y)) ; on-left (lambda (x=y) x=y) ; on-right (lambda (x<>y) (singleton-has-unique-element-FiniteSet A 2 x y (pair A x y x<>y) (cong ; target 1=0 ; fun (the (-> Nat Nat) (lambda (k) (add1 k)))) (left (same x)) (right (left (same y)))))))) (claim 1=0-implies-i-am-the-pope-classical (-> (Pi ((A U)) (Either A (Not A))) (= Nat 1 0) (= Atom 'me 'pope))) (define 1=0-implies-i-am-the-pope-classical (lambda (lem 1=0) (1=0-implies-x=y-given-dec-= Atom 'me 'pope (lambda (x y) (lem (= Atom x y))) 1=0)))
So if you're a staunch intuitionist who believes that people admit decidable equality, then rest assured you can still carry out Russell's argument in this contrived form, but you're gonna need the principle of explosion (and doesn't this beg the question)?
June 16, 2025
Footnotes:
The exact source of this story seems to be lost. An old reddit post claims it's in the introduction to the second edition of Russell's Principles of Mathematics, but unless I have a false copy, this is not the case.
It goes without saying (but I'll say it anyway) that he's doing none of these things, it's just a quip.
Dependent pattern matching and implicit arguments are beautiful features, but using them sometimes feels like a riding finely-tuned motorcycle (not that I'd actually know, but I think the analogy stands). Pie is the steel frame bike you had in college, clunky and simple and gets the job done.
A version of 1<>0 is given
in The Little Typer.
It's fair to question this choice. That said, using
atoms has some nice properties. For one, it allows me to avoid
postulating a Person type. It would have also been possible to use
a different type as a proxy for Person, e.g. Nat, but Atom is
nice because it doesn't admit decidable equality, so using it makes
fewer philosophical assumptions about the nature of personhood.
That is, excluding paraconsistent and minimal systems.
To call this heavy artillery is somewhat anachronistic. At the time, set theory was a fairly lightweight mathematical foundations, and it would be several decades before we feel comfortable leaving the "paradise" of set theory (to quote Hilbert) and spend more time in the "playgrounds" of weaker foundational systems (to quote Shore). It's also a bit unfair: set theory is only heavy if you're not already doing set theory, e.g., if you're doing type theory. But no matter, we forge ahead.
Note that Pie uses the term motive for a predicate used in an induction principle.
This is a standard fact of constructive mathematics. See, e.g., Proposition 3.2 of Constructivism in Mathematics by Troelstra and van Dalen. I most recently came across this argument in a comment by Marc Hermes on a blog post by Lawrence C. Paulson on the same topic as this one.
There's much more to say about
this. For example, it's outside the scope of this piece to prove that
the principle of explosion isn't a theorem in Pie without
ind-Absurd. There are also some interesting semi-classical
principles that arise from looking more carefully at the notion of
explosion. I may come back to these questions in another piece.
This isn't
a limitation of dependent type theory in general, just a limitation of
Pie: it doesn't have a universe hierarchy. Without a recursor (as
opposed to an inductor) we'd get the dreaded "U is a type, but it does
not have a type" error when defining the motive (lambda (_ _) U).
This is where things get a bit finicky. Technically
we can prove everything in this section without ind-Absurd but
we'd have to use something explosive like (= Nat 1 0) in place of
Absurd in Elem-List. But this is cheating. We could make the
nature of this cheating more formal, but I'm satisfied with simply
stipulating that, in this game we're playing, we're not allowed to
replace Absurd in predicates we define.
When I was a TA for Stu's type theory course I made it a tradition to do at least one over-the-top proof in Pie each quarter. I'd like to think this proof continues the tradition.