Transcendental syntax I: deterministic case

Autor: Jean-Yves Girard
Přispěvatelé: Institut de Mathématiques de Marseille (I2M), Aix Marseille Université (AMU)-École Centrale de Marseille (ECM)-Centre National de la Recherche Scientifique (CNRS), ANR-10-BLAN-0213,LOGOI,Logique et géometrie de l'interaction(2010)
Jazyk: angličtina
Rok vydání: 2017
Předmět:
Zdroj: Mathematical Structures in Computer Science
Mathematical Structures in Computer Science, 2017, 27 (5), pp.827-849. ⟨10.1017/S0960129515000407⟩
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2017, 27 (5), pp.827-849. ⟨10.1017/S0960129515000407⟩
ISSN: 0960-1295
1469-8072
Popis: 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.
Databáze: OpenAIRE