Hostname: page-component-745bb68f8f-mzp66 Total loading time: 0 Render date: 2025-02-11T00:11:29.287Z Has data issue: false hasContentIssue false
  • English
  • Français

First order in Ludics

Published online by Cambridge University Press:  17 March 2004

MARIE-RENEE FLEURY  and
MYRIAM QUATRINI
MARIE-RENEE FLEURY
Affiliation:
Institut de Mathématiques de Luminy, UPR 9016 C.N.R.S., Université de la Méditerranée, 163, avenue de Luminy – Case 907, 13288 Marseille Cedex 9 – France Email: mrd@iml.univ-mrs.fr
MYRIAM QUATRINI
Affiliation:
Institut de Mathématiques de Luminy, UPR 9016 C.N.R.S., Université de la Méditerranée, 163, avenue de Luminy – Case 907, 13288 Marseille Cedex 9 – France Email: quatrini@iml.univ-mrs.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

In Girard (2001), J.-Y. Girard presents a new theory, The Ludics, which is a model of realisibility of logic that associates proofs with designs, and formulas with behaviours. In this article we study the interpretation in this semantics of formulas with first-order quantifications and their proofs. We extend to the first-order quantifiers the full completeness theorem obtained in Girard (2001) for $MALL_2$. A significant part of this article is devoted to the study of a uniformity property for the families of designs that represent proofs of formulas depending on a first-order free variable.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 14 , Issue 2 , April 2004 , pp. 189 - 213
Copyright
2004 Cambridge University Press