Room
0C2 Chevaleret's building 175, rue du Chevaleret 75013
Paris Metro Chevaleret
Thesis abstract
Game
semantics is a modelisation of logic reasoning : if I claim a
proposition, I must be able to reply to any attack on my reasoning by
an imaginary opponent. This interpretation of logic is both flexible
and precise, which is why it has been such a fruitful topic of research during the last decade. The object of the present thesis is to
study game semantics in the case of second order quantification, id est
when one can quantifiy over logical propositions. Our model, inspired
by previous works on that question, is complete for the logic, but more
importantly it is enough compliant to allow us to make calculi and
reasonings. Thus, we use this model to study a question that
concerns only the logical syntax we modelize : namely, the
characterisation of type isomorphisms, which are the equivalence
between formulas induced by syntax. This thesis is built on
three main resuts : the characterisation of type isomorphisms for
Church-style system F, for its classical extension, and for Curry-style
system F. In each case, the characterisation of isomorphisms in the
model is done through the finding of a geometric invariant, which
afterwards can be translated into equations.