INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES

2018 ◽  
Vol 83 (3) ◽  
pp. 991-1012 ◽  
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.

The bounded functional interpretation of the double negation shift

2010 ◽  
Vol 75 (2) ◽  
pp. 759-773 ◽  
Author(s):  
Engrácia Patrícia ◽  
Fernando Ferreira
Keyword(s):  
Finite Type ◽  
Classical Case ◽  
Double Negation ◽  
Functional Interpretation ◽  
Double Negation Shift

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.

scholarly journals THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT

2017 ◽  
Vol 82 (2) ◽  
pp. 590-607 ◽  
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.

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

2008 ◽  
Vol 67 (2) ◽  
pp. 119-123 ◽  
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.

Relativized realizability in intuitionistic arithmetic of all finite types

1978 ◽  
Vol 43 (1) ◽  
pp. 23-44 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Extension Theorem ◽  
General Notion ◽  
Conservative Extension ◽  
First Order ◽  
New Information ◽  
Reflection Theorem ◽  
Order Arithmetic ◽  
Special Case ◽  
Dependent Choice ◽  
Intuitionistic Arithmetic

In this paper we introduce a new notion of realizability for intuitionistic arithmetic in all finite types. The notion seems to us to capture some of the intuition underlying both the recursive realizability of Kjeene [5] and the semantics of Kripke [7]. After some preliminaries of a syntactic and recursion-theoretic character in §1, we motivate and define our notion of realizability in §2. In §3 we prove a soundness theorem, and in §4 we apply that theorem to obtain new information about provability in some extensions of intuitionistic arithmetic in all finite types. In §5 we consider a special case of our general notion and prove a kind of reflection theorem for it. Finally, in §6, we consider a formalized version of our realizability notion and use it to give a new proof of the conservative extension theorem discussed in Goodman and Myhill [4] and proved in our [3]. (Apparently, a form of this result is also proved in Mine [13]. We have not seen this paper, but are relying on [12].) As a corollary, we obtain the following somewhat strengthened result: Let Σ be any extension of first-order intuitionistic arithmetic (HA) formalized in the language of HA. Let Σω be the theory obtained from Σ by adding functionals of finite type with intuitionistic logic, intensional identity, and axioms of choice and dependent choice at all types. Then Σω is a conservative extension of Σ. An interesting example of this theorem is obtained by taking Σ to be classical first-order arithmetic.

scholarly journals Negation in Berber: Variation, evolution, and typology

Linguistics ◽  
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.

scholarly journals On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Mathematics ◽  
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.

Sign in / Sign up

Export Citation Format

Share Document