iGödel and Ibn Sina in Cambridge
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.
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
2 comments:
Steve Jobs like eh? Flattery will get you everywhere ...
Flattery would have been 'Gödel like' ;)
Post a Comment