Ever tried reading logical texts from the 20s or before (e.g., C. I. Lewis’s Symbolic Logic)? Confused by the absence of parentheses and all the dots and colons? Here’s Carnap’s explanation of the notation (from Abriss der Logistik):

4 c. The Dot Rules

The dot symbols (. : :. :: etc.) replace the bracketing of propositions. The dot signs fall into three distinct levels, depending on whether they occur

1. between two propositions in a conjunction,
2. after an operator (x), (∃ x), [(ιx)(φx)],
3. after |-, before and after the sign ⊃, ≡ ∨, |, =_Df.

Dot rules for reading: The scope of a dot symbol (for 1, to the left and to the right, for 2 to the right, for 3 to left or right, depending) extends either to the end of the proposition or to a dot symbol with more dots or to a symbol of the same or a higher level with the same number of dots.

Dot rules for writing: If the scope of a dot sybol is to extend beyond that of another, it must, if it is of a higher level than the latter, contain at least as many dots, and otherwise more dots.

Examples:

p ∨ . q . r	means	p ∨ (q . r)
|- : (p, q) : p ∨ q . ⊃ . q ∨ p	“	|- {(p, q) . [(p ∨ q) ⊃ (q ∨ p)]}
p : ∨ : q . ⊃ . q ∨ p	“	p ∨ [q ⊃ (q ∨ p)]
(x) . φx . ⊃ . p ∨ q	“	[(x) . φx] ⊃ (p ∨ q)
(x) : φx . ⊃ . p ∨ q	“	(x) . [φx ⊃ (p ∨ q)]
(x) : φx ⊃ p . ∨ q	“	(x) . [(φx ⊃ p) ∨ q]
(x) : φx ⊃ p : ∨ q	“	[(x) . (φx ⊃ p)] ∨ q

50 years ago this summer, McCarthy, Minsky, Rochester, and Shannon organized a summer conference at Dartmouth which turned out to be a milestone in Artificial Intelligence research. For the logically minded, this item in the funding proposal to the Rockefeller Foundation is perhaps most interesting:

4. Theory of the Size of a Calculation

If we are given a well-defined problem (one for which it is possible to test mechanically whether or not a proposed answer is a valid answer) one way of solving it is to try all possible answers in order. This method is inefficient, and to exclude it one must have some criterion for efficiency of calculation. Some consideration will show that to get a measure of the efficiency of a calculation it is necessary to have on hand a method of measuring the complexity of calculating devices which in turn can be done if one has a theory of the complexity of functions. Some partial results on this problem have been obtained by Shannon, and also by McCarthy.

Last week I had the pleasure of attending the Computability in Europe conference in the lovely seaside town of Swansea, Wales. Lots of interesting talks on all kinds of aspects of computation, including a number of talks on the (limits of) hypercomputation, a tutorial on proof complexity by Sam Buss, and special sessions on Gödel’s legacy for computability theory with talks by Arnon Avron, John Dawson, Andrew Hodges, and Wilfried Sieg. I won’t talk about the details–the abstracts are up on the website, the slides for many of the talks should be up very soon, and the proceedings volumes (invited, contributed [big PDF!] talks) are online as well.

Oh, and this guy stopped by to visit the building across from the conference site:

I also had an enjoyable bus ride back to Heathrow with Bob Meyer, talking about relevant logic and the epsilon calculus.