Formalizing topos-theoretic arguments in Lean

Formalizing topos-theoretic arguments in Lean

[Todd Wilson]

For those interested in formalizing internal topos-theoretic arguments
in a proof assistant, I'd like to make a plug for a newer entry on the
usual list of provers, namely the Lean Theorem Prover [1]. In Lean, Prop
is impredicative and extensional, and so it functions much like a
subobject classifier, allowing a direct encoding of topos-theoretic
arguments.

As an example, you can look at my formalization [2] of the results from
my paper

    J. Todd Wilson, "An Intuitionistic version of Zermelo's proof that
    every choice set can be well-ordered", J. Symbolic Logic, 66:3
    (2001), 1121-1126.

    Abstract: We give a proof, valid in any elementary topos, of the
    theorem of Zermelo that any set possessing a choice function for its
    set of inhabited subsets can be well-ordered. Our proof is
    considerably simpler than existing proofs in the literature and
    moreover can be seen as a direct generalization of Zermelo's own 1908
    proof of his theorem.

This "elementary" proof, besides being a direct generalization of
Zermelo's, makes crucial use of both impredicativity and extensionality
of the subobject classifier, and so is a good illustration of these
features of Lean when it comes to doing such formalizations. (The
"existing proofs in the literature" mentioned in the abstract referred
to proofs of Freyd and Axel.)

Also, if I can be permitted an additional self-plug, this proof does not
appear to be well-known, since there is no reference to it in Section
D4.5 of Johnstone's Elephant book or, for example, in the article on the
well-ordering theorem in the nLab [3].

[1] https://leanprover.github.io/
[2] https://github.com/lambdacalculator/lean-choice
[3] https://ncatlab.org/nlab/show/well-ordering+theorem

-- 
Todd Wilson                               A smile is not an individual
Computer Science Department               product; it is a co-product.
California State University, Fresno                 -- Thich Nhat Hanh



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Formalizing topos-theoretic arguments in Lean

[Toby Bartels]

Todd Wilson wrote in part:

>this proof does not appear to be well-known, since there is no reference 
>to it in Section D4.5 of Johnstone's Elephant book or, for example, in 
>the article on the well-ordering theorem in the nLab

It's mentioned there now, since I just added your paper and formalization 
to the reference list.

But it's rare for the nLab to have a comprehensive list of references. 
This article, for example, despite being begun in 2009, had only Zermelo's 
original 1904 paper until Thomas Holder added more last year (in 2015).


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]