From: Todd Wilson <twilson@csufresno.edu>
To: categories@mta.ca
Subject: Formalizing topos-theoretic arguments in Lean
Date: Sat, 16 Jan 2016 09:45:58 -0800 [thread overview]
Message-ID: <E1aKq0X-0003Pv-0e@mlist.mta.ca> (raw)
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/ ]
next reply other threads:[~2016-01-16 17:45 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-01-16 17:45 Todd Wilson [this message]
2016-01-19 3:36 ` Toby Bartels
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=E1aKq0X-0003Pv-0e@mlist.mta.ca \
--to=twilson@csufresno.edu \
--cc=categories@mta.ca \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
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).