Saturday, March 7, 2026

Transcendental Syntax I : deterministic case - Jean-Yves Girard

https://girard.perso.math.cnrs.fr/trsy1.pdf

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 spititual: a posteriori (explicit) as far as correctness is concerned, a priori (implicit) for questions dealing with consequence, typically cut-elimination.

No comments:

Post a Comment

Transcendental Syntax I : deterministic case - Jean-Yves Girard

https://girard.perso.math.cnrs.fr/trsy1.pdf We study logic in the light of the Kantian distinction between analytic (untyped, meaningless, l...