Ezra's Research

It's customary to indicate the end of a proof with a little square (a "tombstone"), with "Q.E.D.," or elsewise. These marks almost never seem helpful to me, but there are other points where significant proof obligations are discharge, and I wish these were marked.

One instance is the end of a case, in a proof by cases. Each of these is a major branch of the proof, which dead-ends in the middle. Variables may be brought into scope, which evaporate when the case is completed, so it's important to know the bounds of that case.

My contribution, then, to the technique of proof-by-cases, is to introduce the marker "huzzah!" indicating the simple end of a case as well as one's excitement at having proven something—a miminal proof-unit, perhaps. Here it is in a screenshot:

Having trouble achieving this effect yourself? Here's a TeX macro:

\def\huzzah{\hfill\emph{huzzah!}}

Update: According to Wikipedia, "Paul Sally at the University of Chicago is known for ending proofs with a pirate face symbol." This doesn't seem to be true of the couple of books coauthored by Sally that I could get through Google Books.

Posted by Ezra elias kilty Cooper at 10:43 PM | Permalink | Comments (3) | TrackBacks (0)

John Baez' enthusiasm is infectious, and his perspective appealing:

It's sort of hilarious that Ferro was solving cubic equations before negative numbers were worked out. It should serve as a lesson: we mathematicians often work on fancy stuff before understanding the basics. Often that's why math seemss hard! But often it's impossible to discover the basics except by working on fancy stuff and getting stuck.

—John Baez, This Week's Finds in Mathematical Physics, Week 261

Posted by Ezra elias kilty Cooper at 2:03 AM | Permalink | Comments (0) | TrackBacks (0)

I was surprised to find that these classic papers are available online:

• Alonzo church, "A Set of Postulates for the Foundation of Logic." 1932 (The original lambda-caculus paper.)
• Alonzo Church, "An Unsolvable Problem of Elementary Number Theory." 1936
• Moses Schönfinkel, "Ãœber die Bausteine der mathematischen Logik." 1924. (In German.)
• Nikolas de Bruijn, "Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem." 1972.
• Alonzo Church and J. B. Rosser, "Some properties of conversion." 1936.

It's interesting to read Church's papers to see how he's approaching the project. Initially, he's trying to clarify the notion of a free variable in logic, or rather to chuck it out in favor of a clear discipline for binding variables. Because he's looking at foundational issues in logic, he's at great pains to identify his assumptions.

A minor historical fact: alpha- and beta-conversion are defined in these early Church papers, but not with those names; they're identified as I-conversion and II-conversion (there is a conversion rule III, which looks like the reverse of beta-conversion).

Posted by Ezra elias kilty Cooper at 3:42 PM | Permalink | Comments (0) | TrackBacks (0)

One of the important perceptions of category theory is that an arrow x : T â†’ A in a category can be regarded as an element of A defined over T. The idea is that x is a variable element of A, meaning about the same thing as the word “quantity” in such sentences as, “The quantity x² is nonnegative”, found in older calculus books.
—Toposes, Triples and Theories, Michael Barr and Charles Wells, Version 1.1, 2002

Posted by Ezra elias kilty Cooper at 12:40 AM | Permalink | Comments (0) | TrackBacks (0)

If you want to learn about ordinal numbers, This Week's Finds in Mathematical Physics, #236, by John Baez, is a good way to start.

That's also a good article to learn about the archaeology of Euclid's writings!

Posted by Ezra elias kilty Cooper at 5:16 AM | Permalink | Comments (0) | TrackBacks (0)