Hostname: page-component-78c5997874-t5tsf Total loading time: 0 Render date: 2024-11-07T01:52:15.520Z Has data issue: false hasContentIssue false
  • English
  • Français

Transcendental syntax I: deterministic case

Published online by Cambridge University Press:  20 July 2015

JEAN-YVES GIRARD
JEAN-YVES GIRARD*
Affiliation:
Institut de Mathématiques de Marseille, Campus de Luminy, Case 907, 13288 Marseille Cedex 9, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We study logic in the light of the Kantian distinction between analytic (untyped, meaningless, locative) answers and synthetic (typed, meaningful, spiritual) questions. Which is specially relevant to proof-theory: in a proof-net, the upper part is locative, whereas the lower part is spiritual: a posteriori (explicit) as far as correctness is concerned, a priori (implicit) for questions dealing with consequence, typically cut-elimination. The divides locative/spiritual and explicit/implicit give rise to four blocks which are enough to explain the whole logical activity.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 27 , Special Issue 5: Computing with Lambda-terms. A Special Issue Dedicated to Corrado Böhm for his 90th Birthday , June 2017 , pp. 827 - 849
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aubert, C., Bagnol, M., Pistone, P. and Seiller, T. (2014). Logic programming and logarithmic space. In: Garrigue (ed.) Proceedings of the 12th Asian Symposium APLAS. Springer Lecture Notes in Computer Science 8858 39–57.CrossRefGoogle Scholar
Danos, V. and Regnier, L. (1989). The structure of multiplicatives. Archive for Mathematical Logic 28 181–203.CrossRefGoogle Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 1–102.CrossRefGoogle Scholar
Girard, J.-Y. (1989). Geometry of interaction I: Interpretation of system F . In: Ferro, R., Bonotto, C., Valentini, S. and Zanardo, A. (eds.) Logic Colloquium '88, Amsterdam, North-Holland 221–260.Google Scholar
Girard, J.-Y. (1995). Geometry of interaction III: Accommodating the additives. In: Girard, J.-Y., Lafont, Y. and Regnier, R. (eds.) Advances in Linear Logic, Cambridge, Cambridge University Press 329–389.Google Scholar
Girard, J.-Y. (2011a). Geometry of interaction V: Logic in the hyperfinite factor. Girard's Festschrift, Ehrhard, T., Faggian, C. and Laurent, O. (eds.) Theoretical Computer Science vol. 412 1860–1883.CrossRefGoogle Scholar
Girard, J.-Y. (2011b). The Blind Spot: Lectures on Logic, Zürich 550, European Mathematical Society.Google Scholar
Girard, J.-Y. (2012). Normativity in logic. In: Dyjber, P., Lindström, S., Palmgren, E. and Sundholm, G. (eds.) Epistemology vs. Ontology, Springer-Verlag 243–264.CrossRefGoogle Scholar
Girard, J.-Y. (2016). Transcendental syntax II: Non-deterministic case. Logical Methods in Computer Science, to appear.Google Scholar
Mogbil, V. and Jacobé de Naurois, P. (2011). Correctness of multiplicative additive proof-structures is NL-complete. Theoretical Computer Science 412 (20) 1941–1957.Google Scholar
Seiller, T. (2013). Interaction graphs: Exponentials. Computing Research Repository, abs/1312.1094, Available at: http://arxiv.org/abs/1312.1094.Google Scholar