In this paper we give a strong normalization proof for a set of reduction rules for classical logic. These reductions, more general than the ones usually considered in literature, are inspired to the reductions of Felleisen's lambda calculus with continuations.

This paper presents a constructive interpretation for the proofs in classical logic of $\Sigma^0_1$ -sentences and for a witness extraction procedure based on Prawitz's reduction rules.

Résumé Dans sa configuration actuelle, l’intellect général est à la fois fragmenté et dépourvu de perception collective et de conscience de soi. Seule l’émergence consciente du travail cognitif comme incarnation sensible et sociale de l’intellect général permettra l’avènement d’une recomposition de notre connaissance commune, scientifique, technique, affective, organisatrice, ainsi que de notre intérêt commun.

An examination of new forms of alienation in our never-off, plugged-in culture—and a clarion call for a “conspiracy of estranged people.” We can reach every point in the world but, more importantly, we can be reached from any point in the world. Privacy and its possibilities are abolished. Attention is under siege everywhere. Not silence but uninterrupted noise, not the red desert, but a cognitive space overcharged with nervous incentives to act: this is the alienation of our times... —from The (...) Soul at Work Capital has managed to overcome the dualism of body and soul by establishing a workforce in which everything we mean by the Soul—language, creativity, affects—is mobilized for its own benefit. Industrial production put to work bodies, muscles, and arms. Now, in the sphere of digital technology and cyberculture, exploitation involves the mind, language, and emotions in order to generate value—while our bodies disappear in front of our computer screens. In this, his newest book, Franco “Bifo” Berardi—key member of the Italian Autonomist movement and a close associate of Félix Guattari—addresses these new forms of estrangement. In the philosophical landscape of the 1960s and 1970s, the Hegelian concept of alienation was used to define the harnessing of subjectivity. The estrangement of workers from their labor, the feeling of alienation they experienced, and their refusal to submit to it became the bases for a human community that remained autonomous from capital. But today a new condition of alienation has taken root in which workers commonly and voluntarily work overtime, the population is tethered to cell phones and Blackberries, debt has become a postmodern form of slavery, and antidepressants are commonly used to meet the unending pressure of production. As a result, the conditions for community have run aground and new philosophical categories are needed. The Soul at Work is a clarion call for a new collective effort to reclaim happiness. The Soul at Work is Bifo's long overdue introduction to English-speaking readers. This Semiotext edition is also the book's first appearance in any language. (shrink)

A wide-ranging exploration of the present, and the future, of the Unconscious. The Unconscious knows no time, it has no before-and-after, it does not have a history of its own. Yet, it is not always the same. As it emerges in the life of people and societies, the Unconscious is shaped by ever-changing historical conditions: its form depends on the unique 'psychosphere' of each historical age. In the early twentieth century, Freud characterised the Unconscious as the dark side of the (...) well-ordered framework of Progress and Reason. At the end of the past century, Deleuze and Guattari described it as a laboratory: the magmatic force that ceaselessly brings about new possibilities of imagination. Today, at a time of viral pandemics and in the midst of the catastrophic collapse of capitalism, the Unconscious has begun to emerge in yet another form. In this book, Franco 'Bifo' Berardi vividly illustrates the form in which the Unconscious will make itself manifest for decades to come, and the challenges that it will pose to our possibilities of political action, poetic imagination, and therapy."--Publisher's description. (shrink)

Introduction: Cartographies in becoming -- The happy depression -- Integrated world capitalism -- Planetary psychopathia -- Postmediatic affect -- User's manual-- Deleuze and the rhizomatic machine -- Why is anti-Oedipus the book of the '68 movement? -- Kafka, hypertext, and assemblages -- The tantric egg -- Chaosmosis -- The provisional eternity of friendship.

_The Uprising_ is an Autonomist manifesto for today's precarious times, and a rallying cry in the face of the catastrophic and irreversible crisis that neoliberalism and the financial sphere have established over the globe. In his newest book, Franco "Bifo" Berardi argues that the notion of economic recovery is complete mythology. The coming years will inevitably see new surges of protest and violence, but the old models of resistance no longer apply. Society can either stick with the prescriptions (...) and "rescues" that the economic and financial sectors have demanded at the expense of social happiness, culture, and the public good; or it can formulate an alternative. For Berardi, this alternative lies in understanding the current crisis as something more fundamental than an economic crisis: it is a crisis of the social imagination, and demands a new language by which to address it. This is a manifesto against the idea of growth, and against the concept of debt, the financial sector's two primary linguistic means of manipulating society. It is a call for exhaustion, and for resistance to the cult of energy on which today's economic free-floating market depends. To this end, Berardi introduces an unexpected linguistic political weapon--poetry: poetry as the insolvency of language, as the sensuous birth of meaning and desire, as that which cannot be reduced to information and exchanged like currency. If the protests now stirring about the world are to take shape and direction, then the revolution will be neither peaceful nor violent--it will be linguistic, or will not be at all. (shrink)

We live in an age of impotence. Stuck between global war and global finance, between identity and capital, we seem to be incapable of producing the radical change that is so desperately needed. Is there still a way to disentangle ourselves from a global order that shapes our politics as well as our imagination? In his most systematic book to date, renowned Italian theorist Franco Berardi tackles this question through a solid yet visionary analysis of the three fundamental (...) concepts of Possibility, Potency, and Power. Characterizing Possibility as the content, Potency as the energy, and Power as the form, Berardi suggests that the road to emancipation unravels from the awareness that the field of the possible is only limited, and not created, by the power structures that implement it. Other futures and other worlds are always already inscribed within the present, despite power's attempt at keeping them invisible. Overcoming any temptation of giving in to despair or nostalgia, Berardi proposes the notion of 'futurability' as a way to remind us that even within the darkness of our current crisis lies dormant the horizon of possibility. (shrink)

In this book, Franco Berardi guides the reader through a wry, dark, disconcerting but also brilliant and invigorating journey through the recent upheavals that we have witnessed. He argues that if our world is dead, then the space is open for another to appear - a world where apocalypse can shake us out of our contemporary zombie-like existence.

Concatenation, conjunction, and connection -- The sensitive infosphere -- Global skin : a trans-identitarian patchwork -- The aesthetic genealogy of globalization -- Language, limit, excess -- Avatars of the general intellect -- The swarm effect -- Social morphogenesis and neuroplasticity -- The transhuman -- The horizon of mutation -- Consciousness and evolution -- The end.

Résumé Si le média-activisme est parvenu à libérer des espaces d’expression, il n’a pas su empêcher les médias dominants, institutionnels et privés, de se réapproprier cette libération. À travers ses effets de saturation et de fragmentation, le « sémiocapitalisme » nous a fait la peau. Les médias dominants ont détruit les médiations individuelles et collectives par leur envoûtement : leur vol du temps et de la sensibilité. C’est la dimension esthétique que le média-activisme doit aujourd’hui investir, d’abord comme art, c’est-à-dire (...) par une nouvelle production de la sensibilité, ensuite comme thérapeutique, c’est-à-dire comme soin apporté à nos appareils bio-médiatiques amoindris. (shrink)

Résumé Une innovation politique susceptible de remodeler le paysage politique mondial est l’enjeu réel de l’unification européenne. Pour ce faire Bifo réclame que le projet européen s’autonomise par rapport à l’extension illimitée du principe libéral porté par les forces mondiales dominantes et prépare leur renversement. Un « nationalisme européen » constituerait une impasse : la construction européenne sera extensive, postnationalitaire, elle se fera par le bas. Constitutionnaliser l’espace européen, c’est constitutionnaliser un devenir de réseaux. Dans le réseau c’est le gouvernement (...) des minorités qui est à l’ordre du jour. (shrink)

Answering to Richard Barbrook’s statements concerning the « the numeric nobility » and « Californian » ideology; Bifo who has lived directly events bound by free radios adventure restores facts and institutionalizing meaning of Felix Guattari’s activist activity. Through the figure of the « technos-nomads », he shows how rhizomatic thought is alone in capacity to realize current changes in the networks universes. He puts bombast it, «aesthetics paradigm » only to realize and to fight against the depth of the (...) contemporary infringements on the sensibility. (shrink)

The purpose of this essay is to provide an interpretive and evaluative introduction to Franco ‘Bifo’ Berardi’s critical media theory and to situate it with a view to understanding but also thinking beyond the limitations of an aesthetic practice rooted almost exclusively in conscious, language-based thought. It begins by examining the way in which Berardi conceptualizes the techno-social paradigm emerging in the passage from late industrial society to semiocapitalism (a form of capitalism based on immaterial labour and (...) the explosion of the infosphere), connecting this to the ecological-aesthetic concerns of Félix Guattari. It concludes by questioning the prospects of poetry to forge lines of escape from the determinism of techno-linguistic governance, suggesting, by way of N. Katherine Hayles and Donna Haraway, that extra-linguistic, nonconscious resources may provide a broader and more viable theoretical palette for conceiving of indeterminability beyond, behind, and in the interstices of a complex digital ecology. (shrink)

Wij presenteren Berardi’s herwerking van de ideologiekritiek in drie stappen. Eerst schetsen wij de context waarin Berardi de ideologiekritiek herdenkt. Hij bouwt verder op de ontdekking van Deleuze en Guattari dat de taal van het kapitalisme niet de code, maar de axiomatiek is. De economische wetenschap biedt, volgens hen, mensen geen identiteit aan, maar bestaat uit een reeks commando’s die stromen van geld, arbeid, elektriciteit, enzovoort reguleert. Daaraan koppelt Berardi de observatie dat het hedendaagse kapitalisme vooral tekens (...) verhandelt in plaats van producten waarnaar zulke tekens zouden verwijzen. In een tweede stap brengen wij tegen deze opvatting in dat Berardi nog steeds vasthoudt aan de representatieve waarde van de economische wetenschap. Deze laatste zou enkel een afbeelding bieden van de realiteit en die vervalsen in het voordeel van het status quo. Sociologen uit de traditie van de actor-netwerktheorie (ANT) hebben dat echter betwist. Zij beweren dat de economische wetenschap de economische realiteit niet zozeer afbeeldt, maar actief vormgeeft. De economische wetenschap heeft de mens geschapen naar zijn evenbeeld: als homo oeconomicus. Het is dan ook een vergissing om de economische wetenschap te bekritiseren voor haar valse representaties. Zij maakt die immers waar. In een derde en laatste stap leggen wij in Berardi’s teksten een nieuw criterium bloot voor ideologiekritiek. In plaats van de economische wetenschap te bekritiseren voor haar valse uitspraken over de realiteit, moeten wij nagaan of de economische wetenschap een manier van leven promoot die mensen in staat zijn te onderhouden. De economische wetenschap is dan ideologisch als en slechts als zij een onhoudbare vorm van leven propageert. Volgens Berardi kan de hedendaagse economische wetenschap hiervan terecht beschuldigd worden. In zijn psychopathologie van het kapitalisme wijst hij immers op de negatieve psychische gevolgen van het hedendaagse kapitalisme, namelijk de instandhouding van een cyclus tussen paniek en depressie, een verlies aan betekenisvol menselijk contact en een neiging tot neurotisch vasthouden aan oude economische recepten die hun failliet reeds meermaals bewezen hebben. Niet de waarheid zal ons verlossen, maar in de verlossing ligt het ware leven. (shrink)

1. La filosofia antica-India, Cina, Grecia -- 2. La filosofia tardo-antica e medioevale: ebraismo, cristianesimo, islamismo -- 3.1. La filosofia moderna: umanesimo, Riforma, rivoluzione scientifica (1350-1715) -- 3.2. La filosofia moderna: illuminismo, criticismo, idealismo (1715-1815) -- 4.1. La filosofia contemporanea: scientismi, sroticismi, irrazionalismi -- 4.2. La filosofia contemporanea: filosofie analitiche e continentali.

We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation.

In the past sixty years or so, a real forest of intuitionistic models for classical theories has grown. In this paper we will compare intuitionistic models of first order classical theories according to relevant issues, like completeness (w.r.t. first order classical provability), consistency, and relationship between a connective and its interpretation in a model. We briefly consider also intuitionistic models for classical ω-logic. All results included here, but a part of the proposition (a) below, are new. This work is, ideally, (...) a continuation of a paper by McCarty, who considered intuitionistic completeness mostly for first order intuitionistic logic. (shrink)

This article compares the political philosophies of Michael Oakeshott and Isaiah Berlin, probably the two most important political philosophers in postwar Britain, who, strangely, had very little to do with one another during their illustrious careers. The article focuses on their respective critiques of rationalism and theories of liberal pluralism, arguing that Oakeshott provides the more consistent and philosophically satisfying account in both instances.

ABSTRACTThis paper analyses the discourses produced on their websites by the two organisations that conducted the official ‘leave’ and ‘remain’ campaigns in the Brexit referendum. The analysis, whi...

In this detailed study of the republican tradition in the development of the Enlightenment, the central problem of utopia and reform is crystallized in a discussion of the right to punish. Describing the political situation in Europe in the seventeenth and eighteenth centuries, the author shows how the old republics in Italy, Poland and Holland stagnated and were unable to survive in the age of absolutism. The Philosophes discussed the ideal of republicanism against this background. They were particularly influenced by (...) the political and religious radicalism of John Toland, which had survived the English Restoration and was then reaching Europe. Professor Venturi traces the debate on the penal laws and the attempt to relate utopian ideas of society to the practical problem of dealing with man in society, which culminated in the assertion by many Philosophes that an unjust social system necessitated harsh penal laws, thereby rejecting the possibility of reform. (shrink)

Volume 16, Issue 4, September 2019, Page 381-388.

We associate with any game G another game, which is a variant of it, and which we call . Winning strategies for have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over , and vice versa. Through we can express in algorithmic form, as a recursive winning strategy, many common proofs of non-constructive Mathematics, namely exactly the theorems of the (...) sub-classical logic Limit Computable Mathematics [6], Hayashi and Nakata [7]). (shrink)

This paper provides a historical reevaluation of the originality and implications of Avempace's critique of Aristotle's causal explanation of the motion of projectiles. It also offers a serious revision of the place which has usually been assigned to Avempace in the history of science. The views regarding projectiles defended in Avempace's Arabic commentary are in sharp opposition to the anti-Aristotelian Avempace that was known in the Medieval West through Averroes. Avempace's commentary reveals only a moderate critic of Aristotle, a critic (...) who did not, in any case, break with the master, and who, therefore, did not even go as far as Philoponus in creating a new and more profound theory of projectile motion. (shrink)

A basic result in intuitionism is Π02-conservativity. Take any proof p in classical arithmetic of some Π02-statement , with P decidable). Then we may effectively turn p in some intuitionistic proof of the same statement. In a previous paper [1], we generalized this result: any classical proof p of an arithmetical statement ∀x.∃y.P, with P of degree k, may be effectively turned into some proof of the same statement, using Excluded Middle only over degree k formulas. When k = 0, (...) we get the original conservativity result as particular case. This result was a by-product of a semantical construction. J. Avigad of Carnegie Mellon University, found a short, direct syntactical derivation of the same result, using H. Friedman's A-translation. His proof is included here with his permission. (shrink)

This paper presents the Futurium platform used by Digital Futures, a foresight project launched by the European Commission's Directorate General for Communications Networks, Content and Technology (DG CONNECT). Futurium was initially developed with the primary purpose of hosting and curating visions and policy ideas generated by Digital Futures (Digital Futures was launched in July 2011 by DG CONNECT's Director General Robert Madelin following a prior DG CONNECT exercise called Digital Science.). However, it has turned into a platform on which to (...) experiment with new policymaking models based on scientific evidence and stakeholder participation, referred to in this paper as ‘Policy Making 3.0’. The platform hosts an online foresight toolkit to facilitate the joint creation of ideas to help design future policies. It leverages the potential of social networks, open data, semantic and knowledge mining technologies as well as participatory brainstorming techniques to engage stakeholders and harness their views and creativity to better inform policies that matter to them. The Futurium distinguishes between different variables, reflecting the emotional vs. rational mindsets of the participants, and offers the possibility to frame the engagement and co-creation process into multiple phases of a workflow. Futurium was developed to support Digital Futures, but its open architecture makes it easily adaptable to any policymaking/decision-making context where thinking ahead, participation, scientific evidence and agility are needed. Futurium is an early prototype implementation of the Policy Making 3.0 model, which is a long-term vision requiring further investigation and experimentation. The Futurium production website can be seen here: ec.europa.eu/digital-agenda/futurium. (shrink)

This article compares the political philosophies of Michael Oakeshott and Isaiah Berlin, probably the two most important political philosophers in postwar Britain, who, strangely, had very little to do with one another during their illustrious careers. The article focuses on their respective critiques of rationalism and theories of liberal pluralism, arguing that Oakeshott provides the more consistent and philosophically satisfying account in both instances.

We introduce an implication-free fragment image of ω-arithmetic, having Exchange rule for sequents dropped. Exchange rule for formulas is, instead, an admissible rule in image. Our main result is that cut-free proofs of image are isomorphic with recursive winning strategies of a set of games called “1-backtracking games” in [S. Berardi, Th. Coquand, S. Hayashi, Games with 1-backtracking, Games for Logic and Programming Languages, Edinburgh, April 2005].We also show that image is a sound and complete formal system for the (...) implication-free fragment of LCM , Seventh International Conference on Typed Lambda Calculi and Applications, in: Lecture Notes in Computer Science, vol. 3461, 2005, pp. 11–22. Invited paper]). A simple syntactical description of this fragment was still missing. No sound and complete formal system is known for LCM itself. (shrink)