Herbrand's Theorem, in the form of $$\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\exists } $$ -inversion lemmata for finitary and infinitary sequent calculi, is the crucial tool for the determination of the provably total function(al)s of a variety of theories. The theories are (second order extensions of) fragments of classical arithmetic; the classes of provably total functions include the elements of the Polynomial Hierarchy, the Grzegorczyk Hierarchy, and the extended Grzegorczyk Hierarchy $\mathfrak{E}^\alpha $ , α < ε0. A subsidiary aim of the paper is to show (...) that the proof theoretic methods used here are distinguished by technical elegance, conceptual clarity, and wide-ranging applicability. (shrink)

The Carnegie Mellon Proof Tutor project was motivated by pedagogical concerns: we wanted to use a "mechanical" (i.e. computerized) tutor for teaching students..

In his classic paper On Computable Numbers Turing analyzed what can be done by a human computor in a routine, “mechanical” way. He argued that mechanical op-erations obey locality conditions and are carried out on configurations satisfying boundedness conditions. Processes meeting these restrictive conditions can be shown to be computable by a Turing machine. Turing viewed memory limitations of computors as the ultimate reason for the restrictive conditions. In contrast, Gandy analyzed in his paper Church’s Thesis and Principles for Mechanisms (...) what can be done by “discrete deterministic mechanical devices” and appealed to physical considerations to motivate restrictive principles. These devices include, crucially, ones that carry out parallel processes, e.g., cellular automata. Following Turing’s methodological ways and guided by Conway’s “Game of Life” as a paradigm, Gandy formulated four restrictive principles and proved that devices satisfying them are computationally equivalent to Turing machines. (shrink)

Dieser Titel aus dem De Gruyter-Verlagsarchiv ist digitalisiert worden, um ihn der wissenschaftlichen Forschung zugänglich zu machen. Da der Titel erstmals im Nationalsozialismus publiziert wurde, ist er in besonderem Maße in seinem historischen Kontext zu betrachten. Mehr erfahren Sie.

— via appropriate substitutions — syntactically identical. The method can be applied directly to quantifierfree formulae and, in this paper, will b e extended in a natural and strai ghlforward way to quantified formulae.

In the pathbreaking essays collected here, Neumann and Kirchheimer demonstrate that the death of democracy and the rise of fascism during the first half of the twentieth century suggest crucial lessons for contemporary political and legal scholars. The volume includes writings on constitutionalism, political freedom, Nazism, sovereignty, and both Nazi and liberal law. Most important, the Frankfurt authors point to the continuing efficacy of the rule of law as an instrument for regulating and restraining state authority, as well as ominous (...) evidence of the rule of law's fragility in modern liberal democracy. (shrink)

This paper offers an intellectual discourse for destination managers by exploring alternative branding approaches used during the colonial period in Kenya, now that the image is under siege both internally through socio-economic instability and unprecedented levels of poaching, and externally through travel warnings, outright trafficking in big game trophies, the constant threat of terror attacks, and poor global rankings in the Travel and Tourism Competitive Index. The paper conforms to the mission of thought and practice by identifying practical ways of (...) promoting tourist destination Kenya through an in-depth analysis of historical experiences. (shrink)

The combative metaphor of Oscience warsO has taken on a predominant position within the collective conscious, from being featured on the programs of scientific meetings to being splashed across the pages of leading national magazines and newspapers. Some in the scientific community perceive their profession to be under siege by members of the academic left, radical environmentalists, religious fundamentalists, eco-feminists, and others. This book, based on in-depth interviews with sixty members of groups with alleged Oanti-scienceO attitudes, examines how pervasive and (...) uniform these critiques are. The research is designed to examine two conflicting hypotheses: 1) that anti-science attitudes reflect a general cynicism about all major social institutions, and 2) that anti-science views are not broadly based but are reflective, instead , of the particular interests of a given social grouping. In the final analysis, Perrucci and Trachtman dig at the root of the so-called Oscience warsO by presenting evidence that the wars are not the product of an overarching suspicion of the institutions at the core of our society, but are instead the product of organized interest groups, which shape the attitudes and beliefs of their respective members. (shrink)

The introductory revised essay, "Horses of Wrath: Recent Critical Lessons," followed by nine reprinted essays, pits the Christian Rationalist, Wimsatt, an aroused Horse of Instruction, against the Tigers of Wrath, Blakean Myth critics led by Northrop Frye. Their battleground is the relation of poetry to life: what for the Blakeans is the fearful symmetry of poetry as the apocalypse of life is for Wimsatt the hateful siege of contraries, both an anarchy of life and a confusion of poetic limits. Wimsatt (...) supports the classical and Christian notion that harmony comes "in spite of" the conflict of good and evil, not "because of" that conflict, as the Blakeans would claim. For Wimsatt, poetry's unique kind of cognition is the analogous perspective it establishes toward contraries, namely the perspective of drama and metaphor in which is created a mock substance of the human condition. But after Wimsatt's analysis, we are left with a dualism which can be itself a hateful contrary: the more poetry performs its perspective function, the more it destroys its subject matter. It is also to the credit of Wimsatt's theoretic hesitancy that he will not let us forget these contraries.—E. S. T. (shrink)

A. F. Norman has recently suggested that a hitherto overlooked passage in Suidas is a fragment from the history of Eunapius of Sardis. He is clearly correct in referring the passage to an incident at the siege of Maiozamalcha during the Persian campaign of the emperor Julian, but I am not so sure that he is right in ascribing it to Eunapius, or in the conclusions he draws from this ascription. I give in parallel columns the accounts of Ammianus Marcellinus, (...) Zosimus, and the passage from Suidas, together with a further version of the incident, unfortunately without names, from the pen of Libanius. (shrink)

A. F. Norman has recently suggested that a hitherto overlooked passage in Suidas is a fragment from the history of Eunapius of Sardis. He is clearly correct in referring the passage to an incident at the siege of Maiozamalcha during the Persian campaign of the emperor Julian, but I am not so sure that he is right in ascribing it to Eunapius, or in the conclusions he draws from this ascription. I give in parallel columns the accounts of Ammianus Marcellinus, (...) Zosimus, and the passage from Suidas, together with a further version of the incident, unfortunately without names, from the pen of Libanius. (shrink)

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)

The introductory revised essay, "Horses of Wrath: Recent Critical Lessons," followed by nine reprinted essays, pits the Christian Rationalist, Wimsatt, an aroused Horse of Instruction, against the Tigers of Wrath, Blakean Myth critics led by Northrop Frye. Their battleground is the relation of poetry to life: what for the Blakeans is the fearful symmetry of poetry as the apocalypse of life is for Wimsatt the hateful siege of contraries, both an anarchy of life and a confusion of poetic limits. Wimsatt (...) supports the classical and Christian notion that harmony comes "in spite of" the conflict of good and evil, not "because of" that conflict, as the Blakeans would claim. For Wimsatt, poetry's unique kind of cognition is the analogous perspective it establishes toward contraries, namely the perspective of drama and metaphor in which is created a mock substance of the human condition. But after Wimsatt's analysis, we are left with a dualism which can be itself a hateful contrary: the more poetry performs its perspective function, the more it destroys its subject matter. It is also to the credit of Wimsatt's theoretic hesitancy that he will not let us forget these contraries.—E. S. T. (shrink)

Abstract“Victories of Freedom which Humans Achieved by Research in the Foundation of Things”. ‐ This article analyzes the political self‐conception of leading representatives of the natural sciences in 19th century Germany. It is argued that the main feature of this self‐conception which remained constant over the time consisted in a strong “rationalization‐imperative”, i.e. the postulate that state and society have to be reshaped on the basis of natural science. On the other hand, this imperative was put forward in very different (...) forms and with different political content: it shifted from revolutionary aspirations in the period of 1848 to moderate and sometimes even reactionary positions in the last decades of the century. (shrink)

C. F. Gellert's 1748 novel "Leben der schwedischen Gräfin von G***" portrays the moral actions of Jews as a result of good Christian conduct. In reaction, G. E. Lessing disputes this depiction in his one-act-play "Die Juden" from 1749. The recognition that a Jew could fulfill the ideals of the Enlightenment helped overcome the prejudices of Christian stage characters and of the audience, but it failed in the social circumstances of the time. Christian reception understood a "noble Jew" to be (...) a violation of the poetic principle of probability - and even for Lessing such a figure was the exception. Moses Mendelssohn, however, believed that Judaism was especially well-suited for fostering the development of certain virtues. In light of far-reaching interreligious concepts on the one hand and religiously motivated conflicts on the other, Lessing's early works reveal today the persistent value of self-critical examination concerning hidden prejudices towards religious and cultural minorities. (shrink)

The identification of an informal concept of ‘effective calculability’ with a rigorous mathematical notion like ‘recursiveness’ or ‘Turing computability’ is still viewed as problematic, and I think rightly so. I analyze three different and conflicting perspectives Gödel articulated in the three decades from 1934 to 1964. The significant shifts in Gödel's position underline the difficulties of the methodological issues surrounding the Church-Turing Thesis.

Since their inception, the Perspectives in Logic and Lecture Notes in Logic series have published seminal works by leading logicians. Many of the original books in the series have been unavailable for years, but they are now in print once again. This volume, the fifteenth publication in the Lecture Notes in Logic series, collects papers presented at the symposium 'Reflections on the Foundations of Mathematics' held in celebration of Solomon Feferman's 70th birthday (The 'Feferfest') at Stanford University, California in 1988. (...) Feferman has shaped the field of foundational research for nearly half a century. These papers reflect his broad interests as well as his approach to foundational research, which emphasizes the solution of mathematical and philosophical problems. There are four sections, covering proof theoretic analysis, logic and computation, applicative and self-applicative theories, and philosophy of modern mathematical and logic thought. (shrink)

Wilfred Sieg. Mechanical Procedures and Mathematical Experience.

Wilfred Sieg and Dirk Schlimm. Dedekind's Analysis of Number: Systems and Axioms.

We establish by elementary proof-theoretic means the conservativeness of two subsystems of analysis over primitive recursive arithmetic. The one subsystem was introduced by Friedman [6], the other is a strengthened version of a theory of Minc [14]; each has been shown to be of considerable interest for both mathematical practice and metamathematical investigations. The foundational significance of such conservation results is clear: they provide a direct finitist justification of the part of mathematical practice formalizable in these subsystems. The results are (...) generalized to relate a hierarchy of subsystems, all contained in the theory of arithmetic properties, to a corresponding hierarchy of fragments of arithmetic. The proof theoretic tools employed there are used to re-establish in a uniform, elementary way relationships between various fragments of arithmetic due to Parsons, Paris and Kirby, and Friedman. (shrink)

Hilbert's finitist program was not created at the beginning of the twenties solely to counteract Brouwer's intuitionism, but rather emerged out of broad philosophical reflections on the foundations of mathematics and out of detailed logical work; that is evident from notes of lecture courses that were given by Hilbert and prepared in collaboration with Bernays during the period from 1917 to 1922. These notes reveal a dialectic progression from a critical logicism through a radical constructivism toward finitism; the progression has (...) to be seen against the background of the stunning presentation of mathematical logic in the lectures given during the winter term 1917/18. In this paper, I sketch the connection of Hilbert's considerations to issues in the foundations of mathematics during the second half of the 19th century, describe the work that laid the basis of modern mathematical logic, and analyze the first steps in the new subject of proof theory. A revision of the standard view of Hilbert's and Bernays's contributions to the foundational discussion in our century has long been overdue. It is almost scandalous that their carefully worked out notes have not been used yet to understand more accurately the evolution of modern logic in general and of Hilbert's Program in particular. One conclusion will be obvious: the dogmatic formalist Hilbert is a figment of historical (de)construction! Indeed, the study and analysis of these lectures reveal a depth of mathematical-logical achievement and of philosophical reflection that is remarkable. In the course of my presentation many questions are raised and many more can be explored; thus, I hope this paper will stimulate interest for new historical and systematic work. (shrink)

David Hilbert was one of the great mathematicians who expounded the centrality of their subject in human thought. In this collection of essays, Wilfried Sieg frames Hilbert's foundational work, from 1890 to 1939, in a comprehensive way and integrates it with modern proof theoretic investigations.

It is a remarkable fact that Hilbert's programmatic papers from the 1920s still shape, almost exclusively, the standard contemporary perspective of his views concerning (the foundations of) mathematics; even his own, quite different work on the foundations of geometry and arithmetic from the late 1890s is often understood from that vantage point. My essay pursues one main goal, namely, to contrast Hilbert's formal axiomatic method from the early 1920s with his existential axiomatic approach from the 1890s. Such a contrast illuminates (...) the circuitous beginnings of the finitist consistency program and connects the complex emergence of existential axiomatics with transformations in mathematics and philosophy during the 19th century; the sheer complexity and methodological difficulties of the latter development are partially reflected in the well known, but not well understood correspondence between Frege and Hilbert. Taking seriously the goal of formalizing mathematics in an effective logical framework leads also to contemporary tasks, not just historical and systematic insights; those are briefly described as “one direction” for fascinating work. (shrink)

Alonzo Church's mathematical work on computability and undecidability is well-known indeed, and we seem to have an excellent understanding of the context in which it arose. The approach Church took to the underlying conceptual issues, by contrast, is less well understood. Why, for example, was "Church's Thesis" put forward publicly only in April 1935, when it had been formulated already in February/March 1934? Why did Church choose to formulate it then in terms of Gödel's general recursiveness, not his own λ (...) -definability as he had done in 1934? A number of letters were exchanged between Church and Paul Bernays during the period from December 1934 to August 1937; they throw light on critical developments in Princeton during that period and reveal novel aspects of Church's distinctive contribution to the analysis of the informal notion of effective calculability. In particular, they allow me to give informed, though still tentative answers to the questions I raised; the character of my answers is reflected by an alternative title for this paper, Why Church needed Gödel's recursiveness for his Thesis. In Section 5, I contrast Church's analysis with that of Alan Turing and explore, in the very last section, an analogy with Dedekind's investigation of continuity. (shrink)

Wilfried Sieg. Calculations by Man and Machine: Conceptual Analysis.

Dedekind’s structuralism is a crucial source for the structuralism of mathematical practice—with its focus on abstract concepts like groups and fields. It plays an equally central role for the structuralism of philosophical analysis—with its focus on particular mathematical objects like natural and real numbers. Tensions between these structuralisms are palpable in Dedekind’s work, but are resolved in his essay Was sind und was sollen die Zahlen? In a radical shift, Dedekind extends his mathematical approach to “the” natural numbers. He creates (...) the abstract concept of a simply infinite system, proves the existence of a “model”, insists on the stepwise derivation of theorems, and defines structure-preserving mappings between different systems that fall under the abstract concept. Crucial parts of these considerations were added, however, only to the penultimate manuscript, for example, the very concept of a simply infinite system. The methodological consequences of this radical shift are elucidated by an analysis of Dedekind’s metamathematics. Our analysis provides a deeper understanding of the essay and, in addition, illuminates its impact on the evolution of the axiomatic method and of “semantics” before Tarski. This understanding allows us to make connections to contemporary issues in the philosophy of mathematics and science. (shrink)

Wilfred Sieg. Relative Consistency and Accesible Domains.

Wilfried Sieg and John Byrnes. AnModel for Parallel Computation: Gandy's Thesis.

"Élève-toi, mon éloquence, j'aperçois Platon qui s'élève au-dessus de l'homme! C'est sur sa bouche que les abeilles ont fait leur miel, que les rossignols ont chanté, que la déesse de la persuasion a élu son siège..." Le jésuite Nicolas Caussin témoigne ici pour nous de la mémoire du platonisme qui est celle du XVIIe siècle: un portrait de Platon en philosophe orateur s'y affirme, où la figure du Sage s'allie au prestige de l'écrivain pour consacrer comme modèle rhétorique celui que (...) Longin nomme l'Homère des philosophes. Après avoir chassé les poètes et fustigé les orateurs, le Platon des classiques redevient le théoricien du Phèdre, de l'Ion et des Lois, l'instigateur d'une philosophie éloquente et d'un lyrisme vertueux. Modèle de pensée et d'écriture pour une rhétorique du philosophique d'abord socratique, puis avec les intuitions d'un Claude Fleury, bientôt poétique, le divin philosophe nous invite alors à réfléchir sur le difficile croisement que l'humanisme classique tente d'opérer entre morale et éloquence relevée. Car ce retour d'un platonisme dans la philosophie de la rhétorique s'est effectué au sein de milieux humanistes mondains puis dévots, et a donné lieu à l'élaboration de formes extrêmement raffinées dans l'écriture de la morale. À travers la leçon de Platon, l'éloquence du Sage s'avère désormais séminale pour intégrer dans les belles-lettres une exigence de spirituel et leur accorder ainsi un nouveau prestige. C'est donc un tableau de la littérature morale à la manière de Platon qui, de La Fontaine à La Bruyère et au Fénelon du Télémaque, se trouve ici esquissé. (shrink)

Church's and Turing's theses dogmatically assert that an informal notion of effective calculability is adequately captured by a particular mathematical concept of computability. I present an analysis of calculability that is embedded in a rich historical and philosophical context, leads to precise concepts, but dispenses with theses. To investigate effective calculability is to analyze symbolic processes that can in principle be carried out by calculators. This is a philosophical lesson we owe to Turing. Drawing on that lesson and recasting work (...) of Gandy, I formulate boundedness and locality conditions for two types of calculators, namely, human computing agents and mechanical computing devices (discrete machines). The distinctive feature of the latter is that they can carry out parallel computations. The analysis leads to axioms for discrete dynamical systems (representing human and machine computations) and allows the reduction of models of these axioms to Turing machines. Cellular automata and a variety of artificial neural nets can be shown to satisfy the axioms for machine computations. (shrink)

On June 4, 1925, Hilbert delivered an address to the Westphalian Mathematical Society in Miinster; that was, as a quick calculation will convince you, almost exactly sixty years ago. The address was published in 1926 under the title Über dasUnendlicheand is perhaps Hilbert's most comprehensive presentation of his ideas concerning the finitist justification of classical mathematics and the role his proof theory was to play in it. But what has become of the ambitious program for securing all of mathematics, once (...) and for all? What of proof theory, the very subject Hilbert invented to carry out his program? The Hilbertian ambition reached out too far: in its original form, the program was refuted by Gödel's Incompleteness Theorems. And even allowing more than finitist means in metamathematics, the Hilbertian expectations for proof theory have not been realized: a constructive consistency proof for second-order arithmetic is still out of reach. Nevertheless, remarkable progress has been made. Two separate, but complementary directions of research have led to surprising insights: classical analysis can be formally developed in conservative extensions of elementary number theory; relative consistency proofs can be given by constructive means for impredicative parts of second order arithmetic. The mathematical and metamathematical developments have been accompanied by sustained philosophical reflections on the foundations of mathematics. This indicates briefly the main themes of the contributions to the symposium; in my introductory remarks I want to give a very schematic perspective, that is partly historical and partly systematic. (shrink)

The incompleteness theorems constitute the mathematical core of Gödel’s philosophical challenge. They are given in their “most satisfactory form”, as Gödel saw it, when the formality of theories to which they apply is characterized via Turing machines. These machines codify human mechanical procedures that can be carried out without appealing to higher cognitive capacities. The question naturally arises, whether the theorems justify the claim that the human mind has mathematical abilities that are not shared by any machine. Turing admits that (...) non-mechanical steps of intuition are needed to transcend particular formal theories. Thus, there is a substantive point in comparing Turing’s views with Gödel’s that is expressed by the assertion, “The human mind infinitely surpasses any finite machine”. The parallelisms and tensions between their views are taken as an inspiration for beginning to explore, computationally, the capacities of the human mathematical mind. (shrink)

Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame (...) is a definitional extension of Zermelo–Fraenkel set theory and has a hierarchically organized structure of concepts and operations, and (3) the construction of formal proofs is deeply connected to the frame through rules for definitions and lemmas. To bring these general ideas to life, we examine, as a case study, proofs of the Cantor–Bernstein Theorem that do not appeal to the principle of choice. A thorough analysis of the multitude of “different” informal proofs seems to reduce them to exactly one. The natural formalization confirms that there is one proof, but that it comes in two variants due to Dedekind and Zermelo, respectively. In this way it enhances the conceptual understanding of the represented informal proofs. The formal, computational work is carried out with the proof search system AProS that serves as a proof assistant and implements the above inference mechanism; it can be fully inspected at (see link below). (shrink)

Wilfried Sieg. Calculations by Man and Machine: Mathematical Presentation.

Wilfred Sieg and John Byrnes. K-Graph Machines: Generalizing Turing's Machines and Arguments.

Dedekind's mathematical work is integral to the transformation of mathematics in the nineteenth century and crucial for the emergence of structuralist mathematics in the twentieth century. We investigate the essential components of what Emmy Noether called, his ‘axiomatic standpoint’: abstract concepts, models, and mappings.

Two young logicians, whose work had a dramatic impact on the direction of logic, exchanged two letters in early 1931. Jacques Herbrand initiated the correspondence on 7 April and Kurt Gödel responded on 25 July, just two days before Herbrand died in a mountaineering accident at La Bérarde (Isère). Herbrand's letter played a significant role in the development of computability theory. Gödel asserted in his 1934 Princeton Lectures and on later occasions that it suggested to him a crucial part of (...) the definition of a general recursive function. Understanding this role in detail is of great interest as the notion is absolutely central. The full text of the letter had not been available until recently, and its content (as reported by Gödel) was not in accord with Herbrand's contemporaneous published work. Together, the letters reflect broader intellectual currents of the time: they are intimately linked to the discussion of the incompleteness theorems and their potential impact on Hilbert's Program. (shrink)