| Автор | Lambek, J. |
| Дата выпуска | 1997 |
| dc.description | RésuméUn paradigme en vogue en informatique théorique exploite l'analogie entre les formules et les types et traite une deduction A<sub>l</sub> … A<sub>n</sub> → B comme une opération plurisortale. On propose ici d'étendre cette analogie aux déductions de la forme A<sub>l</sub> … A<sub>n</sub> →, où la place à droite de la flèche est vide. D'un point de vue logique, une telle déduction constitue une réfutation de la conjonction desformules qui se trouvent à gauche de la flèche. On défend l'idée qu'ilfaut, selon ce paradigme étendu, interpréter la flèche comme assignant à n'importe quelle séquence a<sub>l</sub> … a<sub>n</sub>, où a<sub>i</sub> est de type A<sub>i</sub>, le type des valeurs de vérite correspondantes. Pour que cela fonctionne, cependant, il faut abandonner la règle structurale de l'affaiblissement à droite de la flèche (cette règle est entièrement abandonnée en logique de la pertinence). La négation de A est alors interprétée comme l'ensemble puissance de A et la complétude fonctionnelle habituelle s'identifie au schème de compréhension avec extensionnalitè. |
| Формат | application.pdf |
| Издатель | Cambridge University Press |
| Копирайт | Copyright © Canadian Philosophical Association 1997 |
| Название | An Extension of the Formulas-as-Types Paradigm |
| Тип | research-article |
| DOI | 10.1017/S0012217300009288 |
| Electronic ISSN | 1759-0949 |
| Print ISSN | 0012-2173 |
| Журнал | Dialogue: Canadian Philosophical Review |
| Том | 36 |
| Первая страница | 33 |
| Последняя страница | 44 |
| Аффилиация | Lambek J.; McGill University |
| Выпуск | 1 |
