What sequential games, the tychonoff theorem and the double-negation shift have in common

AbstractWe prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functional of finite type. As an application, we show that full numerical comprehension is compatible with the uniformities introduced by the characteristic principles of the bounded functional interpretation for the classical case.

Download Full-text

INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES

Journal of Symbolic Logic ◽

10.1017/jsl.2017.63 ◽

2018 ◽

Vol 83 (3) ◽

pp. 991-1012 ◽

Cited By ~ 2

Author(s):

MAKOTO FUJIWARA ◽

ULRICH KOHLENBACH

Keyword(s):

Consistency Proof ◽

Double Negation ◽

Double Negation Shift ◽

Negative Translation ◽

Intuitionistic Arithmetic

AbstractWe investigate two weak fragments of the double negation shift schema, which are motivated, respectively, from Spector’s consistency proof of ACA0 and from the negative translation of RCA0, as well as double negated variants of logical principles. Their interrelations over both intuitionistic arithmetic and analysis are completely solved.

Download Full-text

THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT

Journal of Symbolic Logic ◽

10.1017/jsl.2017.8 ◽

2017 ◽

Vol 82 (2) ◽

pp. 590-607 ◽

Cited By ~ 1

Author(s):

MARTÍN ESCARDÓ ◽

PAULO OLIVA

Keyword(s):

Double Negation ◽

Functional Interpretation ◽

Image Position ◽

Special Case ◽

Double Negation Shift

AbstractThis paper considers a generalisation of selection functions over an arbitrary strong monad T, as functionals of type $J_R^T X = (X \to R) \to TX$. It is assumed throughout that R is a T-algebra. We show that $J_R^T$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of T-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector’s bar recursion. We then prove several properties of this product in the special case when T is the finite powerset monad ${\cal P}_{\rm{f}} \left( \cdot \right)$. These are used to show that when $TX = {\cal P}_{\rm{f}} \left( X \right)$ the explicitly controlled product of T-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.

Download Full-text

Test d’Indépendance au Contexte (TIC) et Structure des Représentations Sociales

Swiss Journal of Psychology ◽

10.1024/1421-0185.67.2.119 ◽

2008 ◽

Vol 67 (2) ◽

pp. 119-123 ◽

Cited By ~ 28

Author(s):

Grégory Lo Monaco ◽

Florent Lheureux ◽

Séverine Halimi-Falkowicz

Keyword(s):

Double Negation ◽

Représentations Sociales ◽

Representations Sociales

Deux techniques permettent le repérage systématique du système central d’une représentation sociale: la technique de la mise en cause (MEC) et le modèle des schèmes cognitifs de base (SCB). Malgré cet apport, ces techniques présentent des inconvénients: la MEC, de par son principe de double négation, et les SCB, de par la longueur de passation. Une nouvelle technique a été développée: le test d’indépendance au contexte (TIC). Elle vise à rendre compte des caractères trans-situationnel ou contingent des éléments représentationnels, tout en présentant un moindre coût cognitif perçu. Deux objets de représentation ont été étudiés auprès d’une population étudiante. Les résultats révèlent que le TIC paraît, aux participants, cognitivement moins coûteux que la MEC. De plus, le TIC permet un repérage du noyau central identique à celui offert par la MEC.

Download Full-text

COMPACTNESS DEGREE AND A GENERALIZATION OF THE TYCHONOFF THEOREM

Acta Mathematica Scientia ◽

10.1016/s0252-9602(18)30416-8 ◽

1990 ◽

Vol 10 (4) ◽

pp. 422-426

Author(s):

Banghe Li ◽

Hanqiao Feng

Keyword(s):

Tychonoff Theorem

Download Full-text

Negation in Berber: Variation, evolution, and typology

Linguistics ◽

10.1515/ling-2020-0010 ◽

2020 ◽

Vol 58 (4) ◽

pp. 967-1008

Author(s):

Mena B. Lafkioui ◽

Vermondo Brugnatelli

Keyword(s):

North Africa ◽

North African ◽

Double Negation ◽

New Developments ◽

Area North

AbstractDouble and triple negation marking is an ancient and deep-rooted feature that is attested in almost the entire Berber-speaking area (North Africa and diaspora), regardless of the type of negators in use; i. e., discontinuous markers (preverbal and postverbal negators) and dedicated negative verb stem alternations. In this article, we deal with the main stages that have led to the present Berber negation patterns and we argue, from a typological viewpoint, that certain morphophonetic mechanisms are to be regarded as a hitherto overlooked source for new negators. Moreover, we present a number of motivations that account for the hypothesis that, in Berber, those languages with both a preverbal and a postverbal negator belong to a diachronic stage prior to the attested languages with a preverbal negator only. Consequently, the study demonstrates that the Jespersen Cycle is back to the beginning in certain Berber languages. In doing so, we also show that Berber is to be regarded as a substrate in the development of double negation in North African Arabic. In addition, the study accounts for the asymmetric nature of Berber negation, although some new developments towards more symmetrical negation configurations are also attested.

Download Full-text

Computation of Stackelberg Equilibria of Finite Sequential Games

ACM Transactions on Economics and Computation ◽

10.1145/3133242 ◽

2017 ◽

Vol 5 (4) ◽

pp. 1-24 ◽

Cited By ~ 2

Author(s):

Branislav Bošanský ◽

Simina Brânzei ◽

Kristoffer Arnsfelt Hansen ◽

Troels Bjerre Lund ◽

Peter Bro Miltersen

Keyword(s):

Sequential Games

Download Full-text

On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Mathematics ◽

10.3390/math9040385 ◽

2021 ◽

Vol 9 (4) ◽

pp. 385

Author(s):

Hyeonseung Im

Keyword(s):

Programming Languages ◽

Intuitionistic Logic ◽

Reference Point ◽

Classical Logic ◽

Proof System ◽

Double Negation

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

Download Full-text