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:7947@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20151210T103000
DTEND;TZID=Europe/Paris:20151210T113000
DTSTAMP:20241120T205611Z
URL:https://www.i2m.univ-amu.fr/evenements/fixed-point-elimination-in-the-
 intuitionisitic-propositional-calculus/
SUMMARY:Luigi Santocanale (LIF\, Aix-Marseille Université): Fixed-point el
 imination in the Intuitionisitic Propositional Calculus
DESCRIPTION:Luigi Santocanale: It is a consequence of existing literature t
 hat least and greatest fixed-points of monotone polynomials on Heyting alg
 ebras—that is\, the algebraic models of the Intuitionistic Propositional
  Calculus—always exist\, even when these algebras are not complete as la
 ttices. The reason is that these extremal fixed-points are definable by fo
 rmulas of the IPC. Consequently\, the μ-calculus based on intuitionistic 
 logic is trivial\, every μ-formula being equivalent to a fixed-point free
  formula.\nWe give in this paper an axiomatization of least and greatest f
 ixed-points of formulas\, and an algorithm to compute a fixed-point free f
 ormula equivalent to a given μ-formula. The axiomatization of the greates
 t fixed-point is simple. The axiomatization of the least fixed-point is mo
 re complex\, in particular every monotone formula converges to its least f
 ixed-point by Kleene’s iteration in a finite number of steps\, but there
  is no uniform upper bound on the number of iterations. We extract\, out o
 f the algorithm\, upper bounds for such n\, depending on the size of the f
 ormula. For some formulas\, we show that these upper bounds are polynomial
  and optimal.\nJoint work with Silvio Ghilardi\, Milan\, and Maria Gouveia
 \, Lisbon.\n\n(Séance commune avec l’équipe MoVe du LIF)\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Luigi_Santocanale.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20151025T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR