Harmony in the Light of Computational Ludics
| Autor: | Yuta Takahashi, Alberto Naibo |
|---|---|
| Přispěvatelé: | Institut d'Histoire et de Philosophie des Sciences et des Techniques (IHPST), Université Paris 1 Panthéon-Sorbonne (UP1)-Centre National de la Recherche Scientifique (CNRS), Université Paris 1 Panthéon-Sorbonne - UFR Philosophie (UP1 UFR10), Université Paris 1 Panthéon-Sorbonne (UP1), Ochanomizu University, ANR-17-CE38-0003,PROGRAMme,Qu'est-ce qu'un programme? Perspectives historiques et philosophiques(2017), ANR-17-FRAL-0003,FFIUM,Formalisme, formalisation, intuition et compréhension en mathématiques : de la pratique informelle aux systèmes formels et retour(2017), ANR-20-CE27-0004,GoA,La géométrie des algorithmes(2020) |
| Rok vydání: | 2021 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science 010102 general mathematics [SHS.PHIL]Humanities and Social Sciences/Philosophy Logical Constants Proof-theoretic Semantics 06 humanities and the arts Computational Ludics 16. Peace & justice 0603 philosophy ethics and religion 01 natural sciences Harmony Logic in Computer Science (cs.LO) [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] 060302 philosophy F.4.1 Inversion Principle 0101 mathematics Recovery Principle |
| Zdroj: | Electronic Proceedings in Theoretical Computer Science Electronic Proceedings in Theoretical Computer Science, EPTCS, 2021, Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity&TLLA 2020), Online, 29-30 June 2020, 353, pp.132-156. ⟨10.4204/EPTCS.353.7⟩ |
| ISSN: | 2075-2180 |
| DOI: | 10.4204/eptcs.353.7 |
| Popis: | Prawitz formulated the so-called inversion principle as one of the characteristic features of Gentzen's intuitionistic natural deduction. In the literature on proof-theoretic semantics, this principle is often coupled with another that is called the recovery principle. By adopting the Computational Ludics framework, we reformulate these principles into one and the same condition, which we call the harmony condition. We show that this reformulation allows us to reveal two intuitive ideas standing behind these principles: the idea of "containment" present in the inversion principle, and the idea that the recovery principle is the "converse" of the inversion principle. We also formulate two other conditions in the Computational Ludics framework, and we show that each of them is equivalent to the harmony condition. Comment: In Proceedings Linearity&TLLA 2020, arXiv:2112.14305 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|