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:1195@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20160426T140000
DTEND;TZID=Europe/Paris:20160426T150000
DTSTAMP:20201215T134343Z
URL:https://www.i2m.univ-amu.fr/evenements/expressing-theories-in-the-lp-c
 alculus-modulo-theory-and-in-the-dedukti-system/
SUMMARY:Gilles Dowek (LSV\, INRIA\, ENS Paris-Saclay): Expressing theories 
 in the λΠ-calculus modulo theory and in the Dedukti system
DESCRIPTION:Gilles Dowek: Defining a theory\, such as arithmetic\, geometry
 \, or set theory\, in predicate logic just requires to chose function and 
 predicate symbols and axioms\, that express the meaning of these symbols. 
 Using\, this way\, a single logical framework\, to define all these theori
 es\, has many advantages. First\, it requires less efforts\, as the logica
 l connectives\, ∧\, ∨\, ∀... and their associated deduction rules ar
 e defined once and for all\, in the framework and need not be redefined fo
 r each theory. Similarly\, the notions of proof\, model... are defined onc
 e and for all. And general theorems\, such as the soundness and the comple
 teness theorems\, can be proved once and for all. Another advantage of usi
 ng such a logical framework is that this induces a partial order between t
 heories. For instance\, Zermelo-Fraenkel set theory with the axiom of choi
 ce (ZFC) is an extension of Zermelo-Fraenkel set theory (ZF)\, as it conta
 ins the same axioms\, plus the axiom of choice. It is thus obvious that an
 y theorem of ZF is provable in ZFC\, and for each theorem of ZFC\, we can 
 ask the question of its provability in ZF. Several theorems of ZFC\, that 
 are provable in ZF have been identified\, and these theorems can be used i
 n extensions of ZF that are inconsistent with the axiom of choice. Finally
 \, using such a common framework permits to combine\, in a proof\, lemmas 
 proved in different theories: if T is a theory expressed in a language L a
 nd T a theory expressed in a language L \, if A is expressed in L ∩ L \,
  A ⇒ B is provable in T \, and A is provable in T \, then B is provable 
 in T ∪ T. Despite these advantages\, several logical systems have been d
 efined\, not as theories in predicate logic\, but as independent systems: 
 Simple type theory\, also known as Higher-order logic\, is defined as an i
 ndependent system—although it is also possible to express it as a theory
  in predicate logic. Similarly\, Intuitionistic type theory\, the Calculus
  of constructions\, the Calculus of inductive constructions... are defined
  as independent systems. As a consequence\, it is difficult to reuse a for
 mal proof developed in an automated or interactive theorem prover based on
  one of these formalisms in another\, without redeveloping it. It is also 
 difficult to combine lemmas proved in different systems: the realm of form
 al proofs is today a tower of Babel\, just like the realm of theories was\
 , before the design of predicate logic. The reason why these formalisms ha
 ve not been defined as theories in predicate logic is that predicate logic
 \, as a logical framework\, has several limitations\, that make it difficu
 lt to express modern logical systems.
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Gilles_Dowek.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20160327T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR