Feminist theorist and philosopher Donna Haraway has substantially impacted thought on science, cyberculture, the environment, animals, and social relations. This long-overdue volume explores her influence on feminist theory and philosophy, paying particular attention to her more recent work on companion species, rather than her "Manifesto for Cyborgs." Margret Grebowicz and Helen Merrick argue that the ongoing fascination with, and re-production of, the cyborg has overshadowed Haraway's extensive body of work in ways that run counter to her own transdisciplinary practices. (...) Sparked by their own personal "adventures" with Haraway's work, the authors offer readings of her texts framed by a series of theoretical and political perspectives: feminist materialism, standpoint epistemology, radical democratic theory, queer theory, and even science fiction. They situate Haraway's critical storytelling and "risky reading" practices as forms of feminist methodology and recognize her passionate engagement with "naturecultures" as the theoretical core driving her work. Chapters situate Haraway as critic, theorist, biologist, feminist, historian, and humorist, exploring the full range of her identities and reflecting her commitment to embodying all of these modes simultaneously. (shrink)

Now that pornography is on the Internet, its political and social functions have changed. So contends Margret Grebowicz in this imperative philosophical analysis of Internet porn. The production and consumption of Internet porn, in her account, are a symptom of the obsession with self-exposure in today's social networking media, which is, in turn, a symptom of the modern democratic construction of the governable subject as both transparent and communicative. In this first feminist critique to privilege the effects of pornography's (...) Internet distribution rather than what it depicts, Grebowicz examines porn-sharing communities and the politics of putting women's sexual pleasure on display as part of the larger democratic project. Arguing against this project, she shows that sexual pleasure is not a human right. Unlikely convergences between thinkers like Catherine MacKinnon, Jean Baudrillard, Judith Butler, and Jean-François Lyotard allow her to formulate a theory of the relationships between sex, speech, and power that stands as an alternative to such cyber-libertarian mottos as "freedom of speech" and "sexual freedom.". (shrink)

Why “do” philosophy, if not to contribute to social consciousness , to develop ideas for change, to articulate the desperations of the present and the possibilities of futures which will help people, however loosely we define “people”? This is one of the most popular objections to philosophy: that it is not practical, and therefore not really politically useful. And in today’s philosophical arena, this argument is directed specifically against postmodern philosophies. However, there is another sense of the word “postmodern,” which (...) we often forget when talking about postmodernism. Lyotard wants us to think about that which resists institutionalization, homogenization, academic taxonomies, economies, and genealogies. The postmodern is the moment of ideological instability and confusion, of radical undermining of foundations and transgressing of boundaries. It is just another name for thought. In this essay, I attempt to describe a sort of postmodern praxis in terms of the Lyotardian notion of thought, discussing the work of Simone de Beauvoir, Hardt and Negri, and June Jordan. (shrink)

This article investigates the intersections of secrecy/interiority, the state, and speech/ expression, and their implications for the rights of women. I propose a critique of commercial pornography that reanimates MacKinnon's claim that pornography and American democracy are in a relationship of mutual reinforcement, and incorporates poststructuralist (Lyotard, Baudrillard, and Butler) commitments to secrecy and unintelligibility, as well as their role in the production of pleasure.

At the end of his attack on my use of the psychoanalytic model for the interpretation of literature, Heller raises the question concerning what the task of the literary critic is or ought to be. His own "sketch of the Kleistean theme's historical ancestry and its later development," he says, seeks to deepen and enrich the reader's appreciation of Kleist's literary art, the artistry of his phrasing, the persuasiveness of his incidents, the conclusiveness of his examples." By implication he suggests (...) that my method does not have this end—that is, appreciation—for its goal. In this he is partially right. "Appreciation" in Heller's sense is not as directly a goal for me. But does Heller's method of intellectual history and literary relation meet his own criteria of deepening and enriching the reader's appreciation of Kleist? In his capsule treatment of Great Thinkers of the Western World from Plato to Marx, we learn that many writers besides Kleist treated Kleist's theme of man's fall from unconscious grace. What exactly does this tell us about Kleist's treatment of it? How does it deepen the reader's appreciation of Kleist's literary art, the artistry of his phrasing, the persuasiveness of his incidents? It doesn't. It isn't even about Kleist. Although Heller tells us that it is the "thought" and "imagery" which "make for the great distinction of the essay" , his evidence for this consists, in the case of the former, in his tracing the history of the essay's thought and, in the case of the latter, in his statements that Kleist's use of the puppet as the exemplar of the unselfconscious graceful being is "unusual" and "novel" and that his bear story, though it may lack "in immediate plausibility," "gains in making Kleist's point" and is "a memorable exemplar" of the "art of grotesque inventions that are capable of floating for quite a while above and between the comic and the serious before landing with scintillating effect in one domain or the other" . Margret Schaefer is a lecturer in the department of psychiatry at Northwestern University Medical School. She responds here to Erich Heller's "The Dismantling of a Marionette Theater; or, Psychology and the Misinterpretation of Literature" , in which he discussed her article, "Kleist's 'About the Puppet Theater,". (shrink)

In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic PA one can find ordinal recursive functionals Φ A of order type 0 which realize the Herbrand normal form A H of A. Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do (...) not carry out the no-counterexample interpretation as a local proof interpretation and don't respect the modus ponens on the level of the no-counterexample interpretation of formulas A and A → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and--at least not constructively-- (γ) which are part of the definition of an 'interpretation of a formal system' as formulated in [15]. In this paper we determine the complexity of the no-counterexample interpretation of the modus ponens rule for (i) PA-provable sentences, (ii) for arbitrary sentences A, B ∈ L(PA) uniformly in functionals satisfying the no-counterexample interpretation of (prenex normal forms of) A and A → B, and (iii) for arbitrary A, B ∈ L(PA) pointwise in given α( 0 ) -recursive functionals satisfying the no-counterexample interpretation of A and A → B. This yields in particular perspicuous proofs of new uniform versions of the conditions (γ), (δ). Finally we discuss a variant of the concept of an interpretation presented in [17] and show that it is incomparable with the concept studied in [15], [16]. In particular we show that the no-counterexample interpretation of PA n by α( n (ω))-recursive functionals (n ≥ 1) is an interpretation in the sense of [17] but not in the sense of [15] since it violates the condition (δ). (shrink)

Synthetic biology" is the label of a new technoscientific field with many different facets and agendas. One common aim is to "create life", primarily by using engineering principles to design and modify biological systems for human use. In a wider context, the topic has become one of the big cases in the legitimization processes associated with the political agenda to solve global problems with the aid of (bio-)technological innovation. Conceptual-level and meta-level analyses are needed: we should sort out conceptual ambiguities (...) to agree on what we talk about, and we need to spell out agendas to see the disagreements clearly. The book is based on the interdisciplinary summer school "Analyzing the societal dimensions of synthetic biology", which took place in Berlin in September 2014. The contributions address controversial discussions around the philosophical examination, public perception, moral evaluation and governance of synthetic biology. (shrink)

We show how to extract effective bounds Φ for $\bigwedge u^1 \bigwedge v \leq_\gamma tu \bigvee w^\eta G_0$ -sentences which depend on u only (i.e. $\bigwedge u \bigwedge v \leq_\gamma tu \bigvee w \leq_\eta \Phi uG_0$ ) from arithmetical proofs which use analytical assumptions of the form \begin{equation*}\tag{*}\bigwedge x^\delta\bigvee y \leq_\rho sx \bigwedge z^\tau F_0\end{equation*} (γ, δ, ρ, and τ are arbitrary finite types, η ≤ 2, G0 and F0 are quantifier-free, and s and t are closed terms). If τ (...) ≤ 2, (*) can be weakened to $\bigwedge x^\delta, z^\tau\bigvee y \leq_\rho sx \bigwedge \tilde{z} \leq_\tau z F_0$ . This is used to establish new conservation results about weak König's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers. (shrink)

In this paper, we present another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation developed in Kohlenbach , Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheney's simplification 189) of Jackson's original proof 320) of the uniqueness of the best L1-approximation of continuous functions fC[0,1] by polynomials pPn of degree n. (...) Cheney's proof is non-effective in the sense that it is based on classical logic and on the non-computational principle WKL . The result of our analysis provides the first effective uniform modulus of uniqueness . Moreover, the extracted modulus has the optimal ε-dependency as follows from Kroó 331). The paper also describes how the uniform modulus of uniqueness can be used to compute the best L1-approximations of a fixed fC[0,1] with arbitrary precision. The second author uses this result to give a complexity upper bound on the computation of the best L1-approximation in Oliva 66–77). (shrink)

A pointwise version of the Howard-Bezem notion of hereditary majorization is introduced which has various advantages, and its relation to the usual notion of majorization is discussed. This pointwise majorization of primitive recursive functionals (in the sense of Gödel'sT as well as Kleene/Feferman's ) is applied to systems of intuitionistic and classical arithmetic (H andH c) in all finite types with full induction as well as to the corresponding systems with restricted inductionĤ↾ andĤ↾c.H and Ĥ↾ are closed under a generalized (...) fan-rule. For a restricted class of formulae this also holds forH c andĤ↾c.We give a new and very perspicuous proof that for each one can construct a functional such that $\tilde \Phi \alpha $ is a modulus of uniform continuity for Φ on {β1∣∧n(βn≦αn)}. Such a modulus can also be obtained by majorizing any modulus of pointwise continuity for Φ.The type structure ℳ of all pointwise majorizable set-theoretical functionals of finite type is used to give a short proof that quantifier-free “choice” with uniqueness (AC!)1,0-qf. is not provable within classical arithmetic in all finite types plus comprehension [given by the schema (C)ϱ:∨y 0ϱ∧x ϱ(yx=0⇔A(x)) for arbitraryA], dependent ω-choice and bounded choice. Furthermore ℳ separates several μ-operators. (shrink)

It is well known by now that large parts of mathematical reasoning can be carried out in systems which are conservative over primitive recursive arithmetic PRA . On the other hand there are principles S of elementary analysis which are known to be equivalent to arithmetical comprehension and therefore go far beyond the strength of PRA . In this paper we determine precisely the arithmetical and computational strength of weaker function parameter-free schematic versions S− of S, thereby exhibiting different levels (...) of strength between these principles as well as a sharp borderline between fragments of analysis which are still conservative over PRA and extensions which just go beyond the strength of PRA. (shrink)

Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Annals of Pure and Applied Logic 64 27–94.We consider uniqueness theorems in classical analysis having the form u ε U, v1, v2 ε Vu = 0 = G→v 1 = v2), where U, V are complete separable metric spaces, Vu is compact in V and G:U x V → is a constructive function.If is proved by arithmetical means from analytical assumptions (...) x εXy ε Yx z ε Z = 0) only , then we can extract from the proof of → an effective modulus of uniqueness, which depends on u, k but not on v1,v2, i.e., u ε U, v1, v2 ε Vu, k εG, G 2-φuk→dv2-itk). Such a modulus φ can e.g. be used to give a finite algorithm which computes the zero of G on Vu with prescribed precision if it exists classically.The extraction of φ uses a proof-theoretic combination of functional interpretation and pointwise majorization. If the proof of → uses only simple instances of induction, then φ is a simple mathematical operation. (shrink)

In this note we show that over a strong intuitionistic base theory, the recursive comprehension principle \ -CA does not imply the disjunctive Markov principle MP\.

Synthetic biology is a dynamic, young, ambitious, attractive, and heterogeneous scientific discipline. It is constantly developing and changing, which makes societal evaluation of this emerging new science a challenging task, prone to misunderstandings. Synthetic biology is difficult to capture, and confusion arises not only regarding which part of synthetic biology the discussion is about, but also with respect to the underlying concepts in use. This book offers a useful toolbox to approach this complex and fragmented field. It provides a biological (...) access to the discussion using a 'layer' model that describes the connectivity of synthetic or semisynthetic organisms and cells to the realm of natural organisms derived by evolution. Instead of directly reviewing the field as a whole, firstly our book addresses the characteristic features of synthetic biology that are relevant to the societal discussion. Some of these features apply only to parts of synthetic biology, whereas others are relevant to synthetic biology as a whole. In the next step, these new features are evaluated with respect to the different areas of synthetic biology. Do we have the right words and categories to talk about these new features? In the third step, traditional concepts like "life" and "artificiality" are scrutinized with regard to their discriminatory power. This approach may help to differentiate the discussion on synthetic biology. Lastly our refined view is utilized for societal evaluation. We have investigated the public views and attitudes to synthetic biology. It also includes the analysis of ethical, risk and legal questions, posed by present and future practices of synthetic biology. This book contains the results of an interdisciplinary research project and presents the authors' main findings and recommendations. They are addressed to science, industry, politics and the general public interested in this upcoming field of biotechnology. (shrink)

In this paper the numerical strength of fragments of arithmetical comprehension, choice and general uniform boundedness is studied systematically. These principles are investigated relative to base systems Tnω in all finite types which are suited to formalize substantial parts of analysis but nevertheless have provably recursive functions of low growth. We reduce the use of instances of these principles in Tnω-proofs of a large class of formulas to the use of instances of certain arithmetical principles thereby determining faithfully the arithmetical (...) content of the former. This is achieved using the method of elimination of Skolem functions for monotone formulas which was introduced by the author in a previous paper.As corollaries we obtain new conservation results for fragments of analysis over fragments of arithmetic which strengthen known purely first-order conservation results.We also characterize the provably recursive functions of type 2 of the extensions of Tnω based on these fragments of arithmetical comprehension, choice and uniform boundedness. (shrink)

It is well-known (due to C. Parsons) that the extension of primitive recursive arithmeticPRA by first-order predicate logic and the rule ofΠ 2 0 -inductionΠ 2 0 -IR isΠ 2 0 -conservative overPRA. We show that this is no longer true in the presence of function quantifiers and quantifier-free choice for numbersAC 0,0-qf. More precisely we show that ℐ :=PRA 2 +Π 2 0 -IR+AC 0,0-qf proves the totality of the Ackermann function, wherePRA 2 is the extension ofPRA by number (...) and function quantifiers andΠ 2 0 -IR may contain function parameters. This is true even forPRA 2 +∑ 1 0 -IR+Π 2 0 -IR −+AC 0,0-qf, whereΠ 2 0 -IR − is the restriction ofΠ 2 0 -IR without function parameters. (shrink)

The Kennedy Institute of Ethics is grateful for the vision, guidance, and dedication on behalf of the Kennedy Institute of Ethics Journal by Robert M. Veatch, PhD, its senior editor and senior research scholar at the KIE. For over twenty years, Bob has steered the journal along its path of success, and its partnership with the Johns Hopkins University Press, to arrive at the place it holds today—truly a "scholarly forum for diverse views on major issues in bioethics." Bob has (...) retired from the editorship effective January 2011 (though thankfully not from the KIE!).We also wish to express our appreciation to Carol M. Spicer, PhD, the journal's editor and hands-on manager of KIEJ. Carol received her doctorate in .. (shrink)

We show that Shoenfield's functional interpretation of Peano arithmetic can be factorized as a negative translation due to J. L. Krivine followed by Gödel's Dialectica interpretation. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim).

Recently, Coquand and Palmgren considered systems of intuitionistic arithmetic in a finite types together with various forms of the axiom of choice and a numerical omniscience schema which implies classical logic for arithmetical formulas. Feferman subsequently observed that the proof theoretic strength of such systems can be determined by functional interpretation based on a non-constructive μ-operator and his well-known results on the strength of this operator from the 70's. In this note we consider a weaker form LNOS of NOS which (...) suffices to derive the strong form of binary König's lemma studied by Coquand/Palmgren and gives rise to a new and mathematically strong semi-classical system which, nevertheless, can proof theoretically be reduced to primitive recursive arithmetic PRA. The proof of this fact relies on functional interpretation and a majorization technique developed in a previous paper. (shrink)

Natural human behavior is segmented into action units, functionally related groups of movements with durations of a few seconds. This phenomenon can also be found in nonhuman primates and other mammals. In humans, a similar segmentation can be found in planning, preparatory behavior, perception, and speech. Temporal segmentation may be related to the functioning of short-term memory. Segmentation may thus be a central feature of neuronal integration. Segment length was hitherto thought to be determined by either capacity constraints or temporal (...) factors. Instead we show that segment length depends on the interplay between capacity and temporal factors. (shrink)

_The National Park to Come_ examines the sense of "the national" that our national parks construct and the kind of citizen they produce in the process. Who is the visitor in these spaces? Who is the national and who the foreigner? To whose children is the ostensibly unpeopled wilderness of the future owed? At what cost, and to whom? Grebowicz explores how such politicized modes of being-in-nature are maintained on the emotional level, shaping our basic sense of coherence, futurity, collectivity, (...) and having a life. Wilderness-as-spectacle, she argues, functions as a form of social relation even as we imagine the true experience of nature to be solitary and apolitical. The book's most pressing concern is the relationship between the foreigner and the future in the democratization of wilderness. For the questions explored here, contends Grebowicz, are precisely those that will shape the future of our entire park system. (shrink)

We show that the so-called weak Markov's principle which states that every pseudo-positive real number is positive is underivable in [MATHEMATICAL SCRIPT CAPITAL T]ω ≔ E-HAω + AC. Since [MATHEMATICAL SCRIPT CAPITAL T]ω allows one to formalize Bishop's constructive mathematics, this makes it unlikely that WMP can be proved within the framework of Bishop-style mathematics . The underivability even holds if the ine.ective schema of full comprehension for negated formulas is added, which allows one to derive the law of excluded (...) middle for such formulas. (shrink)

This fresh portrait of Varenius presents a young German scholar, whose books on Japan, the first one from a European perspective, and on General Geography were written and published in Amsterdam and led to establishing geography as a science.

If feminists argue for the irreducibility of the social dimensions of science, then they ought to embrace the idea that feminist and non-feminist scientists are not in collaboration, but in fact defend different interests. Instead, however, contemporary feminist science studies literature argues that feminist research improves particular, existing scientific enterprises, both epistemically (truer claims) and politically (more democratic methodologies and applications). I argue that the concepts of empirical success and democracy at work in this literature from Longino (1994) and Harding (...) (1996), to Longino (2002), Gilbert and Rader (2001), and Keller (2001) are not sufficiently critical, and fail to do justice to the truly revolutionary work done by feminist scientists. I offer the beginnings of an epistemology of dissensus (as opposed to consensus), using the work of Haraway (1978), Lyotard (1984), and Ziarek (2001). How would such an epistemology relate to feminist discussions of the possibility of democratic, responsible knowledge? (shrink)

The so-called weak König's lemma WKL asserts the existence of an infinite path b in any infinite binary tree . Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π 2 0 -conservative over primitive recursive arithmetic PRA . In Kohlenbach 1239–1273) we established such conservation results relative to finite type extensions PRA ω of PRA . In this setting one can consider also a (...) uniform version UWKL of WKL which asserts the existence of a functional Φ which selects uniformly in a given infinite binary tree f an infinite path Φf of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in Kohlenbach [10] actually can be used to eliminate even this uniform weak König's lemma provided that PRA ω only has a quantifier-free rule of extensionality QF-ER instead of the full axioms of extensionality for all finite types. In this paper we show that in the presence of , UWKL is much stronger than WKL: whereas WKL remains to be Π 2 0 -conservative over PRA, PRA ω ++ UWKL contains full Peano arithmetic PA. We also investigate the proof–theoretic as well as the computational strength of UWKL relative to the intuitionistic variant of PRA ω both with and without the Markov principle. (shrink)

Goodman's theorem states that intuitionistic arithmetic in all finite types plus full choice, HA + AC, is conservative over first-order intuitionistic arithmetic HA. We show that this result does not extend to various subsystems of HA, HA with restricted induction.

Examines Lyotard’s writings in light of contemporary feminist theory.

_The National Park to Come_ examines the sense of "the national" that our national parks construct and the kind of citizen they produce in the process. Who is the visitor in these spaces? Who is the national and who the foreigner? To whose children is the ostensibly unpeopled wilderness of the future owed? At what cost, and to whom? Grebowicz explores how such politicized modes of being-in-nature are maintained on the emotional level, shaping our basic sense of coherence, futurity, collectivity, (...) and having a life. Wilderness-as-spectacle, she argues, functions as a form of social relation even as we imagine the true experience of nature to be solitary and apolitical. The book's most pressing concern is the relationship between the foreigner and the future in the democratization of wilderness. For the questions explored here, contends Grebowicz, are precisely those that will shape the future of our entire park system. (shrink)

We prove a result relating the author's monotone functional interpretation to the bounded functional interpretation due to Ferreira and Oliva. More precisely we show that largely a solution for the bounded interpretation also is a solution for the monotone functional interpretation although the latter uses the existence of an underlying precise witness. This makes it possible to focus on the extraction of bounds while using the conceptual benefit of having precise realizers at the same time without having to construct them.

This volume examines the ways in which the authors of the early Frankfurt School criticized, adopted and modified traditional forms of religious thought and practice. Focusing on the works of Theodor W. Adorno, Walter Benjamin, Erich Fromm, Max Horkheimer, Otto Kirchheimer and Franz Neumann, it analyzes the relevance of religious traditions and of the Enlightenment critique of religion for modern conceptions of emancipatory thought, art, law, and politics.

Both Husserl and Popper share the sentiment that philosophy should model itself after something called "science," despite their differing attitudes toward the Galilean tradition. I begin by describing their respective approaches to the problem of objectivity by examining their accounts of the origins of science in Husserl's Vienna Lecture and Popper's Conjectures and Refutations. Each of them explicitly takes up the problem of objectivity in The Origin of Geometry and Epistemology Without a Knowing Subject, respectively, and it is here that (...) they develop their notions of the role played by subjectivity in science. I argue that Popper suffers from a commitment to subjectivism even in the course of renouncing the subject as irrelevant for science. Husserl, on the other hand, sees in the possibility of crisis the need to reinstate subjectivist concerns in order for any discourse to be capable of saying something about the world. Husserl thus proposes a scientism which takes account of the fact that the world is, first and foremost, experienced by subjects. I contend that Popper can ultimately be held to the same position, and thus be forced to qualify his strong dismissal of subjectivity. (shrink)

: Grebowicz argues from the perspective of Jean-François Lyotard's critique of deliberative democracy that the project of democratizing knowledge may bring us closer to terror than to justice. The successful formulation of a critical standpoint requires that we figure the political as itself a contested site, and incorporate this into our theorizing about the role of dissent in the production of knowledges. This essay contrasts Lyotard's notion of the differend with Chantal Mouffe's agonistic model.

In 2007. Terence Tao wrote on his blog an essay about soft analysis, hard analysis and the finitization of soft analysis statements into hard analysis statements. One of his main examples was a quasi-finitization of the infinite pigeonhole principle IPP, arriving at the "finitary" infinite pigeonhole principle FIPP₁. That turned out to not be the proper formulation and so we proposed an alternative version FIPP₂. Tao himself formulated yet another version FIPP₃ in a revised version of his essay. We give (...) a counterexample to FIPP₁ and discuss for both of the versions FIPP₂ and FIPP₃ the faithfulness of their respective finitization of IPP by studying the equivalences IPP ↔ FIPP₂ and IPP ↔ FIPP₃ in the context of reverse mathematics ([9]). In the process of doing this we also introduce a continuous uniform boundedness principle CUB as a formalization of Tao's notion of a correspondence principle and study the strength of this principle and various restrictions thereof in terms of reverse mathematics, i.e., in terms of the "big five" subsystems of second order arithmetic. (shrink)

In [U. Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 89–128], the second author obtained metatheorems for the extraction of effective bounds from classical, prima facie non-constructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT and normed linear spaces and guarantee the independence of the bounds from parameters ranging over metrically bounded spaces. Recently ]), the authors obtained generalizations of these metatheorems (...) which allow one to prove similar uniformities even for unbounded spaces as long as certain local boundedness conditions are satisfied. The use of classical logic imposes some severe restrictions on the formulas and proofs for which the extraction can be carried out. In this paper we consider similar metatheorems for semi-intuitionistic proofs, i.e. proofs in an intuitionistic setting enriched with certain non-constructive principles. Contrary to the classical case, there are practically no restrictions on the logical complexity of theorems for which bounds can be extracted. Again, our metatheorems guarantee very general uniformities, even in cases where the existence of uniform bounds is not obtainable by straightforward functional analytic means. Already in the purely intuitionistic case, where the existence of effective bounds is implicit, the metatheorems allow one to derive uniformities that may not be obvious at all from a given constructive proof. Finally, we illustrate our main metatheorem by an example from metric fixed point theory. (shrink)

In this paper a new method, elimination of Skolem functions for monotone formulas, is developed which makes it possible to determine precisely the arithmetical strength of instances of various non-constructive function existence principles. This is achieved by reducing the use of such instances in a given proof to instances of certain arithmetical principles. Our framework are systems ${\cal T}^{\omega} :={\rm G}_n{\rm A}^{\omega} +{\rm AC}$ -qf $+\Delta$ , where (G $_n$ A $^{\omega})_{n \in {\Bbb N}}$ is a hierarchy of (weak) subsystems (...) of arithmetic in all finite types (introduced in [14]), AC-qf is the schema of quantifier-free choice in all types and $\Delta$ is a set of certain analytical principles which e.g. includes the binary König's lemma. We apply this method to show that the arithmetical closures of single instances of $\Pi^0_1$ -comprehension and -choice contribute to the growth of extractable bounds from proofs relative to ${\cal T}^\omega$ only by a primitive recursive functional in the sense of Kleene. In subsequent papers these results are widely generalized and the method is used to determine the arithmetical content of single sequences of instances of the Bolzano-Weierstraß principle for bounded sequences in ${\Bbb R}^d$ , the Ascoli-lemma and others. (shrink)