January 16, 2011

For a bit of light bedtime reading, I'm going through Raymond Smullyan's book First-Order Logic. It's a proper math book, not one of his popular fantasias like The Lady or the Tiger, and it was first published in 1968.

One of the things that strikes me is how mired in mechanics it is. He defines propositional formulae, as you might expect, as formed from variables, negations, and parenthesized binary connectives, and then he is at pains to point out that every proposition uniquely decomposes as either a variable, a negation, or a parenthesized binary connective. He cites proofs from Church and Kleene.

I spent ages going back and forth trying to decide what the difference between the definition and the lemma was, or to see what the supposed proof obligation was here.

Finally it dawned on me that he sees his formulae as essentially strings of symbols, rather than terms per se, and so the "uniqueness of decomposition" was essentially saying that there is a unique way to parse these symbol-strings as terms. To my modern eyes, it never occurred to me that the definition itself would be interpreted as anything but a definition about terms, or trees.

He goes on to note that, whereas his definition provided for connectives formed as, for example, (X /\ Y), they could have been defined as (X) /\ (Y). Three pages are spent on all this fuss over parentheses, and the equivalence between their different placements! When I didn't even see the parentheses as objects in the first place—they were just notation. How times have changed, for the better.

April 3, 2008

Huzzah

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.

March 21, 2008

Fancy math, basics

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

January 14, 2008

Classics

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

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).

September 11, 2007

Elements

I quite like this:
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 x2 is nonnegativeâ€, found in older calculus books.
â€”Toposes, Triples and Theories, Michael Barr and Charles Wells, Version 1.1, 2002

July 28, 2006

Ordinal Numbers Intro

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!