By providing an interdisciplinary reading of advance directives regulation in international, European and domestic law, this book offers new insights into the most controversial legal issues surrounding the debate over dignity and autonomy ...

Geometric theories are presented as contraction- and cut-free systems of sequent calculi with mathematical rules following a prescribed rule-scheme that extends the scheme given in Negri and von Plato. Examples include cut-free calculi for Robinson arithmetic and real closed fields. As an immediate consequence of cut elimination, it is shown that if a geometric implication is classically derivable from a geometric theory then it is intuitionistically derivable.

Antonio Negri, a leading scholar on Baruch Spinoza (1632–1677) and his contemporary legacy, offers a straightforward explanation of the philosopher’s elaborate arguments and a persuasive case for his ongoing utility.

In Subversive Spinoza , Antonio Negri spells out the philosophical credo that inspired his radical renewal of Marxism and his compelling analysis of the modern state and the global economy by means of an inspiring reading of the challenging metaphysics of the seventeenth-century Dutch-Jewish philosopher Spinoza. For Negri, Spinoza's philosophy has never been more relevant than it is today to debates over individuality and community, democracy and resistance, modernity and postmodernity.

This pamphlet casts a polemical eye on the panorama of twentieth-century Italian philosophical culture and declares that only three figures stand as exceptions to a pervasive political and intellectual capitulation: Antonio Gramsci, Mario Tronti and Luisa Muraro. Negri argues that the two key post-war contributions to an Italian political ontology, the workerism of Tronti and the feminism of Muraro, start from the identification of the principal forms of exploitation, capitalism and patriarchy, to develop a potent thinking of singularity and (...) creative difference. He concludes that they provide the basis for a political philosophy of the multitude that can at last move beyond postmodernity. (shrink)

Nine letters on art, written to friends from exile in France in the 1980s. Starting from earlier materialist approaches to art, Negri relates artistic production to the structures of social production characteristic of each historical era. This enables him to define the nature of both material and artistic production in the era of post-modernity and post-Fordism - the era Negri characterizes as that of immaterial labour. Negri then seeks to define artistic beauty in this new era, and (...) this he does in terms of concepts that have become fundamental to his thinking - singularity, multitude, abstraction, collective work, event, the biopolitical, the common. Art is living labour, and therefore invention of singularity, of singular figures and objects. But this expressive act only achieves beauty when the signs and language through which it expresses itself turn themselves into community, when they are contained within a common project. The beautiful is not the act of imagining, but an imagination that has become action. Art, in this sense, is multitude. (shrink)

Four men in a cell in Rebibbia prison, Rome, awaiting trial on serious charges of subversion. One of them, the political thinker Antonio Negri, spends his days writing. Among his writings are twenty letters addressed to a young friend in France Ð letters in which Negri reflects on his own personal development as a philosopher, theorist and political activist and analyses the events, activities and movements in which he has been involved. The letters recount an existential journey that (...) links a rigorous philosophical education with a powerful political passion, set against the historical backdrop of postwar Italy. Crucially, Negri recalls the pivotal moment in 1978 when the former prime minister of Italy, Aldo Moro, was kidnapped and killed by the Red Brigades, and how the institutions then pinned that killing onto him and his associates. Published here for the first time, these letters offer a unique and invaluable insight into the factors that shaped the thinking of one of the most influential political theorists of our time and they document Negri’s role in the development of political movements like Autonomia. They are a vivid testimony to one man’s journey through the political upheavals and intellectual traditions of the late 20th century, in the course of which he produced a body of work that has had, and continues to have, a profound impact on radical thought and politics around the world. (shrink)

In this essential rereading of Spinoza's (1632-1677) philosophical and political writings, Negri positions this thinker within the historical context of the development of the modern state and its attendant political economy.

Constituent power : the concept of a crisis -- Virtue and fortune : the machiavellian paradigm -- The Atlantic model and the theory of counterpower -- Political emancipation in the American constitution -- The revolution and the constitution of labor -- Communist desire and the dialectic restored -- The constitution of strength.

Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that (...) restricts its use to cases in which the premiss does not depend on assumptions. This restriction is entirely analogous to the restriction of the rule of universal generalization of first-order logic. A necessitation rule with this restriction permits a proof of the deduction theorem in its usual formulation. Other suggestions presented in the literature to deal with the problem are reviewed, and the present solution is argued to be preferable to the other alternatives. A contraction-and cut-free sequent calculus equivalent to the Hubert system for basic modal logic shows the standard failure argument untenable by proving the underivability of DA from A. (shrink)

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the (...) explanation of the rules. (shrink)

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class (...) is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$, by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$. The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}$. A Gentzen-style reconstruction of the Church–Fitch paradox is presented (...) following a labelled approach to sequent calculi. First, a cut-free system for classical bimodal logic is introduced as the logical basis for the Church–Fitch paradox and the relationships between ${\mathcal {K}}$ and ${\diamondsuit}$ are taken into account. Afterwards, by exploiting the structural properties of the system, in particular cut elimination, the semantic frame conditions that correspond to KP are determined and added in the form of a block of nonlogical inference rules. Within this new system for classical and intuitionistic “knowability logic”, it is possible to give a satisfactory cut-free reconstruction of the Church–Fitch derivation and to confirm that OP is only classically derivable, but neither intuitionistically derivable nor intuitionistically admissible. Finally, it is shown that in classical knowability logic, the Church–Fitch derivation is nothing else but a fallacy and does not represent a real threat for anti-realism. (shrink)

A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

Translation of the authoro's Fabbrica della strategia.

A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefore (...) it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction. (shrink)

A constructive definition of the continuum based on formal topology is given and its basic properties studied. A natural notion of Cauchy sequence is introduced and Cauchy completeness is proved. Other results include elementary proofs of the Baire and Cantor theorems. From a classical standpoint, formal reals are seen to be equivalent to the usual reals. Lastly, the relation of real numbers as a formal space to other approaches to constructive real numbers is determined.

The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for -formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cut-free derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cut-elimination.

Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity results for the theories of constructive order over (...) the usual theories of order. (shrink)

We introduce the concept of partial event as a pair of disjoint sets, respectively the favorable and the unfavorable cases. Partial events can be seen as a De Morgan algebra with a single fixed point for the complement. We introduce the concept of a measure of partial probability, based on a set of axioms resembling Kolmogoroff’s. Finally we define a concept of conditional probability for partial events and apply this concept to the analysis of the two-slit experiment in quantum mechanics.

A proof-theoretical treatment of collectively accepted group beliefs is presented through a multi-agent sequent system for an axiomatization of the logic of acceptance. The system is based on a labelled sequent calculus for propositional multi-agent epistemic logic with labels that correspond to possible worlds and a notation for internalized accessibility relations between worlds. The system is contraction- and cut-free. Extensions of the basic system are considered, in particular with rules that allow the possibility of operative members or legislators. Completeness with (...) respect to the underlying Kripke semantics follows from a general direct and uniform argument for labelled sequent calculi extended with mathematical rules for frame properties. As an example of the use of the calculus we present an analysis of the discursive dilemma. (shrink)

The decision problem for positively quantified formulae in the theory of linearly ordered Heyting algebras is known, as a special case of work of Kreisel, to be solvable; a simple solution is here presented, inspired by related ideas in Gödel-Dummett logic.

A uniform calculus for linear logic is presented. The calculus has the form of a natural deduction system in sequent calculus style with general introduction and elimination rules. General elimination rules are motivated through an inversion principle, the dual form of which gives the general introduction rules. By restricting all the rules to their single-succedent versions, a uniform calculus for intuitionistic linear logic is obtained. The calculus encompasses both natural deduction and sequent calculus that are obtained as special instances from (...) the uniform calculus. Other instances give all the invertibilities and partial invertibilities for the sequent calculus rules of linear logic. The calculus is normalizing and satisfies the subformula property for normal derivations. (shrink)

Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions of such systems from logic (...) to mathematics, and on the connection between the two main forms of structural proof theory - natural deduction and sequent calculus. The authors emphasize the computational content of logical results. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated. (shrink)

This paper explores the question of whether it is possible to be communist without Marx. This entails encountering the ontological dimension of communism, that is, the material tenor of this ontology, its residual effectiveness, the desire of human beings to go beyond capital, and the reality of the episode of statism.

This article investigates three major contexts in which Henry of Ghent’s Summa quaestionum ordinariarum was received from the thirteenth to the fifteenth century. The study takes into account the material features of a group of relevant manuscripts of the Summa: Paris, where the Summa was copied and annotated by Godfrey of Fontaines and his socii; the Dominican convent in Bologna at the beginning of the fourteenth century, to which Aimericus de Placentia gave a copy of the Summa corrected against the (...) very manuscript of Godfrey of Fontaines; the Roman Papal Court, where the Summa attracted the special attention of the humanist Pope Nicholas V, who employed the manuscript from the Bolognese convent for producing new copies of the work. In this study, I endeavour to present a late-medieval history of the Summa as a book, and to contribute to the debate about the mutual relationships among some of the most important witnesses of the text. I pay particular attention to the marginal annotations in t... (shrink)

A proof-theoretical analysis of elementary theories of order relations is effected through the formulation of order axioms as mathematical rules added to contraction-free sequent calculus. Among the results obtained are proof-theoretical formulations of conservativity theorems corresponding to Szpilrajn’s theorem on the extension of a partial order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is shown by giving terminating methods of proof-search.