BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:8121@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20150327T000000
DTEND;TZID=Europe/Paris:20150327T000000
DTSTAMP:20241210T143237Z
URL:https://www.i2m.univ-amu.fr/evenements/sur-les-preuves-et-les-types-da
 ns-la-logique-du-second-ordre/
SUMMARY:Paolo Pistone (I2M\, Aix-Marseille Université): Sur les preuves et
  les types dans la logique du second ordre
DESCRIPTION:Paolo Pistone: Sous la direction de Jean-Yves Girard.\n\nSouten
 ue le 27-03-2015\n\nà Aix-Marseille en cotutelle avec  l'Università degl
 i studi di Roma "Tor Vergata". Facoltà di scienze \, dans le cadre de  Ec
 ole Doctorale Mathématiques et Informatique de Marseille (Marseille) .\n\
 nLe président du jury était Pierre-Louis Curien.\n\nLe jury était compo
 sé de Enrico Moriconi\, Simone Martini.\n\nLes rapporteurs étaient Guise
 ppe Longo\, Jean baptiste Joinet.\n\nTitle: On Proofs and Types in Second 
 Order Logic\nIn my dissertation I address some questions concerning the pr
 oof theory of second order logic and its constructive counterpart\, System
  F (Girard 1971). These investigations follow two distinct (though histori
 cally related) viewpoints in proof theory\, which are compared throughout 
 the text: on the one side\, the proof theoretic semantics tradition inaugu
 rated by Dummett and Prawitz (Prawitz 1971\, Dummett 1991)\, focusing on t
 he analysis of the inferential content of proofs\; on the other side\, the
  interactionist tradition arising from Kleene's realizability (Kleene 1945
 ) and the Tait/Girard reducibility technique (Tait 1967\, Girard 1971)\, w
 hich interprets proofs as untyped programs and focuses\, rather\, on the b
 ehavioral content of proofs\, i.e. the way in which they interact through 
 the cut-elimination algorithm.\nA distinction is made between the issues o
 f justifying and understanding ("explaining why" and "explaining how"\, as
  in Girard 2000) impredicative reasoning\, i.e. between non elementary res
 ults like the Hauptsatz and the combinatorial analysis of proofs\, seen as
  programs\, i.e. recursive objects.\nAs for justifi-cation\, an epistemolo
 gical analysis of the circularity involved in the second order Hauptsatz i
 s developed\; it is shown that the usual normalization arguments for secon
 d order logic do not run into the vicious circularity claimed by Poincar-
 é and Russell\, but involve a\ndiff-erent\, epistemic\, form of circulari
 ty. Still\, this weaker circularity makes justifi-cation\, in a sense\, po
 intless\; in particular\, some examples of inconsistent higher order theor
 ies admitting epistemically circular normalization arguments are discussed
 .\nAs for the explanation issue\, a constructive and combinatorial (i.e. i
 ndependent from normalization) analysis of higher order order quantifi-cat
 ion is developed along two directions\, with some related technical result
 s. The fi-rst direction arises from the parametric and dinatural interpret
 ations of polymorphism (Reynolds 1983\, Girard-Scott-Scedrov 1992)\, which
  provide a clear mathematical meaning to Carnap's defense of impredicative
  quanti-fication (Carnap 1983). In particular\, the violation of the param
 etric condition leads to paradoxes which are often ignored in the philosop
 hical literature (with the exception of Longo-Fruchart 1997). The analysis
  of the combinatorial content of these interpretations leads to a -1-compl
 eteness theorem (every normal closed --term in the universal closure of a 
 simple type is typable in simple type theory)\, which connects the interac
 tionist and the inferential conceptions of proof.\nThe second direction fo
 llows the analysis of the typing conditions of the --terms associated with
  intuitionistic second order proofs. To the \\vicious circles" in the proo
 fs there correspond recursive (i.e. circular) speci-fications for the type
 s of the --terms. The geometrical structure of these vicious circles is in
 vestigated (following Lechenadec 1989\, Malecki 1990\, Giannini - Ronchi D
 ella Rocca 1991)\, leading to a combinatorial characterization of typabili
 ty in some inconsistent extension of System F: since\, as Girard's paradox
  shows\, a typable term need not be normalizing\, one is indeed naturally 
 led to consider not normalizing theories.\nSuch investigations go in the d
 irection both of a mathematical understanding of the structure generated b
 y the vicious circles of impredicative theories and of the development of 
 a proof-theoretic analysis of potentially incorrect or uncertain proofs.\n
 -\nKeywords : Type Theory\, Proof Theory\, Philosophy of Logic\, Cut-Elimi
 nation\, Second-order logic\, Lambda Calculus\, Impredicativity.\n-\n\nhtt
 p://www.academia.edu/10495837/On_Proofs_and_Types_in_Second_Order_Logic\nL
 ien : theses.fr
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/12/Paolo_Pistone.jpg
CATEGORIES:Soutenance de thèse,AGLR,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20141026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR