The complexity class of [Formula: see text]-polynomial local search problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1 ≤ i ≤ k + 1, the [Formula: see text]-definable functions of [Formula: see text] are characterized in terms of [Formula: see text]-PLS problems. These [Formula: see text]-PLS problems can be defined in a weak base theory such as [Formula: see text], and proved to be total in [Formula: see text]. Furthermore, the [Formula: (...) see text]-PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. We introduce a new [Formula: see text]-principle that is conjectured to separate [Formula: see text] and [Formula: see text]. (shrink)

We investigate the relation between intermediate predicate logics based on countable linear Kripke frames with constant domains and Gödel logics. We show that for any such Kripke frame there is a Gödel logic which coincides with the logic defined by this Kripke frame on constant domains and vice versa. This allows us to transfer several recent results on Gödel logics to logics based on countable linear Kripke frames with constant domains: We obtain a complete characterisation of axiomatisability of logics based (...) on countable linear Kripke frames with constant domains. Furthermore, we obtain that the total number of logics defined by countable linear Kripke frames on constant domains is countable. (shrink)

We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ-calculus with β-, ξ- and η-conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.

Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of sΠ b 1(X) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories sΣ b n (X)−L m IND for m=n and m=n+1, n≥0. Different dynamic ordinals lead to (...) separation. In this way we will obtain several separation results between these relativized theories. We will generalize our results to further languages extending the language of bounded arithmetic. (shrink)

We prove that the boundedness theorem of generalized recursion theory can be derived from the ω-completeness theorem for number theory. This yields a proof of the boundedness theorem which does not refer to the analytical hierarchy theorem.

This paper proves exponential separations between depth d-LK and depth -LK for every utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth -LK for . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size -LK-refutations for to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle (...) and d=0. From this we also deduce width lower bounds for resolution refutations of the Ramsey principle. (shrink)

Inspired from Buchholz' ordinal analysis of ID1 and Beckmann's analysis of the simple typed λ-calculus we classify the derivation lengths for Gödel's system T in the λ-formulation.

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.

Let T be Gödel's system of primitive recursive functionals of finite type in a combinatory logic formulation. Let $T^{\star}$ be the subsystem of T in which the iterator and recursor constants are permitted only when immediately applied to type 0 arguments. By a Howard-Schütte-style argument the $T^{\star}$ -derivation lengths are classified in terms of an iterated exponential function. As a consequence a constructive strong normalization proof for $T^{\star}$ is obtained. Another consequence is that every $T^{\star}$ -representable number-theoretic function is elementary (...) recursive. Furthermore, it is shown that, conversely, every elementary recursive function is representable in $T^{\star}$ .The expressive weakness of $T^{\star}$ compared to the full system T can be explained as follows: In contrast to $T$ , computation steps in $T^{\star}$ never increase the nesting-depth of ${\mathcal I}_\rho$ and ${\mathcal R}_\rho$ at recursion positions. (shrink)

We construct by diagonalization a non-well-founded primitive recursive tree, which is well-founded for co-r.e. sets, provable in Σ1 0. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ1 0, equals the limit of all recursive ordinals ω1 ck . RID=""ID="" Mathematics Subject Classification (2000): 03B30, 03F15 RID=""ID="" Supported by the Deutschen Akademie der Naturforscher Leopoldina grant #BMBF-LPD 9801-7 with funds from the Bundesministerium für Bildung, Wissenschaft, Forschung und Technologie. RID=""ID="" (...) I would like to thank A. SETZER for his hospitality during my stay in Uppsala in December 1998 – these investigations are inspired by a discussion with him; S. BUSS for his hospitality during my stay at UCSD and for valuable remarks on a previous version of this paper; and M. MÖLLERFELD for remarks on a previous title. (shrink)

The theories Si1 and Ti1 are the analogues of Buss' relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i, a Σbi+1-formula TOPi, which expresses a form of the total ordering principle, is exhibited that is provable in Si+11 , but unprovable in Ti1. This is in contrast with the classical situation, where Si+12 is conservative over Ti2 w. r. t. Σbi+1-sentences. The independence (...) results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems. (shrink)

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.

This paper studies the complexity of constant depth propositional proofs in the cedent and sequent calculus. We discuss the relationships between the size of tree-like proofs, the size of dag-like proofs, and the heights of proofs. The main result is to correct a proof construction in an earlier paper about transformations from proofs with polylogarithmic height and constantly many formulas per cedent.

We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S 1 2 . In particular this solves an open problem formulated by TAKEUTI (c.f. [5, p.5 problem 9.]).

We define and study a new restricted consistency notion RCon ∗ for bounded arithmetic theories T 2 j . It is the strongest ∀ Π 1 b -statement over S 2 1 provable in T 2 j , similar to Con in Krajíček and Pudlák, 29) or RCon in Krajı́ček and Takeuti 107). The advantage of our notion over the others is that RCon ∗ can directly be used to construct models of T 2 j . We apply this by (...) proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The ∀ Π 1 b -separation of bounded arithmetic theories S 2 i from T 2 j is equivalent to the existence of a model of S 2 i which does not have a Δ 0 b -elementary extension to a model of T 2 j . More specific, let M ⊨ Ω 1 nst denote that there is a nonstandard element c in M such that the function n ↦ 2 log c is total in M . Let BLΣ 1 b be the bounded collection schema for Σ 1 b -formulas. We obtain the following preservation results: the ∀ Π 1 b -separation of S 2 i from T 2 j is equivalent to the existence of 1. a model of S 2 i +Ω 1 nst which is 1 b -closed w.r.t. T 2 j , 2. a countable model of S 2 i + BLΣ 1 b without weak end extensions to models of T 2 j. (shrink)

Seit fast 200 Jahren wird Clausewitz gelesen und interpretiert. Rasmus Beckmann erschließt seine Kriegstheorie den modernen Sozialwissenschaften. Dabei wird deutlich, dass sich Clausewitz keineswegs auf zwischenstaatliche Kriege beschränkt hat. Auch die asymmetrischen Kriege kann man durch seine Theorie besser analysieren und verstehen. Dies zeigt der Autor am Beispiel des Afghanistankrieges.

"Arguing that debates over legitimacy, political violence, freedom, and justice would benefit greatly from cross-tradition theorizing, this book shows how putting analytic and continental political theory in conversation would help us to overcome these intractable problems"--.

Am 6. Dezember 1915 und am 8. Januar 1916 legte Arnold Sommerfeld der Bayerischen Akademie der Wissenschaften zwei Abhandlungen im Umfang von 75 Druckseiten vor, mit denen er das Bohrsche Atommodell aus dem Jahr 1913 zur Bohr-Sommerfeldschen Atomtheorie erweiterte. In Sommerfelds Gesammelten Schriften findet sich nur die im Juli 1916 von Sommerfeld in den Annalen der Physik eingereichte Publikation darüber. "Meine Spektrallinien sind endlich in der Akademie in’s Unreine gedruckt. In den Annalen werden sie in geläuterter Form erscheinen", so (...) hatte Sommerfeld am 10. Februar 1916 dem Herausgeber der Annalen der Physik diese Publikation angekündigt. Aus wissenschaftshistorischer Sicht sind für die Erweiterung der Bohrschen Atomtheorie jedoch gerade die vor dem Läuterungsprozess publizierten Akademieabhandlungen von besonderem Interesse. Der Reproduktion dieser Akademieabhandlungen wird ein ausführlicher physikhistorischer Essay (ca. 100 Druckseiten) vorangestellt. (shrink)

As forms of private self-regulation, multi-stakeholder initiatives have emerged as an important empirical phenomenon in global governance processes. At the same time, MSIs are also theoretically intriguing because of their inherent double nature. On the one hand, MSIs spell out CSR standards that define norms for corporate behavior. On the other hand, MSIs are also the result of corporate and stakeholder behavior. We combine the perspectives of institutional theory and club theory to conceptualize this double nature of MSIs. Based on (...) a stage model that looks at the interplay of actor and institutional dynamics, we generate insights into why actors join a voluntary MSI, how the various motivations and intentions of the actors influence the standard development, and how these as well as the MSI design are subsequently influenced by both external and internal dynamics. (shrink)

"As a 'rhetoric of the mean' (mesotes ideal), sensibility provides a positive catalog of emotionalization. This is because ethos as an emotional level is viewed as being able, through gentle emotions, to please, placate and achieve sympathy and virtue (Quintilian). Sensibility in literature creates a bridge between an 'art of the soul' that developed into a major subjective and personal factor in the 18th century and a sense of sociability that aimed to integrate the individual into the community. The goal (...) of this study is to provide, through a structural linking of the ethos of virtue and the 'rhetoric of the mean', a reading of literature of sensibility based on rhetoric and cultural history that can explain both its public success 'with the people' and the reasons for why it failed to meet its own claims."--Publisher's website. (shrink)

This book explores the relationship between scientific fact and metaphysical reality, offering a fresh perspective on the intersection of these two seemingly disparate fields. This work has been selected by scholars as being culturally important, and is part of the knowledge base of civilization as we know it. This work is in the "public domain in the United States of America, and possibly other nations. Within the United States, you may freely copy and distribute this work, as no entity (individual (...) or corporate) has a copyright on the body of the work. Scholars believe, and we concur, that this work is important enough to be preserved, reproduced, and made generally available to the public. We appreciate your support of the preservation process, and thank you for being an important part of keeping this knowledge alive and relevant. (shrink)