L'histoire de la logique se confond avec celle de la philosophie, depuis l'antiquité grecque jusqu'au 20e siècle. Mais ce n'est que dans les années 30 que la réflexion philosophique d'un mathématicien du nom de Brouwer, conduit à la définition rigoureuse d'une logique dite « intuitionniste », distincte de la logique classique qui a régné presque sans partage jusqu'alors. Sterling et Shapiro ont remarqué que la chute du programme de Hilbert qui suivit les résultats d'incomplétude de Gödel et de Turing a marqué aussi le début de l'âge des ordinateurs. On peut ajouter à cette remarque que cette même période s'accompagne d'un intérêt croissant pour cette logique intuitionniste, jusqu'à ce que la recherche sur les logiques dites « constructives » donne aujourd'hui l'impression d'être dominante dans les Départements d'informatique fondamentale. Cet intérêt scientifique contemporain est fondé principalement sur l'isomorphisme de Curry-Howard, c'est-à-dire sur l'équivalence entre preuves et programmes d'une part, et propositions et types d'autre part. Il est cependant difficilement contestable que ce tournant de l'histoire de la logique n'a été perçu et compris que par une minorité de philosophes. Cette conférence qui réunit théoriciens de la preuve, philosophes et historiens de la logique, a pour but de contribuer à mettre fin à cette incompréhension qui s'est peut-être traduite à la fin du 20e siècle par le débat philosophique entre réalisme et anti-réalisme sémantique. C'est la conjonction des perspectives scientifiques et philosophiques qui doit éclairer l'une des questions les plus fondamentales de la philosophie de la connaissance, qui est de savoir si le relativisme s'impose en matière de logique ou bien s'il existe une (ou des) logique(s) fondamentale(s). Il n'est pas anodin que ce thème de réflexion se poursuive dans la ville d'Henri Poincaré qui, en raison de positions proches de l'intuitionnisme, engagea une polémique célèbre contre le logicisme de Russell.
- Didier GALMICHE – (Université de Lorraine, LORIA) – « Sequent Calculi and Decidability for Intuitionistic Hybrid Logic »
- Jean-Baptiste JOINET (Université de Paris 1) - « Sur la correspondance preuves-programmes »
- Dominique LARCHEY-WENDLING - (Université de Lorraine, LORIA) – « Preuves, réfutations et contre-modèles dans des logiques intuitionnistes »
- Sara NEGRI (Université d'Helsinki, Finlande) - « Structural Proof Theory »
- Göran SUNDHOLM (Université de Leyde, Pays Bas) « Constructive validity versus classical logical consequence. »
- Jan von PLATO (Université d'Helsinki, Finlande) - « Proof theory of full classical propositional logic »
- Joseph VIDAL-ROSSET (Université de Lorraine, Archives Poincaré) - « Comment interpréter le plongement de la logique classique dans la logique intuitionniste ? »
Didier GALMICHE – (Université de Lorraine, LORIA)
Sequent Calculi and Decidability for Intuitionistic Hybrid Logic
We study proof theory for the first constructive version of hybrid logic called IHL. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for IHL. In addition to soundness and completeness, we show that this calculus has the cut-elimination property. Finally, we give the first decision procedure for IHL, that is based on this calculus, and therefore we prove its decidability.
In the standard Kripke semantics for modal logics, a model is a transition system where the same formula may have different truth values at different worlds. The hybrid logics were mainly introduced in order to express this relativity of truth by adding to modal logics a new kind of propositional symbols called nominals, and also a new operator, called satisfaction operator, that allows one to jump to the world named by a nominal. There exist many works on hybrid logics, mainly on classical versions, about calculi, decidability and complexity. In this work we aim at studying an intuitionistic version that is the first constructive version of hybrid logic, defined by Brauner and de Paiva and called here IHL. It has been designed from the intuitionistic modal logic IK introduced in, knowing that intuitionistic modal logics have some important applications in computer science, for instance for formal verification of computer hardware and also definition of programming languages. There exists a natural deduction system for IHL, extended with additional inference rules corresponding to conditions on the accessibility relation but in this logic proof-theory and decidability have not really been explored.
Jean-Baptiste JOINET (Université de Paris 1) -
Sur la correspondance preuves-programmes
La perception de la logique, par les logiciens eux-mêmes, a été profondément transformée depuis la fin des années 1970, au fur et à mesure que la « correspondance preuves-programmes » a été étendue de la logique intuitionniste à l'ensemble de la logique classique et à la théorie des ensembles. Au pays recto-verso des preuves-programmes, la question sémantique (ce compagnon de route régulier de la logique, dès la fin du 19e et tout au long du 20e siècle), prend un sens nouveau. La signification du texte d’un programme informatique ne dépend en effet pas, en première instance, de la question sémantique usuelle « à quoi réfère-t-il ? », « que désigne-t-il ? », mais de la question préalable « que fait-il ? », « comment agit-il ? » Partant de cette idée que les programmes informatiques sont des textes dont la signification est d'emblée et paradigmatiquement actionnelle, je commencerai par mettre en place et discuter l'idée qu'un langage de programmation est une axiomatique de l'action. J'analyserai ensuite les conséquences sur la distinction frégéenne entre sens et référence de l'irruption de la notion de programme dans la question sémantique. Je terminerai enfin par un retour sur la logique avec une analyse de l'impact de ces remarques sur la question sémantique en logique et sur les rapports entre syntaxe et sémantique.
Dominique LARCHEY-WENDLING - (Université de Lorraine, LORIA)
Preuves, réfutations et contre-modèles dans des logiques intuitionnistes
Les logiques sont de puissants outils qui permettent la spécification de systèmes informatiques et la preuve de l'adéquation de leur implantation avec ces spécifications. Dans le cadre des logiques sous-structurelles, nous mettons en place des outils de démonstration automatique et de construction de contre-modèles. Ces logiques intègrent la notion de ressources : au niveau de la recherche de preuves, la gestion de ressource permet de construire des modèles fidèles et complets. Nous établissons un lien entre la notion syntaxique de réfutation et la notion sémantique de contre-modèle. Nous en déduisons des méthodes de démonstration de la propriété de modèles finis, ainsi que des algorithmes de construction de contre-modèles. En logique intuitionniste propositionnelle, la gestion fine des ressources permet d'en déduire une implémentation efficace de la recherche de preuves. En logique intuitionniste linéaire, les modèles à base de ressources permettent une preuve élégante de la propriété des modèles finis. Nous établissons un lien entre la sémantique des ressources et la sémantique à base de réseaux de Petri, ce qui permet de raffiner les résultats de complétude partiels connus jusqu'alors.
Sara NEGRI (Université d'Helsinki, Finlande)
On the embedding of Intuitionistic Logic into Intuitionistic Linear Logic
It is well known that Intuitionistic Logic can be faithfully embedded into (Intuitionistic) Linear Logic. For the embedding, or translation, different solutions have been proposed (cf. Girard (1987), Troelstra (1992), Danos et al. (1993)). The purpose of this paper is to study the embedding from a semantical viewpoint, by investigating into the relationship between various models for Intuitionistic Logic and for Intuitionistic Linear Logic. We will follow this pattern: given a structure which is a model for Intuitionistic Linear Logic we explain how to reconstruct inside it a structure which is a model for Intuitionistic Logic. In the first section this procedure is worked out for the algebraic semantics of quantales with modality (cf. Rosenthal (1990), Troelstra (1992), Yetter (1990)). Here it is proved in detail that every quantale with modality gives rise to a frame included in it; furthermore the isomorphism between the complete lattice of modalities on a quantale and the complete lattice of subframes of a quantale is established. Finally, the largest subframe included in a quantale is described. By a result due to G. Sambin, frames and quantales are representable by means of formal topologies and pretopologies respectively (cf. Battilotti and Sambin (199?)). In the appendix, by an extension of these representation theorems to quantales with modality, we show that any quantale with modality is isomorphic to the class of saturated subsets of a suitable pretopology endowed with an operator, already introduced in Sambin (1989), and called {\it stable interior operator}. As an application, we show, given a formal pretopology with a stable interior operator representing a quantale, how to obtain a formal topology representing the subframe determined by the modality. All these semantical considerations lead to consider, in the second section, ``natural'' requirements on translations from Intuitionistic Logic into Intuitionistic Linear Logic. More explicitly, we define a faithful translation corresponding to the insertion of a subframe into its matching quantale with modality, and such that translated formulas are equivalent to their exclamation. Furthermore we define a faithful translation which is also a translation of schemes, that is which commutes with substitution. In the final section we deal with categorical semantics, extensively studied in Linear Logic literature (cf. Barr (1991), Mart\'\i\/-Oliet and Meseguer (1991), de Paiva (1989), Seely(1989), etc.). We study sufficient (and in a way necessary) conditions so that the co-Kleisli construction, applied to a category which is a model for Linear Logic, gives rise to a categorical model for Intuitionistic Logic. In particular, we propose an answer to a question, raised in Seely (1989), concerning the existence of coproducts in the co-Kleisli category. Finally, we show that the algebraic construction developed in the first part is just a particular case of this categorical one, namely its reduction to partial orders.
Göran SUNDHOLM (Université de Leyde, Pays Bas)
The proper explanation of intuitionistic logic
Brouwer’s demonstration of his Bar Theorem gives rise to provocative questions regarding the proper explanation of the logical connectives within intuitionistic and constructivist frameworks, respectively, and, more generally, regarding the role of logic within intuitionism. It is the purpose of the present talk to discuss a number of these issues, both from an historical, as well as a systematic point of view. The Bar Theorem is a theorem in intuitionistic mathematics about trees. A bar is a set of nodes in a tree such that every infinite path through the tree intersects it; every infinite path is barred by that set of nodes. The question arises whether a bar admits of a direct, well-ordered construction. For the development of intuitionistic analysis it turns out to be crucial that such a well-ordered construction be possible. The content of the Bar Theorem is that this is indeed the case: it states that if a tree contains a bar, then it contains a well-ordered bar.
Jan von PLATO (Université d'Helsinki, Finlande)
Reareading Gentzen
We present a series of connected observations on proof theory inspired by a reading of Gentzen’s papers. These include a reconstruction of the reasons that led Gentzen to the particular set of logical rules of sequent calculus, and an interpretation of the structural rules of weakening and contraction in terms of natural deduction for intuitionistic logic.
Joseph VIDAL-ROSSET (Université de Lorraine, Archives Poincaré)
Des fondements de la logique intuitionniste aux méthodes de preuves
A la première page d’un ouvrage intitulé Les fondements des mathématiques - Intuitionnisme - Théorie de la démonstration, Heyting écrit en 1934 :
On affirme encore parfois, à tort, que le but de la recherche des fondements consiste dans l’élimination des contradictions. Au sens philosophique comme au sens mathématique, cette recherche dépasse de beaucoup un tel but. Philosophiquement, elle consiste à examiner l’essence de de la connaissance mathématique, ses hypothèses et son but final, ses rapports avec les autres domaines scientifiques, en particulier avec la physique, et la façon dont elle se distingue de celle-ci par son contenu et sa méthode. A ces discussions philosophiques se rattachent des recherches mathématiques considérables sur la construction de la mathématique à partir d’hypothèses données philosophiquement, et sur la structure des démonstrations mathématiques. Certaines parties de ces recherches se sont déjà développées dans des disciplines autonomes, qui se trouvent être indépendantes des recherches des fondements proprement dites, quant aux méthodes et à la position des problèmes ; la logique mathématique constitue un exemple de branche des mathématiques devant ainsi sa naissance aux recherches sur les fondements.
On se propose de montrer pourquoi Heyting ne peut faire référence ici qu'à la logique intuitionniste et non à la logique classique, et de montrer comment les fondements philosophiques de la logique intuitionniste déterminent intégralement ses méthodes de preuves.
Joseph VIDAL ROSSET (LHSP - Archives Poincaré)