Martin-Löf Conference on the Foundations of Mathematics: Day 2
The second conference day promised the greatest spectacle of them all. For years I’ve wanted to see Girard in action, in fact I’ve been to an event or two to see him only to find that he couldn’t make it. Day 2 finally delivered: the morning session was Girard with ‘Towards Non-Commutative Foundations’. I find it impossible to report reliably on the content of the talk – even if some of it was familiar from his writings (proof nets and the “geometry of interaction”), most of it was either mystical or mathematical. From what I could gather, Girard invokes a notion of ‘entanglement’, a label for the idea that proofs somehow affect or even distort the models (“the subject appears as a commutative window”), a thought explicitly inspired by quantum physics. The “object” -- in Girard’s view part of a non-commutative foundations -- is somehow elusive: “You have to become commutative to have a notion of mistake”... As a logician I find myself hopelessly lost, and as a philosopher I wonder if I’m in the presence of brilliancy or quakery, yet there is something seducing about his prophetic style. In any event, I recommend having a look at some of his writing, for example ‘Linear Logic, its syntax and semantics’. Incidentally, a signifcant part of his opus is availble online.
On a more sober note, Peter Pagin took us back to more mainstream philosophy later in the day. Pagin has been to St Andrews a number of times, and I’ve always thoroughly enjoyed his talks. ‘Assertion, truth, and judgement’ is an honest attempt at bringing together his work on assertion and assertoric content with Martin-Löf’s proposition/judgement distinction in a type-theoretic setting.
The starting point is a puzzle about propositions and disagreement: When a speaker asserts a proposition p, we might be tempted by the thought that the proposition is somehow about the world of utterance to include a world index in the structure of the proposition ‘In w, p’, where w is fixed by the context of utterance. Yet this threatens to trivialise propositional content since it is either true in every world or false in every world (compare the old puzzle about mathematical propositions in propositions-as-sets-of-possible-worlds). Thus, propositions are too coarse-grained to function as what is tracked in genuine disagreement.
Pagin is a proponent of the information account of assertion (an utterance is assertoric iff it is informative), and his general strategy for the above puzzle is to separate propositional content from assertoric content. This suggests, Pagin proposes, an analogy to Martin-Löf’s judgments, a : A where a is a proof object, or truth-maker, and A is the proposition (think w : A read ‘A is (actually) true’). The guiding idea is that type-theory offers, by analogy, a way to get more fine-grained distinctions by way of truth-makers. Since assertoric content can thus be used in a theory of disagreement, we avoid the problem of individuating propositional content further.
On a more sober note, Peter Pagin took us back to more mainstream philosophy later in the day. Pagin has been to St Andrews a number of times, and I’ve always thoroughly enjoyed his talks. ‘Assertion, truth, and judgement’ is an honest attempt at bringing together his work on assertion and assertoric content with Martin-Löf’s proposition/judgement distinction in a type-theoretic setting.
The starting point is a puzzle about propositions and disagreement: When a speaker asserts a proposition p, we might be tempted by the thought that the proposition is somehow about the world of utterance to include a world index in the structure of the proposition ‘In w, p’, where w is fixed by the context of utterance. Yet this threatens to trivialise propositional content since it is either true in every world or false in every world (compare the old puzzle about mathematical propositions in propositions-as-sets-of-possible-worlds). Thus, propositions are too coarse-grained to function as what is tracked in genuine disagreement.
Pagin is a proponent of the information account of assertion (an utterance is assertoric iff it is informative), and his general strategy for the above puzzle is to separate propositional content from assertoric content. This suggests, Pagin proposes, an analogy to Martin-Löf’s judgments, a : A where a is a proof object, or truth-maker, and A is the proposition (think w : A read ‘A is (actually) true’). The guiding idea is that type-theory offers, by analogy, a way to get more fine-grained distinctions by way of truth-makers. Since assertoric content can thus be used in a theory of disagreement, we avoid the problem of individuating propositional content further.
Posts
No comments:
Post a Comment