* Formalizing topos-theoretic arguments in Lean
@ 2016-01-16 17:45 Todd Wilson
2016-01-19 3:36 ` Toby Bartels
0 siblings, 1 reply; 2+ messages in thread
From: Todd Wilson @ 2016-01-16 17:45 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Formalizing topos-theoretic arguments in Lean
2016-01-16 17:45 Formalizing topos-theoretic arguments in Lean Todd Wilson
@ 2016-01-19 3:36 ` Toby Bartels
0 siblings, 0 replies; 2+ messages in thread
From: Toby Bartels @ 2016-01-19 3:36 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2016-01-19 3:36 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2016-01-16 17:45 Formalizing topos-theoretic arguments in Lean Todd Wilson
2016-01-19 3:36 ` Toby Bartels
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).