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: |
Correctness
Syntax (programming languages) business.industry Computer science 010102 general mathematics 0102 computer and information sciences Locative case 16. Peace & justice 01 natural sciences 03F52 (03B40) Computer Science Applications [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] Mathematics (miscellaneous) 010201 computation theory & mathematics Calculus A priori and a posteriori Transcendental number Artificial intelligence 0101 mathematics business |
| 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 |
| Externí odkaz: |
|