Currently on the East Line towards Edinburgh. I'm heading back from the
CAMELEON logic event in Cambridge. Although the time-spent-on-train/time-spent-in-lectures ratio is abysmal, I've enjoyed it enormously. I was forced to miss the last sessions this morning due to the train schedule, but so far it's been quality stuff. It's not often you see the kind of chalk'n'talk performance that we saw with
Thomas Forster the other day (on countable ordinals). How convenient then that the Centre for Mathematical Studies is equipped with proper blackboards.
Yet, nostalgia notwithstanding, the performance award still goes to
Peter Smith with his Steve Jobs like iGödel talks. In other words, how to make Gödel touch-pad user-friendly in three short lectures. One important moral is that Gödel's theorems are being done a disfavour by the standard manner of presentation (no names mentioned). Instead of mixing the general proof of the 1st Theorem with proofs of its applications to interesting systems, we're given an all-purpose formulation which is brief and transparent. The idea is to show that the result holds for so-called
nice theories: A theory
T is
nice iff it's p.r. adequate, p.r. formalized, and contains first-order logic. The boring job, then, is to show that some interesting theory, say
PA, is in fact nice.
The philosopher's among us also probably felt the sting of Peter Smith's next insight. A typical gloss on the 1st theorem (I suspect particularly among philosophers) is that Gödel sentences are
true since they say about themselves that they are unprovable, and
are unprovable. However, there are nice theories with false Gödel sentences. The point is roughly that the diagonalization function,
Diag for some theory
T, can be captured by an artificial wff
Diag(x, y) ∧
Θ, where
Diag(x, y) captures
Diag and Θ is a
T-theorem. Letting Θ be a theorem that is indeed false (
T is unsound), we can construct a Gödel sentence that is false since the Θ-conjunct is false. (See
Peter Smith's book on Gödel ch. 16.8 for details.)
Wilfred Hodges took us on one of his tours de force through the history of logic. Modern logic, says he, arrived too late. Why, we ask. Because the traditionalist logicians never managed to formalise the idea of reasoning under assumption! (What a treat for a proof-theorist.) Hodges asks the question: How come traditionalist logicians thought their formalisations were complete, yet they lacked the means to formalise the reasoning in Euclid's geometry - a pinnacle of mathematical thought? The answer, according to Hodges, is (at least partly) that the Aristotelian tradition - the ancients, the Scholastics and the early moderns - all attempted to formalise inferences with
antecedents (of conditionals) instead of proper
assumptions of inferences. As a result, Hodges suggests, their schematic systems were restricted to
local formalisation, as opposed to
global formalization where a single inference step doesn't need to be self-sufficient (think natural deduction).
It is only with Frege, Jaskowski and Gentzen that we get proper formalisations of reasoning under assumptions. However, Hodges tracks an early attempt at making the distinction to the Port-Royal logicians
Arnauld and
Nicole. And, even further back, to the writings of
Ibn Sina (Avicenna) in the 11th century.
Hodges analysis is intriguing, but I leave it to the experts to decide whether it is indeed the case that the mode of reasoning under an assumption was not present in, say, the medieval logic literature. Hodges refers to some passages from Burley (
De Puritate Logicae) to support his claim that they are unclear about the distinction between 'Si A, B' and 'Ad A sequitur B'. I'm looking forward to see what the
Medieval Logic group in St Andrews will come up with regarding other medieval logicians. I had two thoughts: first, regarding the historic evidence, that my impression of
Obligationes was one of fairly sophisticated reasoning under assumptions (e.g., in paradoxical cases). Second, that it is interesting that much of contemporary proof-theory has returned to local formalization with sequent calculus.
Looking forward to more CAMELEON events. Meanwhile, you can find some of the handouts
here.
Posts
